From 703ea6b52c24f085215bf5d4631f17a472790dc7 Mon Sep 17 00:00:00 2001 From: redianthus Date: Tue, 17 Feb 2026 00:49:17 +0100 Subject: [PATCH] switch to latest symex and add equalities optimizations --- doc/src/symex/quickstart.md | 4 +- dune-project | 3 +- owi.opam | 2 +- shell.nix | 52 +++++++++++----- src/symbolic/solver.ml | 2 +- src/symbolic/symbolic_choice.ml | 106 +++++++++++++++++++------------- src/symbolic/thread.ml | 4 +- src/symbolic/thread.mli | 2 +- 8 files changed, 107 insertions(+), 68 deletions(-) diff --git a/doc/src/symex/quickstart.md b/doc/src/symex/quickstart.md index a8d336cb0..310814a7c 100644 --- a/doc/src/symex/quickstart.md +++ b/doc/src/symex/quickstart.md @@ -638,8 +638,8 @@ owi: [ERROR] Reached problem! $ owi rust ./mean.rs --entry-point=check --invoke-with-symbols -w1 --fail-on-assertion-only --no-assert-failure-expression-printing --deterministic-result-order owi: [ERROR] Assert failure model { - symbol symbol_0 i32 915013628 - symbol symbol_1 i32 -1225654275 + symbol symbol_0 i32 685822388 + symbol symbol_1 i32 -685822389 } owi: [ERROR] Reached problem! diff --git a/dune-project b/dune-project index cf6685ef2..397ab4dd5 100644 --- a/dune-project +++ b/dune-project @@ -76,7 +76,8 @@ (>= 3.3)) (smtml (>= 0.20.0)) - symex + (symex + (>= 0.2)) (synchronizer (>= 0.3)) (uutf diff --git a/owi.opam b/owi.opam index cc4790d77..5f777d15d 100644 --- a/owi.opam +++ b/owi.opam @@ -40,7 +40,7 @@ depends: [ "processor" {>= "0.2"} "sedlex" {>= "3.3"} "smtml" {>= "0.20.0"} - "symex" + "symex" {>= "0.2"} "synchronizer" {>= "0.3"} "uutf" {>= "1.0.3"} "xmlm" {>= "1.4.0"} diff --git a/shell.nix b/shell.nix index a4546646d..296c38047 100644 --- a/shell.nix +++ b/shell.nix @@ -4,23 +4,41 @@ }: let - ocamlPackages = pkgs.ocaml-ng.ocamlPackages_5_4; - landmarks = ocamlPackages.landmarks.overrideAttrs (old: { - src = pkgs.fetchFromGitHub { - owner = "hra687261"; - repo = "landmarks"; - rev = "17be3567a63650090f9cf94654fcc8d99f946e27"; - hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8="; - }; - }); - landmarks-ppx = ocamlPackages.landmarks-ppx.overrideAttrs (old: { - src = pkgs.fetchFromGitHub { - owner = "hra687261"; - repo = "landmarks"; - rev = "17be3567a63650090f9cf94654fcc8d99f946e27"; - hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8="; - }; - meta.broken = false; + ocamlPackages = pkgs.ocaml-ng.ocamlPackages_5_4.overrideScope (self: super: { + smtml = super.smtml.overrideAttrs (old: { + src = pkgs.fetchFromGitHub { + owner = "formalsec"; + repo = "smtml"; + rev = "a9dff52e7ef2215c786ee8ce2c24d716db0b5ace"; + hash = "sha256-TIOOE/bsis6oYV3Dt6TcI/r/aN3S1MQNtxDAnvBbVO0="; + }; + doCheck = false; + }); + symex = super.symex.overrideAttrs (old: { + src = pkgs.fetchFromGitHub { + owner = "ocamlpro"; + repo = "symex"; + rev = "c4200e160f69d3cd9443301c1c4dc4224c3cab2e"; + hash = "sha256-KX+OHiCsAHEw0kBWLUDVakIcshUNXLYjm2f2le75Mj8="; + }; + }); + landmarks = super.landmarks.overrideAttrs (old: { + src = pkgs.fetchFromGitHub { + owner = "hra687261"; + repo = "landmarks"; + rev = "17be3567a63650090f9cf94654fcc8d99f946e27"; + hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8="; + }; + }); + landmarks-ppx = super.landmarks-ppx.overrideAttrs (old: { + src = pkgs.fetchFromGitHub { + owner = "hra687261"; + repo = "landmarks"; + rev = "17be3567a63650090f9cf94654fcc8d99f946e27"; + hash = "sha256-3ui4uvSAvUgzk2UMVtH9A4BhAX6nWbwx7q0YwkANNv8="; + }; + meta.broken = false; + }); }); in diff --git a/src/symbolic/solver.ml b/src/symbolic/solver.ml index 991175ce2..f5db36400 100644 --- a/src/symbolic/solver.ml +++ b/src/symbolic/solver.ml @@ -43,7 +43,7 @@ let model_of_path_condition (S (solver_module, s)) ~path_condition : let exception Unknown in let module Solver = (val solver_module) in try - let sub_conditions = Symex.Path_condition.slice path_condition in + let sub_conditions = Symex.Path_condition.to_list path_condition in let models = List.map (fun pc -> diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index b5b272282..482c27067 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -23,21 +23,15 @@ let solver_dls_key = let[@inline] solver () = Domain.DLS.get solver_dls_key -let add_pc (c : Symbolic_boolean.t) = - let c = Smtml.Typed.simplify c in - match Smtml.Typed.view c with - | Val True -> return () - | Val False -> prune () - | _ -> - let* state in - let new_thread = Thread.add_pc state c in - set_state new_thread +let add_already_checked_condition_to_pc (condition : Symbolic_boolean.t) = + let* state in + let state = Thread.add_already_checked_condition_to_pc state condition in + set_state state [@@inline] let get_pc () = let+ state in - let pc = state.pc in - let pc = Symex.Path_condition.slice pc in + let pc = Symex.Path_condition.to_list state.pc in List.fold_left Smtml.Expr.Set.union Smtml.Expr.Set.empty pc let add_breadcrumb crumb = modify_state (fun t -> Thread.add_breadcrumb t crumb) @@ -60,16 +54,24 @@ let with_new_symbol ty f = let n = state.num_symbols in let sym = Fmt.kstr (Smtml.Symbol.make ty) "symbol_%d" n in let+ () = - modify_state (fun thread -> - let thread = Thread.add_symbol thread sym in - Thread.incr_num_symbols thread ) + modify_state (fun state -> + let state = Thread.add_symbol state sym in + Thread.incr_num_symbols state ) in f sym -let check_reachability v = +let check_reachability condition = let* state in let solver = solver () in - let pc = state.pc |> Symex.Path_condition.slice_on_condition v in + let pc = Symex.Path_condition.slice_on_new_condition condition state.pc in + (* the condition must be simplified only *after* slicing when we don't know if it is SAT, otherwise, we may exclude some slices and go to an unsat path! *) + let condition = + let equalities = Symex.Path_condition.get_known_equalities state.pc in + Smtml.Expr.inline_symbol_values equalities + (Smtml.Typed.Unsafe.unwrap condition) + |> Smtml.Typed.Unsafe.wrap |> Smtml.Typed.simplify + in + let pc = Smtml.Expr.Set.add (Smtml.Typed.Unsafe.unwrap condition) pc in let stats = state.bench_stats in let reachability = Benchmark.handle_time_span stats.solver_sat_time @@ fun () -> @@ -111,13 +113,14 @@ let select_inner ~with_breadcrumbs (cond : Symbolic_boolean.t) | _ -> let is_other_branch_unsat = Atomic.make false in let branch condition final_value priority = - let* () = add_pc condition in let* () = if with_breadcrumbs then add_breadcrumb (if final_value then 1 else 0) else return () in + let* () = yield priority in (* this is an optimisation under the assumption that the PC is always SAT (i.e. we are performing eager pruning), in such a case, when a branch is unsat, we don't have to check the reachability of the other's branch negation, because it is always going to be SAT. *) if Atomic.get is_other_branch_unsat then begin + let* () = add_already_checked_condition_to_pc condition in Log.debug (fun m -> m "The SMT call for the %b branch was optimized away" final_value ); (* the other branch is unsat, we must be SAT and don't need to check reachability! *) @@ -125,10 +128,10 @@ let select_inner ~with_breadcrumbs (cond : Symbolic_boolean.t) end else begin (* the other branch is SAT (or we haven't computed it yet), so we have to check reachability *) - let* () = yield priority in let* satisfiability = check_reachability condition in begin match satisfiability with | `Sat -> + let* () = add_already_checked_condition_to_pc condition in let* () = modify_state (Thread.set_priority priority) in return final_value | `Unsat -> @@ -137,7 +140,7 @@ let select_inner ~with_breadcrumbs (cond : Symbolic_boolean.t) | `Unknown -> (* It can happen when the solver is interrupted *) (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged - if solver was interrupted then prune () else assert false *) + if solver was interrupted then prune () else assert false *) prune () end end @@ -175,28 +178,34 @@ let select (cond : Symbolic_boolean.t) ~instr_counter_true ~instr_counter_false ~with_breadcrumbs:true [@@inline] -let summary_symbol (e : Smtml.Typed.Bitv32.t) : - (Smtml.Typed.Bool.t option * Smtml.Symbol.t) t = +let select_i32 (e : Symbolic_i32.t) : int32 t = let* state in + let equalities = Symex.Path_condition.get_known_equalities state.pc in + let e = + Smtml.Expr.inline_symbol_values equalities (Smtml.Typed.Unsafe.unwrap e) + |> Smtml.Typed.Unsafe.wrap |> Smtml.Typed.simplify + in match Smtml.Typed.view e with - | Symbol sym -> return (None, sym) - | _ -> - let num_symbols = state.num_symbols in - let+ () = modify_state Thread.incr_num_symbols in - let name = Fmt.str "choice_i32_%i" num_symbols in - (* TODO: having to build two times the symbol this way is not really elegant... *) - let sym = Smtml.Symbol.make Smtml.Typed.Types.(to_ty bitv32) name in - let assign = Smtml.Typed.Bitv32.(eq (symbol sym) e) in - (Some assign, sym) - -let select_i32 (i : Symbolic_i32.t) : int32 t = - match Smtml.Typed.view i with | Val (Bitv bv) when Smtml.Bitvector.numbits bv <= 32 -> return (Smtml.Bitvector.to_int32 bv) | _ -> - let* assign, symbol = summary_symbol i in + let* assign, symbol = + match Smtml.Typed.view e with + | Symbol symbol -> return (None, symbol) + | _ -> + let num_symbols = state.num_symbols in + let+ () = modify_state Thread.incr_num_symbols in + let name = Fmt.str "choice_i32_%i" num_symbols in + let sym = Smtml.Symbol.make Smtml.Typed.Types.(to_ty bitv32) name in + let assign = Smtml.Typed.Bitv32.(eq (symbol sym) e) in + (Some assign, sym) + in let* () = - match assign with Some assign -> add_pc assign | None -> return () + match assign with + | Some assign -> + (* it must be SAT because we only introduced a constraint: new_symbol = e *) + add_already_checked_condition_to_pc assign + | None -> return () in let rec generator () = let* possible_value = get_model_or_prune symbol in @@ -215,16 +224,26 @@ let select_i32 (i : Symbolic_i32.t) : int32 t = in let this_val_branch = let* () = add_breadcrumb (Int32.to_int i) in - let* () = add_pc this_value_cond in + let* () = add_already_checked_condition_to_pc this_value_cond in return i in - let not_this_value_cond = Symbolic_boolean.not this_value_cond in let not_this_val_branch = - let* () = add_pc not_this_value_cond in - generator () + let not_this_value_cond = Symbolic_boolean.not this_value_cond in + (* TODO: this is annoying as the next call to get_model_or_prune is also going to check for satisfiability which is useless! it can probably be simplified. + I'm leaving it for now to be sure this is correct. It may actually not be required but better safe than sorry! *) + let* satisfiability = check_reachability not_this_value_cond in + match satisfiability with + | `Sat -> + let* () = add_already_checked_condition_to_pc not_this_value_cond in + generator () + | `Unsat -> prune () + | `Unknown -> + (* It can happen when the solver is interrupted *) + (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged + if solver was interrupted then prune () else assert false *) + prune () in - let* state in Thread.incr_path_count state; (* TODO: better prio here? *) @@ -289,13 +308,14 @@ let assume condition = | Val True -> return () | Val False -> prune () | _ -> ( - let* () = add_pc condition in let* satisfiability = check_reachability condition in match satisfiability with - | `Sat -> return () + | `Sat -> + let* () = add_already_checked_condition_to_pc condition in + return () | `Unsat -> prune () | `Unknown -> (* It can happen when the solver is interrupted *) (* TODO: once https://github.com/formalsec/smtml/pull/479 is merged - if solver was interrupted then prune () else assert false *) + if solver was interrupted then prune () else assert false *) prune () ) diff --git a/src/symbolic/thread.ml b/src/symbolic/thread.ml index 731c47485..3b51e5327 100644 --- a/src/symbolic/thread.ml +++ b/src/symbolic/thread.ml @@ -71,8 +71,8 @@ let add_symbol t s = let open Symbol_scope in { t with symbol_scopes = symbol s t.symbol_scopes } -let add_pc t c = - let pc = Symex.Path_condition.add c t.pc in +let add_already_checked_condition_to_pc t c = + let pc = Symex.Path_condition.add_checked_sat_condition c t.pc in { t with pc } let add_breadcrumb t crumb = diff --git a/src/symbolic/thread.mli b/src/symbolic/thread.mli index 9b5ef5c2a..6058401e9 100644 --- a/src/symbolic/thread.mli +++ b/src/symbolic/thread.mli @@ -30,7 +30,7 @@ type t = private val init : unit -> t -val add_pc : t -> Symbolic_boolean.t -> t +val add_already_checked_condition_to_pc : t -> Symbolic_boolean.t -> t val add_breadcrumb : t -> int -> t