Symbolic Testing

Writing Symbolic Tests

The whole-program symbolic testing module of Gillian-JS extends JavaScript with a mechanism for declaring symbolic variables and performing first-order reasoning on them.

Declaring Symbolic Variables

One can declare untyped symbolic variables, symbolic booleans, symbolic strings, and symbolic numbers as follows:

var x = symb(x); // Untyped symbolic variable

var b = symb_number(b); // Symbolic boolean
var n = symb_number(n); // Symbolic number
var s = symb_string(s); // Symbolic string

The single parameters provided to these functions indicate the name of the created symbol, or logical variable, that Cosette will further use in the reaasoning. Normally, we choose these to coincide with the JavaScript variables in which they are stored so that the outputs of the analysis are more readable.

Assumptions and Assertions

Cosette provides a mechanism for reasoning about the symbols, in the form of assumptions and assertions, as follows:

Assume(B); // Assume that the boolean expression B holds
Assert(B); // Assert that the boolean expression B holds

The grammar of boolean expressions (B) and expressions (E) is (approximately) as follows:

B ::=
  | x                         // (Boolean) variables
  | E = E                     // Equality
  | E < E | E <= E            // Comparison
  | not B | B and B | B or B  // Logical operators

E ::=
  | c                           // Constants
  | x                           // Variables
  | E + E | E - E | ...         // Numeric operators
  | E ++ E | s-len E | s-nth E  // String concat, length, and n-th

Here is the example of a symbolic test using assumptions and assertions:

// Create two symbolic numbers
var n1 = symb_number(n1), n2 = symb_number(n2);

// Assume that they are non-negative and different
Assume((0 <= n1) and (0 <= n2) and (not (n1 = n2)));

// Perform some calculations
var res = f(n1, n2);

// Assert, for example, that n1 and n2 are not greater than the result
Assert((n1 <= res) and (n2 <= res));

This example is already in the repository (with f instantiated to n1 + n2), and you can run it, starting from the Gillian folder, as follows:

dune build
make js-init-env
cd JaVerT/environment
dune exec -- gillian-js wpst Examples/Cosette/simple_example.js -s

Since the assertion in the end does hold, there will be no output from Cosette, meaning that the test has passed. If however, you change n1 + n2 to n1 * n2 and re-run the example, you will be faced with the following error message and counter-model:

Assert failed with argument ((#n1 <=# (#n1 * #n2)) /\ (#n2 <=# (#n1 * #n2))).
Failing Model:
  [ (#n2: 1), (#n1: 0) ]

which means that the assertion does not hold if n1 = 0 and n2 = 1. Here, variables prefixed by # denote logical variables; in this case, the parameters given to the symb_number function.

Semantics of Operators

Importantly, the semantics of all of the operators is deliberately NOT as in JavaScript. For example, comparison and numeric operators do not perform any implicit type coercions. If you want to use JavaScript comparison/numeric operators, say <=, you can proceed as follows:

var res_leq_n1 = n1 <= res;

Assert(n1_leq_res);

Typing and Objects in Symbolic Tests

Since we do not (yet) perform lazy initialisation in symbolic execution, errors may occur if you attempt to reason about symbolic objects or untyped symbolic variables. This can be prevented as follows:

var x = symb(x);
Assume(not (typeOf x = Obj));

where typeOf is the built-in GIL typing operator and Obj is the built-in GIL object type. In this way, it is guaranteed that x is not an object (but may still equal null).