Overview¶

• Table of contents
• Overview
  • Basic Concepts
  • SMT-LIB
  • Constraints and SMT
    • SMT Limitations.
    • Constraints in XML
  • Tree Representation
  • Library Packages
    • Core classes/interfaces

Basic Concepts¶

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.

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, Z3, CVC4). 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).

SMT-LIB¶

In SMT solvers, a special functional language is used to specify constraints. The library components allow to generate constructions in the SMT-LIBv2 language and run solver to process them and produce the results (find values of unknown input variables).

Constraints and SMT¶

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:

(define-sort        Int_t () (_ BitVec 64))

(define-fun      INT_ZERO () Int_t (_ bv0 64))
(define-fun INT_BASE_SIZE () Int_t (_ bv32 64))
(define-fun INT_SIGN_MASK () Int_t (bvshl (bvnot INT_ZERO) INT_BASE_SIZE))

(define-fun IsValidPos ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_ZERO) true false))
(define-fun IsValidNeg ((x!1 Int_t)) Bool (ite (= (bvand x!1 INT_SIGN_MASK) INT_SIGN_MASK) true false))
(define-fun IsValidSignedInt ((x!1 Int_t)) Bool (ite (or (IsValidPos x!1) (IsValidNeg x!1)) true false))

(declare-const rs Int_t)
(declare-const rt Int_t)

; rt and rs must contain valid sign-extended 32-bit values (bits 63..31 equal)
(assert (IsValidSignedInt rs))
(assert (IsValidSignedInt rt))

; the condition for an overflow: the summation result is not a valid sign-extended 32-bit value
(assert (not (IsValidSignedInt (bvadd rs rt))))

; just in case: rs and rt are not equal (to make the results more interesting)
(assert (not (= rs rt)))

(check-sat)

(echo "Values that lead to an overflow:")
(get-value (rs rt))

SMT Limitations.¶

1. 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:

(define-fun fact ((x Int)) Int (ite (= x 0) 1 (fact (- x 1))))
(simplify (fact 10))

Constraints in XML¶

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.

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<Constraint version="1.0">
    <Name>SimpleBitVector</Name>
    <Description>SimpleBitVector constraint</Description>
    <Solver id="Z3_TEXT"/>
    <Signature>
        <Variable length="3" name="a" type="BIT_VECTOR" value=""/>
        <Variable length="3" name="b" type="BIT_VECTOR" value=""/>
    </Signature>
    <Syntax>
        <Formula>
            <Expression>
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="NOT"/>
                <Expression>
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
                    <VariableRef name="a"/>
                    <VariableRef name="b"/>
                </Expression>
            </Expression>
        </Formula>
        <Formula>
            <Expression>
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
                <Expression>
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVOR"/>
                    <VariableRef name="a"/>
                    <VariableRef name="b"/>
                </Expression>
                <Value length="3" type="BIT_VECTOR" value="111"/>
            </Expression>
        </Formula>
        <Formula>
            <Expression>
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
                <Expression>
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVLSHL"/>
                    <VariableRef name="a"/>
                    <Value length="3" type="BIT_VECTOR" value="011"/>
                </Expression>
                <Expression>
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVSMOD"/>
                    <VariableRef name="a"/>
                    <Value length="3" type="BIT_VECTOR" value="010"/>
                </Expression>
            </Expression>
        </Formula>
        <Formula>
            <Expression>
                <Operation family="ru.ispras.fortress.expression.StandardOperation" id="EQ"/>
                <Expression>
                    <Operation family="ru.ispras.fortress.expression.StandardOperation" id="BVAND"/>
                    <VariableRef name="a"/>
                    <VariableRef name="b"/>
                </Expression>
                <Value length="3" type="BIT_VECTOR" value="000"/>
            </Expression>
        </Formula>
    </Syntax>
</Constraint>

The same constraint described in SMT-LIBv2 looks like this:

(declare-const a (_ BitVec 3))
(declare-const b (_ BitVec 3))
(assert (not (= a b)))
(assert (= (bvor a b) #b111))
(assert (= (bvand a b) #b000))
(assert (= (bvshl a (_ bv3 3))(bvsmod a (_ bv2 3))))
(check-sat)
(get-value (a b))
(exit)

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.

Tree Representation¶

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:

1. 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.
2. 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.
3. Operation Represents an operation on some variables, values, parameters or other operations.
4. 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.
5. Value Specifies some known value of the specified type which can be accessed as an attribute.

Note: Operation, Variables and Value are designed to be treated polymorphically. This allows combining them to build complex expressions.

Library Packages¶

The Fortress library is implemented in Java. The Java classes are organized in the following packages:

1. ru.ispras.fortress.calculator - constant sub-expressions simplifier
2. ru.ispras.fortress.data - data types (basic, bit vectors, arrays, etc.)
3. ru.ispras.fortress.esexpr - Lisp-like S-expressions
4. ru.ispras.fortress.expression - syntax tree nodes, operation identifiers
5. ru.ispras.fortress.jaxb - XML integration
6. ru.ispras.fortress.logic - normal form orthogonalizer
7. ru.ispras.fortress.randomizer - randomization engine
8. ru.ispras.fortress.solver - SMT solver integration
9. ru.ispras.fortress.transformer - syntax tree transformation rules and mechanisms
10. ru.ispras.fortress.util - utility methods

Core classes/interfaces¶

Syntax Tree Implementation

The syntax tree nodes are implemented in the following classes:

• Constraint. Parameterized by a collection of Variable objects and a collection of Formula objects.
• Formulas. Parameterized by a collection of syntax tree node objects.
• Operation. Parameterized by operands and an operation type.
• Variable. Parameterized by the variable name string, a data type and a value.
• Value. Parameterized by a data type and a value.

The current implementation supports operations with the following data types: (1) Bit vectors, (2) Booleans, (3) Integers, (4) Real numbers, (5) Arrays.
The code below demonstrates how we can build a syntax tree representation for the integer overflow constraint:

public class IntegerOverflowBitVectorTestCase extends GenericSolverTestBase {
  public IntegerOverflowBitVectorTestCase() {
    super(new IntegerOverflow());
  }

  public static class IntegerOverflow implements SampleConstraint {
    private static final int BIT_VECTOR_LENGTH = 64;
    private static final DataType BIT_VECTOR_TYPE = DataType.bitVector(BIT_VECTOR_LENGTH);

    private static final NodeValue INT_ZERO =
        new NodeValue(BIT_VECTOR_TYPE.valueOf("0", 10));

    private static final NodeValue INT_BASE_SIZE =
        new NodeValue(BIT_VECTOR_TYPE.valueOf("32", 10));

    private static final NodeOperation INT_SIGN_MASK =
        Nodes.bvlshl(Nodes.bvnot(INT_ZERO), INT_BASE_SIZE);

    @Override
    public Constraint getConstraint() {
      final ConstraintBuilder builder = new ConstraintBuilder();

      builder.setName("IntegerOverflow");
      builder.setKind(ConstraintKind.FORMULA_BASED);
      builder.setDescription("IntegerOverflow constraint");

      // Unknown variables
      final NodeVariable rs = new NodeVariable(builder.addVariable("rs", BIT_VECTOR_TYPE));
      final NodeVariable rt = new NodeVariable(builder.addVariable("rt", BIT_VECTOR_TYPE));

      final Formulas formulas = new Formulas();
      builder.setInnerRep(formulas);

      formulas.add(newIsValidSignedInt(rs));
      formulas.add(newIsValidSignedInt(rt));

      formulas.add(Nodes.not(newIsValidSignedInt(Nodes.bvadd(rs, rt))));
      formulas.add(Nodes.not(Nodes.eq(rs, rt)));

      return builder.build();
    }

    private NodeOperation newIsValidPos(final Node arg) {
      return Nodes.eq(Nodes.bvand(arg, INT_SIGN_MASK), INT_ZERO);
    }

    private NodeOperation newIsValidNeg(final Node arg) {
      return Nodes.eq(Nodes.bvand(arg, INT_SIGN_MASK), INT_SIGN_MASK);
    }

    private NodeOperation newIsValidSignedInt(final Node arg) {
      return Nodes.or(newIsValidPos(arg), newIsValidNeg(arg));
    }

    @Override
    public Iterable<Variable> getExpectedVariables() {
      final List<Variable> result = new ArrayList<>();

      result.add(new Variable("rs", BIT_VECTOR_TYPE.valueOf("000000009b91b193", 16)));
      result.add(new Variable("rt", BIT_VECTOR_TYPE.valueOf("000000009b91b1b3", 16)));

      return result;
    }
  }
}

Solver Implementation

Solver implement a common interface that looks like this:

public interface Solver
{
  String getName();
  String getDescription();
  boolean isSupported(ConstraintKind kind);
  boolean isGeneric();
  SolverResult solve(Constraint constraint);
  boolean addCustomOperation(Function function);
  boolean addCustomOperation(FunctionTemplate template);
  String getSolverPath();
  void setSolverPath(String value);
}