From 649f1e0ba0c92928d31e5e0e4b3563d41e3f2651 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20L=C3=B6=C3=B6w?= Date: Wed, 11 Dec 2024 08:47:48 +0000 Subject: [PATCH] Gillian-JS symbolic testing documentation for website --- Gillian-JS/Examples/Cosette/simple_example.js | 5 -- sphinx/js/symbolic-testing.rst | 53 +++++++------------ 2 files changed, 20 insertions(+), 38 deletions(-) diff --git a/Gillian-JS/Examples/Cosette/simple_example.js b/Gillian-JS/Examples/Cosette/simple_example.js index 8fdc98a8b..aca9c1066 100644 --- a/Gillian-JS/Examples/Cosette/simple_example.js +++ b/Gillian-JS/Examples/Cosette/simple_example.js @@ -5,8 +5,3 @@ Assume((0 <= n1) and (0 <= n2) and (not (n1 = n2))); var res = n1 + n2; Assert((n1 <= res) and (n2 <= res)); - -var x = symb(); -Assume(not (typeOf x = Obj)); - -var tx = typeof(x); \ No newline at end of file diff --git a/sphinx/js/symbolic-testing.rst b/sphinx/js/symbolic-testing.rst index bc879da7c..3b586f864 100644 --- a/sphinx/js/symbolic-testing.rst +++ b/sphinx/js/symbolic-testing.rst @@ -13,18 +13,16 @@ One can declare untyped symbolic variables, symbolic booleans, symbolic strings, .. code-block:: js - var x = symb(x); // Untyped symbolic variable + var x = symb(); // 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. + var b = symb_number(); // Symbolic boolean + var n = symb_number(); // Symbolic number + var s = symb_string(); // Symbolic string Assumptions and Assertions ^^^^^^^^^^^^^^^^^^^^^^^^^^ -Cosette provides a mechanism for reasoning about the symbols, in the form of assumptions and assertions, as follows: +Gillian-JS provides assumption and assertion constructs, as follows: .. code-block:: js @@ -47,12 +45,12 @@ The grammar of boolean expressions (``B``) and expressions (``E``) is (approxima | 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: +Here is an example of a symbolic test using assumptions and assertions: .. code-block:: js // Create two symbolic numbers - var n1 = symb_number(n1), n2 = symb_number(n2); + 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))); @@ -63,44 +61,33 @@ Here is the example of a symbolic test using assumptions and assertions: // 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: +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: -.. code-block:: bash +.. code-block:: text - dune build - make js-init-env - cd JaVerT/environment - dune exec -- gillian-js wpst Examples/Cosette/simple_example.js -s + dune exec -- gillian-js wpst Gillian-JS/Examples/Cosette/simple_example.js -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: +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: .. code-block:: text - Assert failed with argument ((#n1 <=# (#n1 * #n2)) /\ (#n2 <=# (#n1 * #n2))). - Failing Model: - [ (#n2: 1), (#n1: 0) ] + 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``. Here, variables prefixed by ``#`` denote logical variables; in this case, the parameters given to the ``symb_number`` function. +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: +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: .. code-block:: js 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: - -.. code-block:: js - - 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``).