Improve symbolic execution output

CHANGES.md

@@ -3,6 +3,7 @@
 ### Changed
 ### Added
 
+- Improves symbolic execution prints
 - Adds `s_join` to ecma-sl's standard library
 - Adds `fpath`, a simple library to manipulate paths, to ecma-sl's standard library
 - Adds `os`, a simple library to manipulate files, to ecma-sl's standard library

bin/commands/cmd_symbolic.ml

@@ -71,7 +71,7 @@ let serialize_thread workspace =
   fun thread witness ->
     let open Fpath in
     let pc = Thread.pc thread in
-    Logs.debug (fun pp -> pp "@[<hov 1>  path cond :@ %a@]" Solver.pp_set pc);
+    Logs.app (fun k -> k "@[<hov 1>Path condition:@;%a@]" Solver.pp_set pc);
     let solver = Thread.solver thread in
     match Solver.check_set solver pc with
     | `Unsat | `Unknown ->
@@ -81,6 +81,7 @@ let serialize_thread workspace =
       let model = Solver.model solver in
       let path = Fmt.kstr (add_seg workspace) "witness-%d" (next_int ()) in
       let pp = Fmt.option Smtml.Model.pp in
+      Logs.app (fun k -> k "@[<v 1>Model:@;%a@]" pp model);
       let pc = Smtml.Expr.Set.to_list @@ pc in
       let _ = Bos.OS.File.writef ~mode (path + ".sexp") "%a@." pp model in
       let _ =

src/semantics/core/functorial/extern_func.ml

@@ -19,7 +19,7 @@ open Prelude
 
 type 'a err =
   [ `Abort of string
-  | `Assert_failure of 'a
+  | `Assert_failure of EslSyntax.Stmt.t * 'a
   | `Eval_failure of 'a
   | `Exec_failure of 'a
   | `ReadFile_failure of 'a

src/semantics/core/functorial/interpreter_functor.ml

@@ -151,8 +151,8 @@ module Make (P : Interpreter_functor_intf.P) () :
     (* Logs.debug (fun k -> *)
     (*   k "@[<hov 1>      store :@ %a@]" Value.Store.pp locals ); *)
     Logs.debug (fun k -> k "@[<hov 1>running stmt:@ %a@]" Stmt.pp_simple stmt);
-    match stmt.it with
-    | Stmt.Skip -> ok state
+    match Stmt.view stmt with
+    | Skip -> ok state
     | Merge -> ok state
     | Debug stmt ->
       Logs.warn (fun k -> k "ignoring break point in line %d" stmt.at.lpos.line);
@@ -170,7 +170,7 @@ module Make (P : Interpreter_functor_intf.P) () :
     | Assert e ->
       let e' = eval_expr locals e in
       let* b = Choice.check ~add_to_pc:true @@ Value.Bool.not_ e' in
-      if not b then ok state else error (`Assert_failure e')
+      if not b then ok state else error (`Assert_failure (stmt, e'))
     | Block blk -> ok { state with stmts = blk @ state.stmts }
     | If (br, blk1, blk2) ->
       let br = eval_expr locals br in

src/symbolic/solver.ml

@@ -1,15 +1,15 @@
 (* Copyright (C) 2022-2025 formalsec programmers
- * 
+ *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
  * the Free Software Foundation, either version 3 of the License, or
  * (at your option) any later version.
- * 
+ *
  * This program is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  * GNU General Public License for more details.
- * 
+ *
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)

src/symbolic/symbolic_error.ml

@@ -1,40 +1,43 @@
 (* Copyright (C) 2022-2025 formalsec programmers
- * 
+ *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
  * the Free Software Foundation, either version 3 of the License, or
  * (at your option) any later version.
- * 
+ *
  * This program is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  * GNU General Public License for more details.
- * 
+ *
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
 type t =
   [ `Abort of string
-  | `Assert_failure of Smtml.Expr.t
+  | `Assert_failure of EslSyntax.Stmt.t * Smtml.Expr.t
   | `Eval_failure of Smtml.Expr.t
   | `Exec_failure of Smtml.Expr.t
   | `ReadFile_failure of Smtml.Expr.t
   | `Failure of string
   ]
 
 let pp fmt = function
-  | `Abort msg -> Fmt.pf fmt "      abort : %s@." msg
-  | `Assert_failure v ->
-    Fmt.pf fmt "     assert : failure with (%a)" Smtml.Expr.pp v
-  | `Eval_failure v -> Fmt.pf fmt "       eval : %a" Smtml.Expr.pp v
-  | `Exec_failure v -> Fmt.pf fmt "       exec : %a" Smtml.Expr.pp v
-  | `ReadFile_failure v -> Fmt.pf fmt "   readFile : %a" Smtml.Expr.pp v
-  | `Failure msg -> Fmt.pf fmt "    failure : %s" msg
+  | `Abort msg -> Fmt.pf fmt "Abort: %s" msg
+  | `Assert_failure (stmt, v) ->
+    let pos = stmt.EslSyntax.Source.at in
+    Fmt.pf fmt
+      "%a: Assert failure:@\n@[<hov 1> Stmt:@;%a@]@\n@[<hov 1> Expr:@;%a@]"
+      EslSyntax.Source.pp_at pos EslSyntax.Stmt.pp stmt Smtml.Expr.pp v
+  | `Eval_failure v -> Fmt.pf fmt "Eval failure: %a" Smtml.Expr.pp v
+  | `Exec_failure v -> Fmt.pf fmt "Exec failure: %a" Smtml.Expr.pp v
+  | `ReadFile_failure v -> Fmt.pf fmt "ReadFile failure: %a" Smtml.Expr.pp v
+  | `Failure msg -> Fmt.pf fmt "Failure: %s" msg
 
 let to_json = function
   | `Abort msg -> `Assoc [ ("type", `String "Abort"); ("sink", `String msg) ]
-  | `Assert_failure v ->
+  | `Assert_failure (_, v) ->
     let v = Smtml.Expr.to_string v in
     `Assoc [ ("type", `String "Assert failure"); ("sink", `String v) ]
   | `Eval_failure v ->

src/syntax/core/stmt.ml

@@ -1,15 +1,15 @@
 (* Copyright (C) 2022-2025 formalsec programmers
- * 
+ *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
  * the Free Software Foundation, either version 3 of the License, or
  * (at your option) any later version.
- * 
+ *
  * This program is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  * GNU General Public License for more details.
- * 
+ *
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
@@ -45,6 +45,8 @@ let default : unit -> t =
   let dlft = Skip @> none in
   fun () -> dlft
 
+let view stmt = Source.view stmt
+
 let rec pp (ppf : Format.formatter) (s : t) : unit =
   let pp_vs pp_v ppf es = Fmt.(list ~sep:comma pp_v) ppf es in
   let pp_indent pp_v ppf = Fmt.pf ppf "@\n  @[<v>%a@]@\n" pp_v in

test/symbolic/js/test_basic_symbolic.t

@@ -30,6 +30,14 @@ Test basic symbolic number:
               "target": symbol("empty"),  }
   All Ok!
   $ ecma-sl symbolic symbolic_string_array.js
-       assert : failure with (false)
+  "":82947.2-82947.20: Assert failure:
+   Stmt: assert (hd params)
+   Expr: false
+  Path condition:
+   (bool.eq "banana bread" (str.++ ((str.++ (flour, " ")), water)))
+  Model:
+   (model
+     (flour str "bread")
+     (water str "banana"))
   Found 1 problems!
   [21]

test/symbolic/js/test_reference_error.t

@@ -1,12 +1,18 @@
 Tests GetValue:
   $ ecma-sl symbolic reference_error_1.js
-        abort : "Uncaught ReferenceError: A is not defined"
-
+  Abort: "Uncaught ReferenceError: A is not defined"
+  Path condition: 
+  Model:
+   (model
+     )
   Found 1 problems!
   [20]
 Tests PutValue:
   $ ecma-sl symbolic reference_error_2.js
-        abort : "Uncaught ReferenceError: a is not defined"
-
+  Abort: "Uncaught ReferenceError: a is not defined"
+  Path condition: 
+  Model:
+   (model
+     )
   Found 1 problems!
   [20]

test/symbolic/simple/test_esl.t

@@ -4,7 +4,11 @@ Esl tests:
   All Ok!
   $ ecma-sl symbolic extern.esl
   x
-      failure : unable to find external function 'i_dont_exist'
+  Failure: unable to find external function 'i_dont_exist'
+  Path condition: 
+  Model:
+   (model
+     )
   Found 1 problems!
   [25]
   $ ecma-sl symbolic func.esl
@@ -19,8 +23,15 @@ Esl tests:
   - : int = 1
   All Ok!
   $ ecma-sl symbolic string_concat.esl
-       assert : failure with ((bool.ne (str.++ (flour, " ", water))
-                               "banana bread"))
+  "string_concat.esl":7.2-7.33: Assert failure:
+   Stmt: assert (loaf != "banana bread")
+   Expr: (bool.ne (str.++ (flour, " ", water)) "banana bread")
+  Path condition:
+   (bool.not (bool.ne (str.++ (flour, " ", water)) "banana bread"))
+  Model:
+   (model
+     (flour str "bread")
+     (water str "banana"))
   Found 1 problems!
   [21]
   $ ecma-sl symbolic while.esl