Project

General

Profile

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

Alexander Kamkin, 04/12/2012 10:42 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 86 Andrei Tatarnikov
h2. Constraints and 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 85 Andrei Tatarnikov
*Syntax Tree Implementation*
65 79 Andrei Tatarnikov
66 70 Andrei Tatarnikov
The syntax tree nodes are implemented in the following classes:
67 74 Andrei Tatarnikov
* Constraint. Parameterized by a collection of Variable objects and a collection of Formula objects.
68 72 Andrei Tatarnikov
* Formula. Parameterized by an Operation object.
69
* Operation. Implements SyntaxElement. Parameterized by operand objects implementing SyntaxElement and an operation type object implementing OperationType.
70 75 Andrei Tatarnikov
* Variable. Implements SyntaxElement. Parameterized by the variable name string, a data type object implemeting DataType and a BigInteger value object.   
71 74 Andrei Tatarnikov
* Value. Implements SyntaxElement. Parameterized a data type object implemeting DataType and a BigInteger value object.
72 71 Andrei Tatarnikov
73
The SyntaxElement interface provides the ability to combine different kinds of elements into expressions.
74 72 Andrei Tatarnikov
75 78 Andrei Tatarnikov
The current implementation supports operations with the following data types: (1) Bit vectors, (2) Booleans. They are implemented in the BitVector and LogicBoolean classes. The BitVectorOperation and LogicBooleanOperation classes specify supported operation with these types. For example, the LogicBooleanOperation class looks like this:
76 1 Alexander Kamkin
77 91 Alexander Kamkin
<pre>
78 76 Andrei Tatarnikov
public final class LogicBooleanOperation extends OperationType
79
{
80
	private LogicBooleanOperation() {}
81
	
82
	/** Operation: Logic - Equality */
83
	public static final OperationType EQ = new LogicBooleanOperation();
84
	/** Operation: Logic - AND */
85
	public static final OperationType AND = new LogicBooleanOperation();
86
	/** Operation: Logic - OR */
87
	public static final OperationType OR  = new LogicBooleanOperation();
88
	/** Operation: Logic - NOT */
89
	public static final OperationType NOT = new LogicBooleanOperation();
90
	/** Operation: Logic - XOR */
91
	public static final OperationType XOR = new LogicBooleanOperation();
92
	/** Operation: Logic - Implication */
93
	public static final OperationType IMPL= new LogicBooleanOperation();
94 90 Alexander Kamkin
} 
95 91 Alexander Kamkin
</pre>
96 73 Andrei Tatarnikov
97
The code below demonstrates how we can build a syntax tree representation for the integer overflow constraint:
98 61 Andrei Tatarnikov
99
<pre>
100
class BitVectorIntegerOverflowTestCase implements SolverTestCase
101
{
102 65 Andrei Tatarnikov
	private static final int      BIT_VECTOR_LENGTH = 64;
103
	private static final DataType   BIT_VECTOR_TYPE = DataType.getBitVector(BIT_VECTOR_LENGTH);
104
	private static final Value             INT_ZERO = new Value(new BigInteger("0"), BIT_VECTOR_TYPE);
105
	private static final Value        INT_BASE_SIZE = new Value(new BigInteger("32"), BIT_VECTOR_TYPE);
106
107
	private static final Operation    INT_SIGN_MASK =
108
		new Operation(BitVectorOperation.BVSHL, new Operation(BitVectorOperation.BVNOT, INT_ZERO, null), INT_BASE_SIZE);
109 61 Andrei Tatarnikov
	
110
	private Operation IsValidPos(SyntaxElement arg)
111
	{
112
		return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_ZERO);
113
	}
114
	
115
	private Operation IsValidNeg(SyntaxElement arg)
116
	{
117
		return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_SIGN_MASK);
118
	}
119
	
120
	private Operation IsValidSignedInt(SyntaxElement arg)
121
	{
122
		return new Operation(LogicBooleanOperation.OR, IsValidPos(arg), IsValidNeg(arg));
123
	}
124
	
125
	public Constraint getConstraint()
126
	{
127
		Constraint constraint = new Constraint();
128
		
129
		Variable rs = new Variable("rs", BIT_VECTOR_TYPE, null);
130
		constraint.addVariable(rs);
131
		
132
		Variable rt = new Variable("rt", BIT_VECTOR_TYPE, null);
133
		constraint.addVariable(rt);
134
		
135
		
136
		constraint.addFormula(
137
			new Formula(
138
				IsValidSignedInt(rs)
139
			)
140
		);
141
		
142
		constraint.addFormula(
143
			new Formula(
144
				IsValidSignedInt(rt)
145
			)
146
		);
147
148
		constraint.addFormula(
149
			new Formula(
150
				new Operation(
151
					LogicBooleanOperation.NOT,
152
					IsValidSignedInt(new Operation(BitVectorOperation.BVADD, rs, rt)),
153
					null
154
				) 
155
			)
156
		);
157
158
		constraint.addFormula(
159
			new Formula(
160
				new Operation(LogicBooleanOperation.NOT, new Operation(LogicBooleanOperation.EQ, rs, rt), null)
161
			)
162
		);
163
164
		return constraint;
165
	}
166
	
167
	public Vector<Variable> getExpectedVariables()	
168
	{
169
		Vector<Variable> result = new Vector<Variable>();
170
		
171
		result.add(new Variable("rs", BIT_VECTOR_TYPE, new BigInteger("000000009b91b193", 16)));
172
		result.add(new Variable("rt", BIT_VECTOR_TYPE, new BigInteger("000000009b91b1b3", 16)));
173
		
174
		return result;	
175
	}
176
}
177
</pre>
178
179 82 Andrei Tatarnikov
*Representation Translation*
180
181 83 Andrei Tatarnikov
The logic that translates a tree representation into an SMT representation is implemented in the following way: Methods of the Translator class traverse the constraint syntax tree and use methods of the RepresentationBuilder interface to translate information about its nodes into a representation that can be understood by a particular solver. The RepresentationBuilder interface looks like follows:
182
183
<pre>
184
public interface RepresentationBuilder
185
{	
186
	public void addVariableDeclaration(Variable variable);
187
188
	public void beginConstraint();
189
	public void endConstraint();
190
191
	public void beginFormula();
192
	public void endFormula();
193
194
	public void beginExpression();
195
	public void endExpression();
196
197
	public void appendValue(Value value);
198
	public void appendVariable(Variable variable);
199
	public void appendOperation(OperationType type);
200
}
201 84 Andrei Tatarnikov
</pre>
202 1 Alexander Kamkin
203 84 Andrei Tatarnikov
*Solver Implementation*
204
205 88 Andrei Tatarnikov
Solvers use the Translator class and a specific implementation of the RepresentationBuilder interface to generate an SMT representation of a constraint. Then they run a solver engine to solve the constraint and produce the results. Solver implement a common interface called Solver that looks like this:
206
207 84 Andrei Tatarnikov
<pre>
208
public interface Solver
209
{
210
	public boolean solveConstraint(Constraint constraint);
211
	
212
	public boolean isSolved();
213
	public boolean isSatisfiable();
214
	
215 87 Andrei Tatarnikov
	public int getErrorCount();
216 89 Andrei Tatarnikov
	public String getErrorText(int index);
217 84 Andrei Tatarnikov
	
218
	public int getVariableCount();
219 87 Andrei Tatarnikov
	public Variable getVariable(int index);
220 84 Andrei Tatarnikov
}
221
</pre>
222 61 Andrei Tatarnikov
223 3 Andrei Tatarnikov
h1. База данных ограничений
224
225
База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений.