## База данных ограничений » History » Version 71

*Andrei Tatarnikov, 12/26/2011 10:28 AM *

1 | 3 | Andrei Tatarnikov | h1. Constraint Solver |
---|---|---|---|

2 | 1 | Alexander Kamkin | |

3 | 69 | Andrei Tatarnikov | The constraint solver subsystem is aimed to provide the possibility to automatically generate test cases based on specified constraints. A constraint is represented by a set of limitations for input values. Solvers calculate values of input variables which will violate the limitations if there are any such values. |

4 | 6 | Andrei Tatarnikov | |

5 | 44 | Andrei Tatarnikov | The subsystem uses an openly distributed SMT solver as an engine (in the current version, we use the Z3 solver by Microsoft Research). In SMT solvers, a special functional language is used to specify constraints. The constraint solver subsystem generates constructions in the SMT language and runs the engine to process them and produce the results (find values of unknown input variables). |

6 | 3 | Andrei Tatarnikov | |

7 | 1 | Alexander Kamkin | h2. Constraints and Satisfiability Modulo Theories (SMT) |

8 | 44 | Andrei Tatarnikov | |

9 | 48 | Andrei Tatarnikov | Constrains specified as an SMT model are represented by a set of assertions (formulas) that must be satisfied. An SMT solver checks the satisfiability of the model and suggests a solution (variable values) that would satisfy the model. In the example below, we specify a model that should help us create a test that will cause a MIPS processor to generate an exception. We want to find values of the rs and rt general purpose registers that will cause the ADD instruction to raise an integer overflow exception. It should be correct 32-bit signed integers that are not equal to each other. Here is an SMT script: |

10 | 43 | Andrei Tatarnikov | |

11 | <pre> |
||

12 | (define-sort Int_t () (_ BitVec 64)) |
||

13 | |||

14 | (define-fun INT_ZERO () Int_t (_ bv0 64)) |
||

15 | (define-fun INT_BASE_SIZE () Int_t (_ bv32 64)) |
||

16 | (define-fun INT_SIGN_MASK () Int_t (bvshl (bvnot INT_ZERO) INT_BASE_SIZE)) |
||

17 | |||

18 | (define-fun IsValidPos ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_ZERO) true false)) |
||

19 | (define-fun IsValidNeg ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_SIGN_MASK) true false)) |
||

20 | (define-fun IsValidSignedInt ((x!1 Int_t)) Bool (ite (or (IsValidPos x!1) (IsValidNeg x!1)) true false)) |
||

21 | |||

22 | (declare-const rs Int_t) |
||

23 | (declare-const rt Int_t) |
||

24 | |||

25 | ; rt and rs must contain valid sign-extended 32-bit values (bits 63..31 equal) |
||

26 | (assert (IsValidSignedInt rs)) |
||

27 | (assert (IsValidSignedInt rt)) |
||

28 | |||

29 | ; the condition for an overflow: the summation result is not a valid sign-extended 32-bit value |
||

30 | (assert (not (IsValidSignedInt (bvadd rs rt)))) |
||

31 | |||

32 | ; just in case: rs and rt are not equal (to make the results more interesting) |
||

33 | (assert (not (= rs rt))) |
||

34 | |||

35 | (check-sat) |
||

36 | |||

37 | (echo "Values that lead to an overflow:") |
||

38 | 35 | Andrei Tatarnikov | (get-value (rs rt)) |

39 | </pre> |
||

40 | |||

41 | 56 | Andrei Tatarnikov | In an ideal case, each run of an SMT solver should return random values from the set of possible solutions. This should improve test coverage. Unfortunately, the current implementation is limited to a single solution that is constant for all run. This should be improved in the final version. |

42 | 49 | Andrei Tatarnikov | |

43 | 59 | Andrei Tatarnikov | h2. Tree Representation |

44 | 18 | Andrei Tatarnikov | |

45 | 57 | Andrei Tatarnikov | In our system, we use context-independent syntax trees to represent constraints. These trees are then used to generate a representation that can be understood by a particular SMT solver. Generally, it is an SMT model that uses some limited set of solver features applicable to microprocessor verification. The syntax tree contains nodes of the following types: |

46 | 69 | Andrei Tatarnikov | # Constraint. This is the root node of the tree. It holds the list of unknown variables and the list of assertions (formulas) for these variables. |

47 | 55 | Andrei Tatarnikov | # Formula. Represents an assertion expression. Can be combined with other formulas to build a more complex expression (by applying logic OR, AND or NOT to it). The underlying expression must be a logic expression that can be solved to true or false. |

48 | 13 | Andrei Tatarnikov | # Operation. Represents an unary or binary operation with some unknown variable, some value or some expression as parameters. |

49 | 69 | Andrei Tatarnikov | # Variable.Represents an input variable. It can have an assigned value and, in such a case, will be treated as a value. Otherwise, it is an unknown variable. A variable includes a type as an attribute. |

50 | 14 | Andrei Tatarnikov | # Value. Specifies some known value of the specified type which can be accessed as an attribute. |

51 | 17 | Andrei Tatarnikov | |

52 | 69 | Andrei Tatarnikov | Note: Operation, Variables and Value are designed to be treated polymorphically. This allows combining them to build complex expressions. |

53 | 16 | Andrei Tatarnikov | |

54 | 22 | Andrei Tatarnikov | h2. Constraint Solver Java Library |

55 | 3 | Andrei Tatarnikov | |

56 | 58 | Andrei Tatarnikov | The Constraint Solver subsystem is implemented in Java. The source code files are located in the "microtesk++/constraint-solver" folder. The Java classes are organized in the following packages: |

57 | # ru.ispras.microtesk.constraints - contains SMT model generation logic and solver implementations. |
||

58 | 1 | Alexander Kamkin | # ru.ispras.microtesk.constraints.syntax - contains classes implementing syntax tree nodes. |

59 | # ru.ispras.microtesk.constraints.syntax.types - contains code that specifies particular data types and operation types. |
||

60 | # ru.ispras.microtesk.constraints.tests - contains JUnit test cases. |
||

61 | |||

62 | 32 | Andrei Tatarnikov | h3. Core classes/interfaces |

63 | 66 | Andrei Tatarnikov | |

64 | 70 | Andrei Tatarnikov | The syntax tree nodes are implemented in the following classes: |

65 | * Constraint |
||

66 | * Formula |
||

67 | 71 | Andrei Tatarnikov | * Operation (implements SyntaxElement) |

68 | * Variable (implements SyntaxElement) |
||

69 | * Value (implements SyntaxElement) |
||

70 | |||

71 | The SyntaxElement interface provides the ability to combine different kinds of elements into expressions. |
||

72 | 70 | Andrei Tatarnikov | |

73 | 66 | Andrei Tatarnikov | The current implementation supports operations with the following data types: |

74 | # Bit vectors |
||

75 | # Booleans |
||

76 | 60 | Andrei Tatarnikov | |

77 | 64 | Andrei Tatarnikov | Example ..... : |

78 | 61 | Andrei Tatarnikov | |

79 | <pre> |
||

80 | class BitVectorIntegerOverflowTestCase implements SolverTestCase |
||

81 | { |
||

82 | 65 | Andrei Tatarnikov | private static final int BIT_VECTOR_LENGTH = 64; |

83 | private static final DataType BIT_VECTOR_TYPE = DataType.getBitVector(BIT_VECTOR_LENGTH); |
||

84 | private static final Value INT_ZERO = new Value(new BigInteger("0"), BIT_VECTOR_TYPE); |
||

85 | private static final Value INT_BASE_SIZE = new Value(new BigInteger("32"), BIT_VECTOR_TYPE); |
||

86 | |||

87 | private static final Operation INT_SIGN_MASK = |
||

88 | new Operation(BitVectorOperation.BVSHL, new Operation(BitVectorOperation.BVNOT, INT_ZERO, null), INT_BASE_SIZE); |
||

89 | 61 | Andrei Tatarnikov | |

90 | private Operation IsValidPos(SyntaxElement arg) |
||

91 | { |
||

92 | return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_ZERO); |
||

93 | } |
||

94 | |||

95 | private Operation IsValidNeg(SyntaxElement arg) |
||

96 | { |
||

97 | return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_SIGN_MASK); |
||

98 | } |
||

99 | |||

100 | private Operation IsValidSignedInt(SyntaxElement arg) |
||

101 | { |
||

102 | return new Operation(LogicBooleanOperation.OR, IsValidPos(arg), IsValidNeg(arg)); |
||

103 | } |
||

104 | |||

105 | public Constraint getConstraint() |
||

106 | { |
||

107 | Constraint constraint = new Constraint(); |
||

108 | |||

109 | Variable rs = new Variable("rs", BIT_VECTOR_TYPE, null); |
||

110 | constraint.addVariable(rs); |
||

111 | |||

112 | Variable rt = new Variable("rt", BIT_VECTOR_TYPE, null); |
||

113 | constraint.addVariable(rt); |
||

114 | |||

115 | |||

116 | constraint.addFormula( |
||

117 | new Formula( |
||

118 | IsValidSignedInt(rs) |
||

119 | ) |
||

120 | ); |
||

121 | |||

122 | constraint.addFormula( |
||

123 | new Formula( |
||

124 | IsValidSignedInt(rt) |
||

125 | ) |
||

126 | ); |
||

127 | |||

128 | constraint.addFormula( |
||

129 | new Formula( |
||

130 | new Operation( |
||

131 | LogicBooleanOperation.NOT, |
||

132 | IsValidSignedInt(new Operation(BitVectorOperation.BVADD, rs, rt)), |
||

133 | null |
||

134 | ) |
||

135 | ) |
||

136 | ); |
||

137 | |||

138 | constraint.addFormula( |
||

139 | new Formula( |
||

140 | new Operation(LogicBooleanOperation.NOT, new Operation(LogicBooleanOperation.EQ, rs, rt), null) |
||

141 | ) |
||

142 | ); |
||

143 | |||

144 | return constraint; |
||

145 | } |
||

146 | |||

147 | public Vector<Variable> getExpectedVariables() |
||

148 | { |
||

149 | Vector<Variable> result = new Vector<Variable>(); |
||

150 | |||

151 | result.add(new Variable("rs", BIT_VECTOR_TYPE, new BigInteger("000000009b91b193", 16))); |
||

152 | result.add(new Variable("rt", BIT_VECTOR_TYPE, new BigInteger("000000009b91b1b3", 16))); |
||

153 | |||

154 | return result; |
||

155 | } |
||

156 | } |
||

157 | </pre> |
||

158 | |||

159 | |||

160 | 3 | Andrei Tatarnikov | h1. База данных ограничений |

161 | |||

162 | База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений. |