Add statemenet information to assert failure

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/symbolic_error.ml

@@ -16,7 +16,7 @@
 
 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
@@ -25,15 +25,19 @@ type t =
 
 let pp fmt = function
   | `Abort msg -> Fmt.pf fmt "Abort: %s" msg
-  | `Assert_failure v -> Fmt.pf fmt "@[<hov 1>Assert failure:@;%a@]" Smtml.Expr.pp v
+  | `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,7 +30,9 @@ Test basic symbolic number:
               "target": symbol("empty"),  }
   All Ok!
   $ ecma-sl symbolic symbolic_string_array.js
-  Assert failure: false
+  "":82947.2-82947.20: Assert failure:
+   Stmt: assert (hd params)
+   Expr: false
   Path condition:
    (bool.eq "banana bread" (str.++ ((str.++ (flour, " ")), water)))
   Model:

test/symbolic/simple/test_esl.t

@@ -23,7 +23,9 @@ Esl tests:
   - : int = 1
   All Ok!
   $ ecma-sl symbolic string_concat.esl
-  Assert failure: (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: