Skip to content

Commit

Permalink
Merge branch 'master' into nat/lab-bug-fix
Browse files Browse the repository at this point in the history
  • Loading branch information
NatKarmios authored Dec 18, 2024
2 parents 884e3cd + d30b852 commit 5e7f88c
Show file tree
Hide file tree
Showing 9 changed files with 180 additions and 162 deletions.
5 changes: 0 additions & 5 deletions Gillian-JS/Examples/Cosette/simple_example.js
Original file line number Diff line number Diff line change
Expand Up @@ -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);
48 changes: 32 additions & 16 deletions GillianCore/command_line/s_interpreter_console.ml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@ module Make
(SState : SState.S with type init_data = ID.t)
(S_interpreter : G_interpreter.S
with type annot = PC.Annot.t
and type state_t = SState.t)
and type state_t = SState.t
and type state_err_t = SState.err_t)
(Gil_parsing : Gil_parsing.S with type annot = PC.Annot.t) : Console.S =
struct
module Common_args = Common_args.Make (PC)
Expand All @@ -35,12 +36,23 @@ struct
open ChangeTracker

let counter_example res =
let error_state =
let error_state, errors =
match res with
| Exec_res.RFail f -> f.error_state
| Exec_res.RFail { error_state; errors; _ } -> (error_state, errors)
| _ -> failwith "Expected failure"
in
let subst = SState.sat_check_f error_state [] in
let f =
errors
|> List.find_map (function
| Exec_err.EState StateErr.(EPure f) -> Some f
| _ -> None)
in
let fs =
match f with
| Some f -> [ Formula.Not f ]
| None -> []
in
let subst = SState.sat_check_f error_state fs in
subst

let run_main prog init_data =
Expand Down Expand Up @@ -76,11 +88,13 @@ struct
let total_time = Sys.time () -. !start_time in
Printf.printf "Total time (Compilation + Symbolic testing): %fs\n"
total_time;
if success then (
Fmt.pr "%a@\n@?" (Fmt.styled `Green Fmt.string) "Success!";
exit 0)
else (
Fmt.pr "%a@\n@?" (Fmt.styled `Red Fmt.string) "Errors occured!";
if success then
let () = Fmt.pr "%a@\n@?" (Fmt.styled `Green Fmt.string) "Success!" in
exit 0
else
let () =
Fmt.pr "%a@\n@?" (Fmt.styled `Red Fmt.string) "Errors occurred!"
in
let first_error =
List.find
(function
Expand All @@ -89,16 +103,18 @@ struct
all_results
in
let counter_example = counter_example first_error in
Fmt.pr "Here's a counter example: %a@\n@?"
Fmt.pr "Here's a counterexample: %a@\n@?"
(Fmt.option
~none:(Fmt.any "Couldn't produce counter-example")
~none:(Fmt.any "Couldn't produce counterexample")
SVal.SESubst.pp)
counter_example;
Fmt.pr "Here's an example of final error state: %a@\n@?"
(Exec_res.pp SState.pp S_interpreter.pp_state_vt
S_interpreter.pp_err_t)
first_error;
exit 1)
let () =
Fmt.pr "Here's an example of final error state: %a@\n@?"
(Exec_res.pp SState.pp S_interpreter.pp_state_vt
S_interpreter.pp_err_t)
first_error
in
exit 1

let run_incr source_files prog init_data =
(* Only re-run program if transitive callees of main proc have changed *)
Expand Down
2 changes: 0 additions & 2 deletions GillianCore/engine/general_semantics/general/g_interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -533,8 +533,6 @@ struct
Fmt.(option ~none:(any "CANNOT CREATE MODEL") ESubst.pp)
failing_model
in
if not (Exec_mode.is_biabduction_exec !Config.current_exec_mode) then
Printf.printf "%s" msg;
L.normal (fun m -> m "%s" msg);
Res_list.error_with err

Expand Down
2 changes: 1 addition & 1 deletion GillianCore/smt/smt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -988,6 +988,7 @@ let exec_sat' (fs : Formula.Set.t) (gamma : typenv) : sexp option =
(Fmt.iter ~sep:(Fmt.any "@\n") Formula.Set.iter Formula.pp)
fs pp_typenv gamma)
in
let () = reset_solver () in
let encoded_assertions = encode_assertions fs gamma in
let () = if !Config.dump_smt then Dump.dump fs gamma encoded_assertions in
let () = List.iter cmd !builtin_funcs in
Expand Down Expand Up @@ -1026,7 +1027,6 @@ let exec_sat' (fs : Formula.Set.t) (gamma : typenv) : sexp option =
| Sat -> Some (get_model solver)
| Unsat -> None
in
let () = reset_solver () in
ret

let exec_sat (fs : Formula.Set.t) (gamma : typenv) : sexp option =
Expand Down
4 changes: 2 additions & 2 deletions sphinx/c2/index.rst
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Gillian-C2 (Alternative C Instantiation)
========================================
Gillian-C2
==========

.. danger::

Expand Down
53 changes: 20 additions & 33 deletions sphinx/js/symbolic-testing.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)));
Expand All @@ -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``).
2 changes: 1 addition & 1 deletion sphinx/wisl/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@ WISL is an instantiation of Gillian to a simple while language with a C-style bl
.. toctree::
:titlesonly:

lab
verification-tutorial
102 changes: 0 additions & 102 deletions sphinx/wisl/lab.rst

This file was deleted.

Loading

0 comments on commit 5e7f88c

Please sign in to comment.