Project

General

Profile

Wiki » History » Version 25

Sergey Smolov, 12/05/2019 06:17 PM

1 24 Sergey Smolov
h1. Fortress
2 1 Andrei Tatarnikov
3 2 Andrei Tatarnikov
h2. Basic Concepts
4 1 Andrei Tatarnikov
5 24 Sergey Smolov
Fortress provides a Java API for generating pseudorandom values that satisfy certain constraints. This feature is important for test generators that aim at creating directed tests. At logical level, a constraint is represented by a set of expressions that specify limitations for input values (assertions that must be hold for those values). If there are values satisfying all of the specified assertions they will be used a solution for the constraint. If there is a multitude of values satisfying the constraint, specific values will be selected from the range of possible solutions on random basis.
6 2 Andrei Tatarnikov
7 25 Sergey Smolov
From an implementational point of view, the API represents a wrapper around some kind of an openly distributed SMT solver engine (in the current version, we support the following solvers: "Yices":https://github.com/SRI-CSL/yices2, "Z3":https://github.com/Z3Prover/z3, "CVC4":https://cvc4.github.io). It can be extended to support other solver engines and it provides a possibility to interact with different solver engines in a uniform way. Also, it facilitates creating task-specific custom solvers and extending functionality of existing solver engines by adding custom operations (macros based on built-in operations).
8 2 Andrei Tatarnikov
9 3 Andrei Tatarnikov
h2. SMT-LIB
10 2 Andrei Tatarnikov
11
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).
12
13 1 Andrei Tatarnikov
h2. Constraints and SMT
14
15
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:
16
17 18 Andrei Tatarnikov
<pre>
18 1 Andrei Tatarnikov
(define-sort        Int_t () (_ BitVec 64))
19
20
(define-fun      INT_ZERO () Int_t (_ bv0 64))
21
(define-fun INT_BASE_SIZE () Int_t (_ bv32 64))
22
(define-fun INT_SIGN_MASK () Int_t (bvshl (bvnot INT_ZERO) INT_BASE_SIZE))
23
24
(define-fun IsValidPos ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_ZERO) true false))
25
(define-fun IsValidNeg ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_SIGN_MASK) true false))
26
(define-fun IsValidSignedInt ((x!1 Int_t)) Bool (ite (or (IsValidPos x!1) (IsValidNeg x!1)) true false))
27
28
(declare-const rs Int_t)
29
(declare-const rt Int_t)
30
31
; rt and rs must contain valid sign-extended 32-bit values (bits 63..31 equal)
32
(assert (IsValidSignedInt rs))
33
(assert (IsValidSignedInt rt))
34
35
; the condition for an overflow: the summation result is not a valid sign-extended 32-bit value
36
(assert (not (IsValidSignedInt (bvadd rs rt))))
37
38
; just in case: rs and rt are not equal (to make the results more interesting)
39
(assert (not (= rs rt)))
40
41
(check-sat)
42
43
(echo "Values that lead to an overflow:")
44
(get-value (rs rt))
45 18 Andrei Tatarnikov
</pre>
46 1 Andrei Tatarnikov
47 5 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.
48
49 9 Sergey Smolov
h3. SMT Limitations.
50 5 Andrei Tatarnikov
51 8 Andrei Tatarnikov
# *Recursion in not allowed* in SMT-LIB. At least, this applies to the Z3 implementation. In other words, code like provided below is not valid:
52 5 Andrei Tatarnikov
53
<pre>
54
(define-fun fact ((x Int)) Int (ite (= x 0) 1 (fact (- x 1))))
55
(simplify (fact 10))
56
</pre>
57 1 Andrei Tatarnikov
58 12 Andrei Tatarnikov
h3. Constraints in XML
59
60 20 Andrei Tatarnikov
Constraints can also be described in the XML format. The API provides functionality to load and save constraints in XML. Here is an example of an XML document describing a simple constraint.
61 19 Andrei Tatarnikov
62 15 Andrei Tatarnikov
<pre><code class="xml">
63 12 Andrei Tatarnikov
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
64 1 Andrei Tatarnikov
<Constraint version="1.0">
65 16 Andrei Tatarnikov
    <Name>SimpleBitVector</Name>
66
    <Description>SimpleBitVector constraint</Description>
67 13 Andrei Tatarnikov
    <Solver id="Z3_TEXT"/>
68 1 Andrei Tatarnikov
    <Signature>
69 16 Andrei Tatarnikov
        <Variable length="3" name="a" type="BIT_VECTOR" value=""/>
70
        <Variable length="3" name="b" type="BIT_VECTOR" value=""/>
71 13 Andrei Tatarnikov
    </Signature>
72 1 Andrei Tatarnikov
    <Syntax>
73 12 Andrei Tatarnikov
        <Formula>
74 13 Andrei Tatarnikov
            <Expression>
75 16 Andrei Tatarnikov
                <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="NOT"/>
76 1 Andrei Tatarnikov
                <Expression>
77 16 Andrei Tatarnikov
                    <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="EQ"/>
78
                    <VariableRef name="a"/>
79 1 Andrei Tatarnikov
                    <VariableRef name="b"/>
80
                </Expression>
81
            </Expression>
82 12 Andrei Tatarnikov
        </Formula>
83 1 Andrei Tatarnikov
        <Formula>
84
            <Expression>
85
                <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="EQ"/>
86 13 Andrei Tatarnikov
                <Expression>
87 16 Andrei Tatarnikov
                    <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="BVOR"/>
88
                    <VariableRef name="a"/>
89
                    <VariableRef name="b"/>
90 1 Andrei Tatarnikov
                </Expression>
91 16 Andrei Tatarnikov
                <Value length="3" type="BIT_VECTOR" value="111"/>
92 13 Andrei Tatarnikov
            </Expression>
93 12 Andrei Tatarnikov
        </Formula>
94 13 Andrei Tatarnikov
        <Formula>
95
            <Expression>
96 16 Andrei Tatarnikov
                <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="EQ"/>
97 12 Andrei Tatarnikov
                <Expression>
98 16 Andrei Tatarnikov
                    <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="BVLSHL"/>
99
                    <VariableRef name="a"/>
100
                    <Value length="3" type="BIT_VECTOR" value="011"/>
101 12 Andrei Tatarnikov
                </Expression>
102 16 Andrei Tatarnikov
                <Expression>
103
                    <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="BVSMOD"/>
104
                    <VariableRef name="a"/>
105
                    <Value length="3" type="BIT_VECTOR" value="010"/>
106
                </Expression>
107 13 Andrei Tatarnikov
            </Expression>
108
        </Formula>
109 12 Andrei Tatarnikov
        <Formula>
110 13 Andrei Tatarnikov
            <Expression>
111 16 Andrei Tatarnikov
                <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="EQ"/>
112
                <Expression>
113
                    <Operation family="ru.ispras.solver.core.syntax.EStandardOperation" id="BVAND"/>
114
                    <VariableRef name="a"/>
115
                    <VariableRef name="b"/>
116
                </Expression>
117
                <Value length="3" type="BIT_VECTOR" value="000"/>
118 12 Andrei Tatarnikov
            </Expression>
119 1 Andrei Tatarnikov
        </Formula>
120 12 Andrei Tatarnikov
    </Syntax>
121 14 Andrei Tatarnikov
</Constraint>
122 15 Andrei Tatarnikov
</code></pre>
123 1 Andrei Tatarnikov
124 21 Andrei Tatarnikov
The same constraint described in SMT-LIB looks like this:
125
126
<pre>
127
(declare-const a (_ BitVec 3))
128
(declare-const b (_ BitVec 3))
129
(assert (not (= a b)))
130
(assert (= (bvor a b) #b111))
131
(assert (= (bvand a b) #b000))
132
(assert (= (bvshl a (_ bv3 3))(bvsmod a (_ bv2 3))))
133
(check-sat)
134
(get-value (a b))
135
(exit)
136
</pre>
137
138 23 Andrei Tatarnikov
As it can be noticed, the description in XML is more redundant. However, this format is independent of a particular solver engine and can be extended with additional information.
139 22 Andrei Tatarnikov
140 1 Andrei Tatarnikov
h2. Tree Representation
141
142
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:
143
# 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.
144
# 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.
145
# Operation. Represents an unary or binary operation with some unknown variable, some value or some expression as parameters.
146
# 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.
147
# Value. Specifies some known value of the specified type which can be accessed as an attribute.
148
149
Note: Operation, Variables and Value are designed to be treated polymorphically. This allows combining them to build complex expressions.
150
151
h2. Constraint Solver Java Library
152
153
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:
154
# ru.ispras.microtesk.constraints - contains SMT model generation logic and solver implementations.
155
# ru.ispras.microtesk.constraints.syntax - contains classes implementing syntax tree nodes.
156
# ru.ispras.microtesk.constraints.syntax.types - contains code that specifies particular data types and operation types.
157
# ru.ispras.microtesk.constraints.tests - contains JUnit test cases.
158
159
h3. Core classes/interfaces
160
161
*Syntax Tree Implementation*
162
163
The syntax tree nodes are implemented in the following classes:
164
* Constraint. Parameterized by a collection of Variable objects and a collection of Formula objects.
165
* Formula. Parameterized by an Operation object.
166
* Operation. Implements SyntaxElement. Parameterized by operand objects implementing SyntaxElement and an operation type object implementing OperationType.
167
* Variable. Implements SyntaxElement. Parameterized by the variable name string, a data type object implemeting DataType and a BigInteger value object.   
168
* Value. Implements SyntaxElement. Parameterized a data type object implemeting DataType and a BigInteger value object.
169
170
The SyntaxElement interface provides the ability to combine different kinds of elements into expressions.
171
172 10 Alexander Kamkin
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:
173 1 Andrei Tatarnikov
174
<pre><code class="java">
175
public final class LogicBooleanOperation extends OperationType
176
{
177
	private LogicBooleanOperation() {}
178
	
179
	/** Operation: Logic - Equality */
180
	public static final OperationType EQ = new LogicBooleanOperation();
181
	/** Operation: Logic - AND */
182
	public static final OperationType AND = new LogicBooleanOperation();
183
	/** Operation: Logic - OR */
184
	public static final OperationType OR  = new LogicBooleanOperation();
185
	/** Operation: Logic - NOT */
186
	public static final OperationType NOT = new LogicBooleanOperation();
187
	/** Operation: Logic - XOR */
188
	public static final OperationType XOR = new LogicBooleanOperation();
189
	/** Operation: Logic - Implication */
190 10 Alexander Kamkin
	public static final OperationType IMPL= new LogicBooleanOperation();
191 1 Andrei Tatarnikov
} 
192
</code></pre>
193
194 10 Alexander Kamkin
The code below demonstrates how we can build a syntax tree representation for the integer overflow constraint:
195 1 Andrei Tatarnikov
196
<pre><code class="java">
197
class BitVectorIntegerOverflowTestCase implements SolverTestCase
198
{
199
	private static final int      BIT_VECTOR_LENGTH = 64;
200
	private static final DataType   BIT_VECTOR_TYPE = DataType.getBitVector(BIT_VECTOR_LENGTH);
201
	private static final Value             INT_ZERO = new Value(new BigInteger("0"), BIT_VECTOR_TYPE);
202
	private static final Value        INT_BASE_SIZE = new Value(new BigInteger("32"), BIT_VECTOR_TYPE);
203
204
	private static final Operation    INT_SIGN_MASK =
205
		new Operation(BitVectorOperation.BVSHL, new Operation(BitVectorOperation.BVNOT, INT_ZERO, null), INT_BASE_SIZE);
206
	
207
	private Operation IsValidPos(SyntaxElement arg)
208
	{
209
		return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_ZERO);
210
	}
211
	
212
	private Operation IsValidNeg(SyntaxElement arg)
213
	{
214
		return new Operation(LogicBooleanOperation.EQ, new Operation(BitVectorOperation.BVAND, arg, INT_SIGN_MASK), INT_SIGN_MASK);
215
	}
216
	
217
	private Operation IsValidSignedInt(SyntaxElement arg)
218
	{
219
		return new Operation(LogicBooleanOperation.OR, IsValidPos(arg), IsValidNeg(arg));
220
	}
221
	
222
	public Constraint getConstraint()
223
	{
224
		Constraint constraint = new Constraint();
225
		
226
		Variable rs = new Variable("rs", BIT_VECTOR_TYPE, null);
227
		constraint.addVariable(rs);
228
		
229
		Variable rt = new Variable("rt", BIT_VECTOR_TYPE, null);
230
		constraint.addVariable(rt);
231
		
232
		
233
		constraint.addFormula(
234
			new Formula(
235
				IsValidSignedInt(rs)
236
			)
237
		);
238
		
239
		constraint.addFormula(
240
			new Formula(
241
				IsValidSignedInt(rt)
242
			)
243
		);
244
245
		constraint.addFormula(
246
			new Formula(
247
				new Operation(
248
					LogicBooleanOperation.NOT,
249
					IsValidSignedInt(new Operation(BitVectorOperation.BVADD, rs, rt)),
250
					null
251
				) 
252
			)
253
		);
254
255
		constraint.addFormula(
256
			new Formula(
257
				new Operation(LogicBooleanOperation.NOT, new Operation(LogicBooleanOperation.EQ, rs, rt), null)
258
			)
259
		);
260
261
		return constraint;
262
	}
263
	
264
	public Vector<Variable> getExpectedVariables()	
265
	{
266
		Vector<Variable> result = new Vector<Variable>();
267
		
268
		result.add(new Variable("rs", BIT_VECTOR_TYPE, new BigInteger("000000009b91b193", 16)));
269
		result.add(new Variable("rt", BIT_VECTOR_TYPE, new BigInteger("000000009b91b1b3", 16)));
270
		
271
		return result;	
272 10 Alexander Kamkin
	}
273 1 Andrei Tatarnikov
}
274
</code></pre>
275
276
*Representation Translation*
277
278 10 Alexander Kamkin
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:
279 1 Andrei Tatarnikov
280
<pre><code class="java">
281
public interface RepresentationBuilder
282
{	
283
	public void addVariableDeclaration(Variable variable);
284
285
	public void beginConstraint();
286
	public void endConstraint();
287
288
	public void beginFormula();
289
	public void endFormula();
290
291
	public void beginExpression();
292
	public void endExpression();
293
294
	public void appendValue(Value value);
295
	public void appendVariable(Variable variable);
296 10 Alexander Kamkin
	public void appendOperation(OperationType type);
297 1 Andrei Tatarnikov
}
298
</code></pre>
299
300
*Solver Implementation*
301
302 10 Alexander Kamkin
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:
303 1 Andrei Tatarnikov
304
<pre><code class="java">
305
public interface Solver
306
{
307
	public boolean solveConstraint(Constraint constraint);
308
	
309
	public boolean isSolved();
310
	public boolean isSatisfiable();
311
	
312
	public int getErrorCount();
313
	public String getErrorText(int index);
314
	
315
	public int getVariableCount();
316 10 Alexander Kamkin
	public Variable getVariable(int index);
317 1 Andrei Tatarnikov
}
318
</code></pre>