nicer output for symbolic execution

README.md

@@ -108,65 +108,31 @@ For more, have a look at the [example] folder, at the [documentation] or at the
 
 The interpreter can also be used in symbolic mode. This allows to find which input values are leading to a trap.
 
-Given a file `test/mini_test.wast` with the following content:
+Given a file `test/sym/mini_test.wast` with the following content:
 
-<!-- $MDX file=test/mini_test.wast -->
+<!-- $MDX file=test/sym/mini_test.wast -->
 ```wast
 (module
-  (import "print" "i32" (func $print_i32 (param i32)))
   (import "symbolic" "i32" (func $gen_i32 (param i32) (result i32)))
-  (func $factR (export "fact") (param $n i32) (result i32)
-    local.get $n
-    local.get $n
-    i32.const 1
-    i32.eq
-    br_if 0
-    i32.const 1
-    i32.sub
-    call $factR
-    local.get $n
-    i32.mul
-  )
 
-  (func $start
-    (local $x i32)
-    (i32.const 123)
-    (call $print_i32)
+  (func $start (local $x i32)
     (local.set $x (call $gen_i32 (i32.const 42)))
     (if (i32.lt_s (i32.const 5) (local.get $x)) (then
       unreachable
-    ))
-    (if (i32.gt_s (i32.const 1) (local.get $x)) (then
-      unreachable
-    ))
-    (local.get $x)
-    (call $factR)
-    (call $print_i32))
+    )))
 
   (start $start)
 )
 ```
 
 You can run the symbolic interpreter through the `sym` command:
 ```sh
-$ dune exec owi -- sym test/mini_test.wast
-(i32 123)
-CHOICE: (i32.lt_s (i32 5) x_1)
-PATH CONDITION:
-(i32.lt_s (i32 5) x_1)
-TRAP: unreachable
-CHOICE: (i32.gt_s (i32 1) x_1)
+$ dune exec owi -- sym test/sym/mini_test.wast
+Trap: unreachable
 Model:
-(model
-(x_1 i32 (i32 6))
-)
+  (model
+    (x_0 i32 (i32 6)))
 Reached problem!
-
-Solver time 0.002983s
-      calls 1
-  mean time 2.983000ms
-CHOICE: (i32.eq x_1 (i32 1))
-x_1
 ```
 
 ## Supported proposals

src/choice_monad.ml

@@ -31,6 +31,9 @@ let check (sym_bool : vbool) (state : Thread.t) : bool =
     Format.printf "@./CHECK %s@." msg;
     not r
 
+(* TODO: make this a CLI flag ? *)
+let print_choice = false
+
 module Make (M : sig
   type 'a t
 
@@ -71,7 +74,8 @@ struct
       | false, false -> M.empty
       | true, false | false, true -> M.return (sat_true, state)
       | true, true ->
-        Format.printf "CHOICE: %a@." Encoding.Expression.pp e;
+        if print_choice then
+          Format.printf "CHOICE: %a@." Encoding.Expression.pp e;
         let state1 = Thread.clone { state with pc = with_e } in
         let state2 = Thread.clone { state with pc = with_not_e } in
         M.cons (true, state1) (M.return (false, state2)) )

src/cmd_sym.ml

@@ -4,6 +4,11 @@ module Value = Symbolic_value.S
 module Choice = Symbolic.P.Choice
 module Solver = Thread.Solver
 
+(* TODO: make this a CLI flag *)
+let print_solver_time = false
+
+let print_path_condition = false
+
 let print_extern_module : Symbolic.P.extern_func Link.extern_module =
   let print_i32 (i : Value.int32) : unit Choice.t =
     Printf.printf "%s\n%!" (Encoding.Expression.to_string i);
@@ -239,21 +244,22 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure workspace
     Seq.filter_map
       (fun (result, thread) ->
         let pc = Thread.pc thread in
-        Format.printf "PATH CONDITION:@.%a@." Expr.pp_list pc;
+        if print_path_condition then
+          Format.printf "PATH CONDITION:@\n%a@\n" Expr.pp_list pc;
         let model = get_model solver pc in
         let result =
           match result with
           | Choice_monad_intf.EVal (Ok ()) -> None
           | EAssert assertion ->
-            Format.printf "Assert failure: %a@." Expr.pp assertion;
-            Format.printf "Model:@.%a@." Encoding.Model.pp model;
+            Format.printf "Assert failure: %a@\n" Expr.pp assertion;
+            Format.printf "Model:@\n  @[<v>%a@]@\n" Encoding.Model.pp model;
             Some pc
           | ETrap tr ->
-            Format.printf "TRAP: %s@." (Trap.to_string tr);
-            Format.printf "Model:@.%a@." Encoding.Model.pp model;
+            Format.printf "Trap: %s@\n" (Trap.to_string tr);
+            Format.printf "Model:@\n  @[<v>%a@]@\n" Encoding.Model.pp model;
             Some pc
           | EVal (Error e) ->
-            Format.eprintf "%s@." e;
+            Format.eprintf "Error: %s@\n" e;
             exit 1
         in
         let testcase =
@@ -269,17 +275,18 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure workspace
   let () =
     if no_stop_at_failure then
       let failures = Seq.fold_left (fun n _ -> succ n) 0 failing in
-      if failures = 0 then Format.printf "All OK@."
-      else Format.printf "Reached %i problems!@." failures
+      if failures = 0 then Format.printf "All OK@\n"
+      else Format.printf "Reached %i problems!@\n" failures
     else
       match failing () with
-      | Nil -> Format.printf "All OK@."
-      | Cons (_thread, _) -> Format.printf "Reached problem!@."
+      | Nil -> Format.printf "All OK@\n"
+      | Cons (_thread, _) -> Format.printf "Reached problem!@\n"
   in
   let time = !Thread.Solver.solver_time in
   let count = !Thread.Solver.solver_count in
-  Format.printf "@.";
-  Format.printf "Solver time %fs@." time;
-  Format.printf "      calls %i@." count;
-  Format.printf "  mean time %fms@." (1000. *. time /. float count);
-  ()
+  if print_solver_time then begin
+    Format.printf "@\n";
+    Format.printf "Solver time %fs@\n" time;
+    Format.printf "      calls %i@\n" count;
+    Format.printf "  mean time %fms@\n" (1000. *. time /. float count)
+  end

test/sym/mini_test.wast

@@ -0,0 +1,11 @@
+(module
+  (import "symbolic" "i32" (func $gen_i32 (param i32) (result i32)))
+
+  (func $start (local $x i32)
+    (local.set $x (call $gen_i32 (i32.const 42)))
+    (if (i32.lt_s (i32.const 5) (local.get $x)) (then
+      unreachable
+    )))
+
+  (start $start)
+)