База данных ограничений » History » Revision 41
Revision 40 (Andrei Tatarnikov, 12/21/2011 03:57 PM) → Revision 41/91 (Andrei Tatarnikov, 12/21/2011 04:02 PM)
h1. Constraint Solver 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 finds values of input variables which will violate the limitations if there are any such values. The subsystem uses a 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). h2. Constraints and Satisfiability Modulo Theories (SMT) <pre> ; Finds ;Finds an integer represented in the form of bit vector ; that would satisfy the following constraint: ; ; - it lies within the in the range 100 to 200 ; - it can be represented as a power of two ; ; The value we look for is 128 (or 0x80). ; ; Expected ;Expected output: ; sat ;sat ((x #x00000080)) (declare-const x (_ BitVec 32)) (assert (bvugt x (_ bv100 32))) (assert (bvult x (_ bv200 32))) (assert (= (bvand x (bvsub x (_ bv1 32))) (_ bv0 32))) (check-sat) (get-value (x)) (exit) </pre> h2. Syntax trees 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: # Constraint. This is the root node of the tree. It holds the list of unknown variables and the list of limitations for these variables. # 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. # Operation. Represents an unary or binary operation with some unknown variable, some value or some expression as parameters. # 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. # Value. Specifies some known value of the specified type which can be accessed as an attribute. Note: Operation, Variables and Value can be treated polymorphically as syntax elements (SyntaxElement). This allows combining them to build complex expressions. The current implementation supports operations with the following data types: # Bit vectors # Booleans h2. Constraint Solver Java Library 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: # ru.ispras.microtesk.constraints - contains SMT representation generation logic and solver implementations. # ru.ispras.microtesk.constraints.syntax - contains classes implementing syntax tree nodes. # ru.ispras.microtesk.constraints.syntax.types - contains code that specifies particular data types and operation types. # ru.ispras.microtesk.constraints.tests - contains JUnit test cases. h1. База данных ограничений База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений.