Fix Symbolic.concretize

src/symbolic.ml

@@ -59,31 +59,19 @@ struct
   module Memory = struct
     include Symbolic_memory
 
-    let concretise a =
+    let concretise (a : Encoding.Expr.t) : Encoding.Expr.t Choice.t =
       let open Choice in
-      let open Encoding.Expr in
-      let* thread in
-      let+ (S (solver_mod, solver)) = solver in
-      let module Solver = (val solver_mod) in
-      let open Hc in
+      let open Encoding in
       match a.node.e with
-      | Val _ | Ptr (_, { node = { e = Val _; _ }; _ }) -> a
+      (* Avoid unecessary re-hashconsing and allocation when the value
+         is already concrete. *)
+      | Val _ | Ptr (_, { node = { e = Val _; _ }; _ }) -> return a
       | Ptr (base, offset) ->
-        (* TODO: can we remove this check? We should be in a SAT branch *)
-        assert (Solver.check solver @@ Thread.pc thread);
-        let concrete_offest = Solver.get_value solver offset in
-        let cond = Relop (Eq, offset, concrete_offest) @: a.node.ty in
-        (* TODO: this should go to the pc *)
-        Solver.add solver [ cond ];
-        Ptr (base, concrete_offest) @: a.node.ty
+        let+ offset = select_i32 offset in
+        Expr.(Ptr (base, Symbolic_value.const_i32 offset) @: Ty_bitv S32)
       | _ ->
-        (* TODO: can we remove this check? We should be in a SAT branch *)
-        assert (Solver.check solver @@ Thread.pc thread);
-        let concrete_addr = Solver.get_value solver a in
-        let cond = Relop (Eq, a, concrete_addr) @: a.node.ty in
-        (* TODO: this should go to the pc *)
-        Solver.add solver [ cond ];
-        concrete_addr
+        let+ v = select_i32 a in
+        Symbolic_value.const_i32 v
 
     (* TODO: *)
     (* 1. Let pointers have symbolic offsets *)

test/sym/dune

@@ -19,6 +19,7 @@
   global.wat
   grow.wat
   memory.wat
+  memory2.wat
   mini_test.wat
   mul_i32.wat
   mul_i64.wat

test/sym/memory.t

@@ -8,11 +8,14 @@ memory stuff:
       (symbol_0 (i32 1)))
   Reached problem!
   [13]
-  $ dune exec owi -- sym store.wat
-  Trap: out of bounds memory access
-  Model:
-    (model
-      (symbol_0 (i32 -11))
-      (symbol_1 (i32 0)))
-  Reached problem!
-  [13]
+# Deactivated because it is currently an enumeration of all i32s with the forced concretization
+#  $ dune exec owi -- sym store.wat
+#  Trap: out of bounds memory access
+#  Model:
+#    (model
+#      (symbol_0 (i32 -11))
+#      (symbol_1 (i32 0)))
+#  Reached problem!
+#  [1]
+  $ dune exec owi -- sym memory2.wat
+  All OK

test/sym/memory2.wat

@@ -0,0 +1,31 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume" (func $assume (param i32)))
+  (import "symbolic" "assert" (func $assert (param i32)))
+
+  (memory $m 1)
+  (data (offset (i32.const 0)) "\00\01\02\03")
+
+  (func $start
+
+    (local $n i32)
+
+    (local.set $n (call $i32_symbol))
+
+    (call $assume   ;; 0 <= i32 < 4
+      (i32.and
+        (i32.ge_u (local.get $n) (i32.const 0))
+        (i32.lt_u (local.get $n) (i32.const 4))
+        )
+    )
+
+    (call $assert
+      (i32.eq
+        (i32.load8_u (local.get $n))
+        (local.get $n)
+      )
+    )
+  )
+
+  (start $start)
+)