From ea95a1ebd6e53c372469566d9d02a29bbb412336 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 27 Jun 2024 11:17:48 +0200 Subject: [PATCH] Refactor symbol creation functions - Use `Thread.symbol` for creating unique symbols, replacing the global atomic variable in `symbolic_wasm_ffi.ml`. - Add `with_new_symbol` to `symbolic_choice` to mirror the approach in `concolic_wasm_ffi`. - Rename `Thread.incr_choices` to `incr_symbols` and make `Thread.symbol_set` immutable. --- src/symbolic/symbolic_choice.ml | 21 ++++++++++++++----- src/symbolic/symbolic_choice.mli | 2 ++ src/symbolic/symbolic_wasm_ffi.ml | 35 ++++++++++--------------------- src/symbolic/thread.ml | 18 ++++++++-------- src/symbolic/thread.mli | 8 +++---- test/sym/div.t | 6 +++--- 6 files changed, 45 insertions(+), 45 deletions(-) diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 8fbc93818..46e286d48 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -309,7 +309,7 @@ end = struct let* thread in let* solver in let pc = Thread.pc thread in - let symbols = Thread.symbols thread |> Option.some in + let symbols = Thread.symbols_set thread |> Option.some in let model = Solver.model solver ~symbols ~pc in State.return (ETrap (t, model)) @@ -336,6 +336,17 @@ let add_pc (c : Symbolic_value.vbool) = let add_breadcrumb crumb = modify_thread (fun t -> Thread.add_breadcrumb t crumb) +let with_new_symbol ty f = + let* thread in + let n = Thread.symbols thread in + let sym = Format.ksprintf (Smtml.Symbol.make ty) "symbol_%d" n in + let+ () = + modify_thread (fun thread -> + let thread = Thread.add_symbol thread sym in + Thread.incr_symbols thread ) + in + f sym + (* Yielding is currently done each time the solver is about to be called, in check_reachability and get_model. @@ -396,9 +407,9 @@ let summary_symbol (e : Smtml.Expr.t) = match Smtml.Expr.view e with | Symbol sym -> return (None, sym) | _ -> - let choices = Thread.choices thread in - let+ () = modify_thread Thread.incr_choices in - let sym_name = Format.sprintf "choice_i32_%i" choices in + let num_symbols = Thread.symbols thread in + let+ () = modify_thread Thread.incr_symbols in + let sym_name = Format.sprintf "choice_i32_%i" num_symbols in let sym_type = Smtml.Ty.Ty_bitv 32 in let sym = Smtml.Symbol.make sym_type sym_name in let assign = Smtml.Expr.(relop Ty_bool Eq (mk_symbol sym) e) in @@ -450,7 +461,7 @@ let assertion c = else let* thread in let* solver in - let symbols = Thread.symbols thread |> Option.some in + let symbols = Thread.symbols_set thread |> Option.some in let pc = Thread.pc thread in let model = Solver.model ~symbols ~pc solver in assertion_fail c model diff --git a/src/symbolic/symbolic_choice.mli b/src/symbolic/symbolic_choice.mli index 60335a9c1..c52a97c0d 100644 --- a/src/symbolic/symbolic_choice.mli +++ b/src/symbolic/symbolic_choice.mli @@ -13,6 +13,8 @@ include and type 'a run_result = ('a eval * Thread.t) Seq.t and module V := Symbolic_value +val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t + val run : workers:int -> Smtml.Solver_dispatcher.solver_type diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index 791c7f51c..e8ffd012e 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -3,7 +3,7 @@ (* Written by the Owi programmers *) module Expr = Smtml.Expr -module Choice = Symbolic.P.Choice +module Choice = Symbolic_choice (* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *) module M : @@ -14,39 +14,26 @@ module M : module Value = Symbolic_value - let sym_cnt = Atomic.make 0 - - let symbol ty () : Value.int32 Choice.t = - let id = Atomic.fetch_and_add sym_cnt 1 in - let sym = Format.kasprintf (Smtml.Symbol.make ty) "symbol_%d" id in - let sym_expr = Expr.mk_symbol sym in - Choice.with_thread (fun thread -> - Thread.add_symbol thread sym; - match ty with - | Ty_bitv 8 -> Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, sym_expr)) - | _ -> sym_expr ) - let assume_i32 (i : Value.int32) : unit Choice.t = - let c = Value.I32.to_bool i in - Choice.add_pc c + Choice.add_pc @@ Value.I32.to_bool i let assume_positive_i32 (i : Value.int32) : unit Choice.t = - let c = Value.I32.ge i Value.I32.zero in - Choice.add_pc c + Choice.add_pc @@ Value.I32.ge i Value.I32.zero let assert_i32 (i : Value.int32) : unit Choice.t = - let c = Value.I32.to_bool i in - Choice.assertion c + Choice.assertion @@ Value.I32.to_bool i - let symbol_i8 = symbol (Ty_bitv 8) + let symbol_i8 () = + Choice.with_new_symbol (Ty_bitv 8) (fun sym -> + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) - let symbol_i32 = symbol (Ty_bitv 32) + let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol - let symbol_i64 = symbol (Ty_bitv 64) + let symbol_i64 () = Choice.with_new_symbol (Ty_bitv 64) Expr.symbol - let symbol_f32 = symbol (Ty_fp 32) + let symbol_f32 () = Choice.with_new_symbol (Ty_fp 32) Expr.symbol - let symbol_f64 = symbol (Ty_fp 64) + let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol open Expr diff --git a/src/symbolic/thread.ml b/src/symbolic/thread.ml index e49a0572e..0f16d4b63 100644 --- a/src/symbolic/thread.ml +++ b/src/symbolic/thread.ml @@ -3,8 +3,8 @@ (* Written by the Owi programmers *) type t = - { choices : int - ; mutable symbol_set : Smtml.Symbol.t list + { symbols : int + ; symbol_set : Smtml.Symbol.t list ; pc : Symbolic_value.vbool list ; memories : Symbolic_memory.collection ; tables : Symbolic_table.collection @@ -14,7 +14,7 @@ type t = ; breadcrumbs : int32 list } -let choices t = t.choices +let symbols t = t.symbols let pc t = t.pc @@ -26,18 +26,18 @@ let globals t = t.globals let breadcrumbs t = t.breadcrumbs -let symbols t = t.symbol_set +let symbols_set t = t.symbol_set -let add_symbol t s = t.symbol_set <- s :: t.symbol_set +let add_symbol t s = { t with symbol_set = s :: t.symbol_set } let add_pc t c = { t with pc = c :: t.pc } let add_breadcrumb t crumb = { t with breadcrumbs = crumb :: t.breadcrumbs } -let incr_choices t = { t with choices = succ t.choices } +let incr_symbols t = { t with symbols = succ t.symbols } let create () = - { choices = 0 + { symbols = 0 ; symbol_set = [] ; pc = [] ; memories = Symbolic_memory.init () @@ -46,8 +46,8 @@ let create () = ; breadcrumbs = [] } -let clone { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } = +let clone { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } = let memories = Symbolic_memory.clone memories in let tables = Symbolic_table.clone tables in let globals = Symbolic_global.clone globals in - { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } + { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } diff --git a/src/symbolic/thread.mli b/src/symbolic/thread.mli index 3d6687a03..d24d7b359 100644 --- a/src/symbolic/thread.mli +++ b/src/symbolic/thread.mli @@ -14,9 +14,9 @@ val globals : t -> Symbolic_global.collection val breadcrumbs : t -> int32 list -val symbols : t -> Smtml.Symbol.t list +val symbols_set : t -> Smtml.Symbol.t list -val choices : t -> int +val symbols : t -> int val create : unit -> t @@ -26,6 +26,6 @@ val add_pc : t -> Symbolic_value.vbool -> t val add_breadcrumb : t -> int32 -> t -val add_symbol : t -> Smtml.Symbol.t -> unit +val add_symbol : t -> Smtml.Symbol.t -> t -val incr_choices : t -> t +val incr_symbols : t -> t diff --git a/test/sym/div.t b/test/sym/div.t index a078d3f92..3d4b56a5e 100644 --- a/test/sym/div.t +++ b/test/sym/div.t @@ -51,16 +51,16 @@ div binop: Model: (model (symbol_0 (i32 1)) - (symbol_2 (i32 0))) + (symbol_1 (i32 0))) Trap: integer divide by zero Model: (model (symbol_0 (i32 2)) - (symbol_3 (i64 0))) + (symbol_1 (i64 0))) Trap: integer divide by zero Model: (model (symbol_0 (i32 3)) - (symbol_5 (i64 0))) + (symbol_1 (i64 0))) Reached 4 problems! [13]