Project

General

Profile

Overview » History » Version 13

Sergey Smolov, 12/06/2019 06:39 PM

1 1 Sergey Smolov
h1. Overview
2
3
{{toc}}
4
5
h2. Basic Concepts
6
7 6 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 6 Sergey Smolov
In SMT solvers, a special functional language is used to specify constraints. The library components allow to generate constructions in the "SMT-LIBv2":https://stp.readthedocs.io/en/latest/smt-input-language.html language and run solver to process them and produce the results (find values of unknown input variables).
14 1 Sergey Smolov
15
h2. Constraints and SMT
16
17 9 Sergey Smolov
Constraints (so-called _SMT model_) are represented by a set of assertions 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-LIBv2 code:
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
h3. SMT Limitations.
50
51
# *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
53
<pre>
54
(define-fun fact ((x Int)) Int (ite (= x 0) 1 (fact (- x 1))))
55
(simplify (fact 10))
56
</pre>
57
58
h3. Constraints in XML
59
60 10 Sergey Smolov
Constraints can also be described in the XML format. The library provides functionality to load and save constraints in XML. Here is an example of an XML document describing a simple constraint.
61 1 Sergey Smolov
62
<pre><code class="xml">
63
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
64
<Constraint version="1.0">
65
    <Name>SimpleBitVector</Name>
66
    <Description>SimpleBitVector constraint</Description>
67
    <Solver id="Z3_TEXT"/>
68
    <Signature>
69
        <Variable length="3" name="a" type="BIT_VECTOR" value=""/>
70
        <Variable length="3" name="b" type="BIT_VECTOR" value=""/>
71
    </Signature>
72
    <Syntax>
73
        <Formula>
74
            <Expression>
75 2 Sergey Smolov
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="NOT"/>
76 1 Sergey Smolov
                <Expression>
77 2 Sergey Smolov
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
78 1 Sergey Smolov
                    <VariableRef name="a"/>
79
                    <VariableRef name="b"/>
80
                </Expression>
81
            </Expression>
82
        </Formula>
83
        <Formula>
84
            <Expression>
85 2 Sergey Smolov
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
86 1 Sergey Smolov
                <Expression>
87 2 Sergey Smolov
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVOR"/>
88 1 Sergey Smolov
                    <VariableRef name="a"/>
89
                    <VariableRef name="b"/>
90
                </Expression>
91
                <Value length="3" type="BIT_VECTOR" value="111"/>
92
            </Expression>
93
        </Formula>
94
        <Formula>
95
            <Expression>
96 2 Sergey Smolov
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
97 1 Sergey Smolov
                <Expression>
98 2 Sergey Smolov
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVLSHL"/>
99 1 Sergey Smolov
                    <VariableRef name="a"/>
100
                    <Value length="3" type="BIT_VECTOR" value="011"/>
101
                </Expression>
102
                <Expression>
103 2 Sergey Smolov
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVSMOD"/>
104 1 Sergey Smolov
                    <VariableRef name="a"/>
105
                    <Value length="3" type="BIT_VECTOR" value="010"/>
106
                </Expression>
107
            </Expression>
108
        </Formula>
109
        <Formula>
110
            <Expression>
111 2 Sergey Smolov
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
112 1 Sergey Smolov
                <Expression>
113 2 Sergey Smolov
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVAND"/>
114 1 Sergey Smolov
                    <VariableRef name="a"/>
115
                    <VariableRef name="b"/>
116
                </Expression>
117
                <Value length="3" type="BIT_VECTOR" value="000"/>
118
            </Expression>
119
        </Formula>
120
    </Syntax>
121
</Constraint>
122
</code></pre>
123
124 10 Sergey Smolov
The same constraint described in SMT-LIBv2 looks like this:
125 1 Sergey Smolov
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
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
140
h2. Tree Representation
141
142 11 Sergey Smolov
In Fortress library context-independent syntax trees are used to represent constraints. These trees are used to generate a representation that can be understood by a particular SMT solver. The syntax tree contains nodes of the following types:
143 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.
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 11 Sergey Smolov
# *Operation* Represents an operation on some variables, values, parameters or other operations.
146 4 Sergey Smolov
# *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 1 Sergey Smolov
149
Note: Operation, Variables and Value are designed to be treated polymorphically. This allows combining them to build complex expressions.
150
151 12 Sergey Smolov
h2. Library Packages
152 1 Sergey Smolov
153 12 Sergey Smolov
The Fortress library is implemented in Java. The Java classes are organized in the following packages:
154
# ru.ispras.fortress.calculator - constant sub-expressions simplifier
155
# ru.ispras.fortress.data - data types (basic, bit vectors, arrays, etc.)
156
# ru.ispras.fortress.esexpr - Lisp-like S-expressions
157
# ru.ispras.fortress.expression - syntax tree nodes, operation identifiers
158
# ru.ispras.fortress.jaxb - XML integration
159
# ru.ispras.fortress.logic - normal form orthogonalizer
160
# ru.ispras.fortress.randomizer - randomization engine
161
# ru.ispras.fortress.solver - SMT solver integration
162
# ru.ispras.fortress.transformer - syntax tree transformation rules and mechanisms
163
# ru.ispras.fortress.util - utility methods
164 1 Sergey Smolov
165
h3. Core classes/interfaces
166
167
*Syntax Tree Implementation*
168
169
The syntax tree nodes are implemented in the following classes:
170
* Constraint. Parameterized by a collection of Variable objects and a collection of Formula objects.
171 12 Sergey Smolov
* Formulas. Parameterized by a collection of syntax tree node objects.
172
* Operation. Parameterized by operands and an operation type.
173
* Variable. Parameterized by the variable name string, a data type and a value.   
174
* Value. Parameterized by a data type and a value.
175 1 Sergey Smolov
176 12 Sergey Smolov
The current implementation supports operations with the following data types: (1) Bit vectors, (2) Booleans, (3) Integers, (4) Real numbers, (5) Arrays.
177
The code below demonstrates how we can build a syntax tree representation for the integer overflow constraint:
178 1 Sergey Smolov
179
<pre><code class="java">
180 12 Sergey Smolov
public class IntegerOverflowBitVectorTestCase extends GenericSolverTestBase {
181
  public IntegerOverflowBitVectorTestCase() {
182
    super(new IntegerOverflow());
183
  }
184 1 Sergey Smolov
185 12 Sergey Smolov
  public static class IntegerOverflow implements SampleConstraint {
186
    private static final int BIT_VECTOR_LENGTH = 64;
187
    private static final DataType BIT_VECTOR_TYPE = DataType.bitVector(BIT_VECTOR_LENGTH);
188 1 Sergey Smolov
189 12 Sergey Smolov
    private static final NodeValue INT_ZERO =
190
        new NodeValue(BIT_VECTOR_TYPE.valueOf("0", 10));
191 1 Sergey Smolov
192 12 Sergey Smolov
    private static final NodeValue INT_BASE_SIZE =
193
        new NodeValue(BIT_VECTOR_TYPE.valueOf("32", 10));
194 1 Sergey Smolov
195 12 Sergey Smolov
    private static final NodeOperation INT_SIGN_MASK =
196
        Nodes.bvlshl(Nodes.bvnot(INT_ZERO), INT_BASE_SIZE);
197 1 Sergey Smolov
198 12 Sergey Smolov
    @Override
199
    public Constraint getConstraint() {
200
      final ConstraintBuilder builder = new ConstraintBuilder();
201 1 Sergey Smolov
202 12 Sergey Smolov
      builder.setName("IntegerOverflow");
203
      builder.setKind(ConstraintKind.FORMULA_BASED);
204
      builder.setDescription("IntegerOverflow constraint");
205 1 Sergey Smolov
206 12 Sergey Smolov
      // Unknown variables
207
      final NodeVariable rs = new NodeVariable(builder.addVariable("rs", BIT_VECTOR_TYPE));
208
      final NodeVariable rt = new NodeVariable(builder.addVariable("rt", BIT_VECTOR_TYPE));
209 1 Sergey Smolov
210 12 Sergey Smolov
      final Formulas formulas = new Formulas();
211
      builder.setInnerRep(formulas);
212 1 Sergey Smolov
213 12 Sergey Smolov
      formulas.add(newIsValidSignedInt(rs));
214
      formulas.add(newIsValidSignedInt(rt));
215 1 Sergey Smolov
216 12 Sergey Smolov
      formulas.add(Nodes.not(newIsValidSignedInt(Nodes.bvadd(rs, rt))));
217
      formulas.add(Nodes.not(Nodes.eq(rs, rt)));
218 1 Sergey Smolov
219 12 Sergey Smolov
      return builder.build();
220
    }
221 1 Sergey Smolov
222 12 Sergey Smolov
    private NodeOperation newIsValidPos(final Node arg) {
223
      return Nodes.eq(Nodes.bvand(arg, INT_SIGN_MASK), INT_ZERO);
224
    }
225 1 Sergey Smolov
226 12 Sergey Smolov
    private NodeOperation newIsValidNeg(final Node arg) {
227
      return Nodes.eq(Nodes.bvand(arg, INT_SIGN_MASK), INT_SIGN_MASK);
228
    }
229
230
    private NodeOperation newIsValidSignedInt(final Node arg) {
231
      return Nodes.or(newIsValidPos(arg), newIsValidNeg(arg));
232
    }
233
234
    @Override
235
    public Iterable<Variable> getExpectedVariables() {
236
      final List<Variable> result = new ArrayList<>();
237
238
      result.add(new Variable("rs", BIT_VECTOR_TYPE.valueOf("000000009b91b193", 16)));
239
      result.add(new Variable("rt", BIT_VECTOR_TYPE.valueOf("000000009b91b1b3", 16)));
240
241
      return result;
242
    }
243
  }
244 1 Sergey Smolov
}
245
</code></pre>
246
247
*Solver Implementation*
248
249 12 Sergey Smolov
Solver implement a common interface that looks like this:
250 1 Sergey Smolov
251
<pre><code class="java">
252 13 Sergey Smolov
public interface Solver {
253 12 Sergey Smolov
  String getName();
254
  String getDescription();
255
  boolean isSupported(ConstraintKind kind);
256
  boolean isGeneric();
257
  SolverResult solve(Constraint constraint);
258
  boolean addCustomOperation(Function function);
259
  boolean addCustomOperation(FunctionTemplate template);
260
  String getSolverPath();
261
  void setSolverPath(String value);
262 1 Sergey Smolov
}
263
</code></pre>