Project

General

Profile

Constraint Database » History » Version 2

Alexander Kamkin, 04/12/2012 10:54 AM

1 1 Alexander Kamkin
h1. Constraint Database
2
3 2 Alexander Kamkin
Constraint database (also known as testing knowledge) is built automatically by analyzing the formal ISA specifications being written in an architecture description language (ADL), e.g. in nML or Sim-nML. Some constraints (test situations) can be described manually and added in to the constraint database.
4 1 Alexander Kamkin
5
h1. Constraint Solver
6
7
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.
8
9
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).
10
11
h2. Constraints and SMT
12
13
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:
14
15
<pre>
16
(define-sort        Int_t () (_ BitVec 64))
17
18
(define-fun      INT_ZERO () Int_t (_ bv0 64))
19
(define-fun INT_BASE_SIZE () Int_t (_ bv32 64))
20
(define-fun INT_SIGN_MASK () Int_t (bvshl (bvnot INT_ZERO) INT_BASE_SIZE))
21
22
(define-fun IsValidPos ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_ZERO) true false))
23
(define-fun IsValidNeg ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_SIGN_MASK) true false))
24
(define-fun IsValidSignedInt ((x!1 Int_t)) Bool (ite (or (IsValidPos x!1) (IsValidNeg x!1)) true false))
25
26
(declare-const rs Int_t)
27
(declare-const rt Int_t)
28
29
; rt and rs must contain valid sign-extended 32-bit values (bits 63..31 equal)
30
(assert (IsValidSignedInt rs))
31
(assert (IsValidSignedInt rt))
32
33
; the condition for an overflow: the summation result is not a valid sign-extended 32-bit value
34
(assert (not (IsValidSignedInt (bvadd rs rt))))
35
36
; just in case: rs and rt are not equal (to make the results more interesting)
37
(assert (not (= rs rt)))
38
39
(check-sat)
40
41
(echo "Values that lead to an overflow:")
42
(get-value (rs rt))
43
</pre>
44
45
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.   
46
47
h2. Tree Representation
48
49
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:
50
# 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.
51
# 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.
52
# Operation. Represents an unary or binary operation with some unknown variable, some value or some expression as parameters.
53
# 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.
54
# Value. Specifies some known value of the specified type which can be accessed as an attribute.
55
56
Note: Operation, Variables and Value are designed to be treated polymorphically. This allows combining them to build complex expressions.
57
58
h2. Constraint Solver Java Library
59
60
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:
61
# ru.ispras.microtesk.constraints - contains SMT model generation logic and solver implementations.
62
# ru.ispras.microtesk.constraints.syntax - contains classes implementing syntax tree nodes.
63
# ru.ispras.microtesk.constraints.syntax.types - contains code that specifies particular data types and operation types.
64
# ru.ispras.microtesk.constraints.tests - contains JUnit test cases.
65
66
h3. Core classes/interfaces
67
68
*Syntax Tree Implementation*
69
70
The syntax tree nodes are implemented in the following classes:
71
* Constraint. Parameterized by a collection of Variable objects and a collection of Formula objects.
72
* Formula. Parameterized by an Operation object.
73
* Operation. Implements SyntaxElement. Parameterized by operand objects implementing SyntaxElement and an operation type object implementing OperationType.
74
* Variable. Implements SyntaxElement. Parameterized by the variable name string, a data type object implemeting DataType and a BigInteger value object.   
75
* Value. Implements SyntaxElement. Parameterized a data type object implemeting DataType and a BigInteger value object.
76
77
The SyntaxElement interface provides the ability to combine different kinds of elements into expressions.
78
79
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:
80
81
<pre>
82
public final class LogicBooleanOperation extends OperationType
83
{
84
	private LogicBooleanOperation() {}
85
	
86
	/** Operation: Logic - Equality */
87
	public static final OperationType EQ = new LogicBooleanOperation();
88
	/** Operation: Logic - AND */
89
	public static final OperationType AND = new LogicBooleanOperation();
90
	/** Operation: Logic - OR */
91
	public static final OperationType OR  = new LogicBooleanOperation();
92
	/** Operation: Logic - NOT */
93
	public static final OperationType NOT = new LogicBooleanOperation();
94
	/** Operation: Logic - XOR */
95
	public static final OperationType XOR = new LogicBooleanOperation();
96
	/** Operation: Logic - Implication */
97
	public static final OperationType IMPL= new LogicBooleanOperation();
98
} 
99
</pre>
100
101
The code below demonstrates how we can build a syntax tree representation for the integer overflow constraint:
102
103
<pre>
104
class BitVectorIntegerOverflowTestCase implements SolverTestCase
105
{
106
	private static final int      BIT_VECTOR_LENGTH = 64;
107
	private static final DataType   BIT_VECTOR_TYPE = DataType.getBitVector(BIT_VECTOR_LENGTH);
108
	private static final Value             INT_ZERO = new Value(new BigInteger("0"), BIT_VECTOR_TYPE);
109
	private static final Value        INT_BASE_SIZE = new Value(new BigInteger("32"), BIT_VECTOR_TYPE);
110
111
	private static final Operation    INT_SIGN_MASK =
112
		new Operation(BitVectorOperation.BVSHL, new Operation(BitVectorOperation.BVNOT, INT_ZERO, null), INT_BASE_SIZE);
113
	
114
	private Operation IsValidPos(SyntaxElement arg)
115
	{
116
		return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_ZERO);
117
	}
118
	
119
	private Operation IsValidNeg(SyntaxElement arg)
120
	{
121
		return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_SIGN_MASK);
122
	}
123
	
124
	private Operation IsValidSignedInt(SyntaxElement arg)
125
	{
126
		return new Operation(LogicBooleanOperation.OR, IsValidPos(arg), IsValidNeg(arg));
127
	}
128
	
129
	public Constraint getConstraint()
130
	{
131
		Constraint constraint = new Constraint();
132
		
133
		Variable rs = new Variable("rs", BIT_VECTOR_TYPE, null);
134
		constraint.addVariable(rs);
135
		
136
		Variable rt = new Variable("rt", BIT_VECTOR_TYPE, null);
137
		constraint.addVariable(rt);
138
		
139
		
140
		constraint.addFormula(
141
			new Formula(
142
				IsValidSignedInt(rs)
143
			)
144
		);
145
		
146
		constraint.addFormula(
147
			new Formula(
148
				IsValidSignedInt(rt)
149
			)
150
		);
151
152
		constraint.addFormula(
153
			new Formula(
154
				new Operation(
155
					LogicBooleanOperation.NOT,
156
					IsValidSignedInt(new Operation(BitVectorOperation.BVADD, rs, rt)),
157
					null
158
				) 
159
			)
160
		);
161
162
		constraint.addFormula(
163
			new Formula(
164
				new Operation(LogicBooleanOperation.NOT, new Operation(LogicBooleanOperation.EQ, rs, rt), null)
165
			)
166
		);
167
168
		return constraint;
169
	}
170
	
171
	public Vector<Variable> getExpectedVariables()	
172
	{
173
		Vector<Variable> result = new Vector<Variable>();
174
		
175
		result.add(new Variable("rs", BIT_VECTOR_TYPE, new BigInteger("000000009b91b193", 16)));
176
		result.add(new Variable("rt", BIT_VECTOR_TYPE, new BigInteger("000000009b91b1b3", 16)));
177
		
178
		return result;	
179
	}
180
}
181
</pre>
182
183
*Representation Translation*
184
185
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:
186
187
<pre>
188
public interface RepresentationBuilder
189
{	
190
	public void addVariableDeclaration(Variable variable);
191
192
	public void beginConstraint();
193
	public void endConstraint();
194
195
	public void beginFormula();
196
	public void endFormula();
197
198
	public void beginExpression();
199
	public void endExpression();
200
201
	public void appendValue(Value value);
202
	public void appendVariable(Variable variable);
203
	public void appendOperation(OperationType type);
204
}
205
</pre>
206
207
*Solver Implementation*
208
209
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:
210
211
<pre>
212
public interface Solver
213
{
214
	public boolean solveConstraint(Constraint constraint);
215
	
216
	public boolean isSolved();
217
	public boolean isSatisfiable();
218
	
219
	public int getErrorCount();
220
	public String getErrorText(int index);
221
	
222
	public int getVariableCount();
223
	public Variable getVariable(int index);
224
}
225
</pre>