Overview

Grackle is a tool for symbolic analyzing MATLAB and LLVM code. This allows one to analyze questions such as “Can I find inputs to a program that lead to a particular result?”, or “Are there inputs that could crash the program?”

During symbolic simulation, the simulator executes the program, and generates expressions describing the results of operations when those operations involve symbolic values. These expressions can then be used to generate constraint problems that are solved using automated decision procedures such as SAT and SMT solvers (see Constraint Solving for details about the supported solvers).

To understand how Grackle works, we start with a simple example showing how the symbolic simulator could be used to solve a linear integer relations:

x = symbolic('x', 'integer');
y = symbolic('y', 'integer');

c1 = 3*x + 5*y < 11;
c2 = 4*x + 3*y > 13;

[r,s] = check_sat(c1 & c2)

When run though the simulator, the output it returns is:

r =

     1

s =

    x: 5
    y: -1

The example shows that r equals 1, indicating the problem is satisfiable, and s is a struct containing the results of the satisfiability query.

The simulator supports both straightline code and control flow statements such as if, switch, and for statements. For example, the following code is supported by the simulator:

x      = symbolic('x', 'real');
target = symbolic('target', 'real');
diff = 3;

if (x > target)
  y = x - diff;
else
  y = x + diff;
end

[r,c] = check_sat(abs(x-target) > diff & abs(y-target) > abs(x-target))

In this case, the example is unsatisfiable, so the result from the simulator is:

r =

     0

c =
     struct with no fields.

In addition to calling Yices directly, the simulator can generate files for Yices and other SMT solvers that can be used offline for verification (see functions write_yices or write_smtlib2 for reference).