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(); // Untyped symbolic variable

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

Assumptions and Assertions

Gillian-JS provides assumption and assertion constructs, 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 an example of a symbolic test using assumptions and assertions:

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

// 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));

The above example is already in the repository, with f instantiated to n1 + n2. You can run the example, starting from the Gillian folder, as follows:

dune exec -- gillian-js wpst Gillian-JS/Examples/Cosette/simple_example.js

Since the assertion in the end does hold, the execution exits successfully. If, instead, you change n1 + n2 to n1 * n2 and re-run the example, you will be faced with the following error message and counterexample:

Compilation time: 0.018218s
Total time (Compilation + Symbolic testing): 3.528332s
Errors occurred!
Here's a counterexample: [ (#gen__0: 0.), (#gen__1: 1.) ]
Here's an example of final error state: FAILURE TERMINATION: Procedure main, Command 77
                                        Errors: EPure(((#gen__0 <=# (#gen__0 * #gen__1)) /\ (#gen__1 <=# (#gen__0 * #gen__1))))
// the rest of the state omitted

which means that the assertion does not hold if n1 = 0 and n2 = 1.

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);