Project

General

Profile

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

Andrei Tatarnikov, 12/22/2011 10:05 AM

1 3 Andrei Tatarnikov
h1. Constraint Solver
2 1 Alexander Kamkin
3 43 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. The solver calculates 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 1 Alexander Kamkin
h2. Constraints and Satisfiability Modulo Theories (SMT)
8 44 Andrei Tatarnikov
9 45 Andrei Tatarnikov
A model in SMT is represented by a set of assertions (folmulas) that must be satisfied. An SMT solver checks the satisfiability of the model and suggests a solution (input variable values) that would satisfy the model. In the example below, we specify a model that should help us find values of the rs and rt general purpose registers that will cause the ADD instruction (for a MIPS processor) to raise an integer overflow exception. 
10
11
12
that conditions that   
13 44 Andrei Tatarnikov
14
For example, the script below 
15 43 Andrei Tatarnikov
16
<pre>
17
(define-sort        Int_t () (_ BitVec 64))
18
19
(define-fun      INT_ZERO () Int_t (_ bv0 64))
20
(define-fun INT_BASE_SIZE () Int_t (_ bv32 64))
21
(define-fun INT_SIGN_MASK () Int_t (bvshl (bvnot INT_ZERO) INT_BASE_SIZE))
22
23
(define-fun IsValidPos ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_ZERO) true false))
24
(define-fun IsValidNeg ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_SIGN_MASK) true false))
25
(define-fun IsValidSignedInt ((x!1 Int_t)) Bool (ite (or (IsValidPos x!1) (IsValidNeg x!1)) true false))
26
27
(declare-const rs Int_t)
28
(declare-const rt Int_t)
29
30
; rt and rs must contain valid sign-extended 32-bit values (bits 63..31 equal)
31
(assert (IsValidSignedInt rs))
32
(assert (IsValidSignedInt rt))
33
34
; the condition for an overflow: the summation result is not a valid sign-extended 32-bit value
35
(assert (not (IsValidSignedInt (bvadd rs rt))))
36
37
; just in case: rs and rt are not equal (to make the results more interesting)
38
(assert (not (= rs rt)))
39
40
(check-sat)
41
42
(echo "Values that lead to an overflow:")
43
(get-value (rs rt))
44
</pre>
45
46 35 Andrei Tatarnikov
47
<pre>
48 42 Andrei Tatarnikov
; Finds an integer represented in the form of a bit vector
49
; that would satisfy the following constraints:
50 41 Andrei Tatarnikov
;
51 42 Andrei Tatarnikov
; - it lies within the range from 100 to 200
52 41 Andrei Tatarnikov
; - it can be represented as a power of two
53
;
54
; The value we look for is 128 (or 0x80).
55
;
56
; Expected output:
57
;   sat ((x #x00000080))
58 35 Andrei Tatarnikov
59
(declare-const x (_ BitVec 32))
60
(assert (bvugt x (_ bv100 32)))
61
(assert (bvult x (_ bv200 32)))
62
(assert (= (bvand x (bvsub x (_ bv1 32))) (_ bv0 32)))
63
(check-sat)
64
(get-value (x))
65
(exit)
66
</pre>
67
68 18 Andrei Tatarnikov
h2. Syntax trees
69
70 9 Andrei Tatarnikov
We use language-independent syntax trees to represent constraints. These trees then are processed to generate a representation that can be understood by a particular SMT solver. The syntax tree contains the following node types:
71 13 Andrei Tatarnikov
# Constraint. This is the root node of the tree. It holds the list of unknown variables and the list of limitations for these variables.
72 21 Andrei Tatarnikov
# Formula. Represents a limitation expression. Can be combined with other limitations to build a more complex limitation (by applying a logic OR, AND or NOT to it). The underlying expression must be a logic expression that can be solved to true or false.
73 13 Andrei Tatarnikov
# Operation. Represents an unary or binary operation with some unknown variable, some value or some expression as parameters.
74 14 Andrei Tatarnikov
# Variable.Represents an input variable. It can have an assigned value and, in such case, will be treated as a value. Otherwise, it is an unknown variable. A variable includes a type as an attribute.
75
# Value. Specifies some known value of the specified type which can be accessed as an attribute.
76 17 Andrei Tatarnikov
77 16 Andrei Tatarnikov
Note: Operation, Variables and Value can be treated polymorphically as syntax elements (SyntaxElement). This allows combining them to build complex expressions.
78 1 Alexander Kamkin
79 24 Andrei Tatarnikov
The current implementation supports operations with the following data types:
80 26 Andrei Tatarnikov
# Bit vectors
81
# Booleans
82 16 Andrei Tatarnikov
83 22 Andrei Tatarnikov
h2. Constraint Solver Java Library
84 3 Andrei Tatarnikov
85 28 Andrei Tatarnikov
The source code files of the Constraint Solver subsystem are located in the "microtesk++/constraint-solver" folder. The java classes are organized in the following packages:
86 32 Andrei Tatarnikov
# ru.ispras.microtesk.constraints - contains SMT representation generation logic and solver implementations.
87
# ru.ispras.microtesk.constraints.syntax - contains classes implementing syntax tree nodes.
88
# ru.ispras.microtesk.constraints.syntax.types - contains code that specifies particular data types and operation types.
89 29 Andrei Tatarnikov
# ru.ispras.microtesk.constraints.tests - contains JUnit test cases.
90 28 Andrei Tatarnikov
91 3 Andrei Tatarnikov
92
h1. База данных ограничений
93
94
База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений.