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

@@ -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

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

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
 

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 }

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

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]