Project

General

Profile

Overview » History » Version 5

Sergey Smolov, 12/06/2019 03:15 PM

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