diff --git a/CHANGES.md b/CHANGES.md index afa881f944..d03394f58d 100644 --- a/CHANGES.md +++ b/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 diff --git a/bin/commands/cmd_symbolic.ml b/bin/commands/cmd_symbolic.ml index 5311b319da..0491e02660 100644 --- a/bin/commands/cmd_symbolic.ml +++ b/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 "@[ path cond :@ %a@]" Solver.pp_set pc); + Logs.app (fun k -> k "@[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 "@[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 _ = diff --git a/src/semantics/core/functorial/extern_func.ml b/src/semantics/core/functorial/extern_func.ml index 3411b0542b..c42e8cf77f 100644 --- a/src/semantics/core/functorial/extern_func.ml +++ b/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 diff --git a/src/semantics/core/functorial/interpreter_functor.ml b/src/semantics/core/functorial/interpreter_functor.ml index 4d40c38f29..9e1e8618ec 100644 --- a/src/semantics/core/functorial/interpreter_functor.ml +++ b/src/semantics/core/functorial/interpreter_functor.ml @@ -151,8 +151,8 @@ module Make (P : Interpreter_functor_intf.P) () : (* Logs.debug (fun k -> *) (* k "@[ store :@ %a@]" Value.Store.pp locals ); *) Logs.debug (fun k -> k "@[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 diff --git a/src/symbolic/solver.ml b/src/symbolic/solver.ml index 6660d5df1d..deaae7cdbe 100644 --- a/src/symbolic/solver.ml +++ b/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 . *) diff --git a/src/symbolic/symbolic_error.ml b/src/symbolic/symbolic_error.ml index f13602aea5..668a26846c 100644 --- a/src/symbolic/symbolic_error.ml +++ b/src/symbolic/symbolic_error.ml @@ -1,22 +1,22 @@ (* 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 . *) 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 @@ -24,17 +24,20 @@ type t = ] 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@[ Stmt:@;%a@]@\n@[ 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 -> diff --git a/src/syntax/core/stmt.ml b/src/syntax/core/stmt.ml index ebaf81bee2..ba433577ea 100644 --- a/src/syntax/core/stmt.ml +++ b/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 . *) @@ -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 @[%a@]@\n" pp_v in diff --git a/test/symbolic/js/test_basic_symbolic.t b/test/symbolic/js/test_basic_symbolic.t index cb266edcfa..e926d38eee 100644 --- a/test/symbolic/js/test_basic_symbolic.t +++ b/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] diff --git a/test/symbolic/js/test_reference_error.t b/test/symbolic/js/test_reference_error.t index a4a36a1874..6b4aaecfd5 100644 --- a/test/symbolic/js/test_reference_error.t +++ b/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] diff --git a/test/symbolic/simple/test_esl.t b/test/symbolic/simple/test_esl.t index 4116cb98f1..d854e6ae19 100644 --- a/test/symbolic/simple/test_esl.t +++ b/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