wip

src/dune

@@ -70,6 +70,7 @@
   symbolic_memory_concretizing
   symbolic_memory_intf
   symbolic_memory_make
+  symbolic_memory_memsight
   symbolic_table
   symbolic_value
   symbolic_wasm_ffi

src/symbolic/symbolic.ml

@@ -136,10 +136,10 @@ struct
 end
 
 module P =
-  MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory)
+  MakeP [@inlined hint] (Symbolic_memory_memsight) (Thread_with_memory)
     (Symbolic_choice_with_memory)
 module M =
-  MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory)
+  MakeP [@inlined hint] (Symbolic_memory_memsight) (Thread_with_memory)
     (Symbolic_choice_minimalist)
 
 let convert_module_to_run (m : 'f Link.module_to_run) =

src/symbolic/symbolic_memory_memsight.ml

@@ -0,0 +1,78 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+[@@@warning "-69"]
+
+module Memsight_backend = struct
+  open Smtml
+  open Symbolic_choice_without_memory
+
+  type address = Symbolic_value.int32
+
+  type record =
+    { address : address
+    ; value : Symbolic_value.int32
+    ; condition : Symbolic_value.vbool
+    ; time : int
+    }
+
+  type t =
+    { mutable records : record list
+    ; mutable time : int
+    }
+
+  let make () = { records = []; time = 0 }
+
+  let clone { records; time } = { records; time }
+
+  let address a = return a
+
+  let address_i32 i = Symbolic_value.const_i32 i
+
+  let loadn mem addr _n =
+    let open Symbolic_value in
+    let v = const_i32 0l in
+    List.fold_right
+      (fun r acc ->
+        Bool.select_expr
+          (Bool.and_ (I32.eq addr r.address) r.condition)
+          ~if_true:r.value ~if_false:acc )
+      mem.records v
+
+  let storen mem addr v _n =
+    mem.time <- succ mem.time;
+    let record =
+      { address = addr
+      ; value = v
+      ; condition = Smtml.Expr.Bool.true_
+      ; time = mem.time
+      }
+    in
+    mem.records <- record :: mem.records
+
+  let validate_address _m a = return (Ok a)
+
+  let free _ _ =
+    Fmt.epr "TODO: Symbolic_memory.free@.";
+    return ()
+
+  let realloc _m ~ptr ~size:_ =
+    Fmt.epr "TODO: Symbolic_memory.replace_size@.";
+    let+ base = select_i32 ptr in
+    Expr.ptr base (Symbolic_value.const_i32 0l)
+
+  let pp_record fmt { address; value; condition; time } =
+    Fmt.pf fmt "%a, %a, %a, %d" Expr.pp address Expr.pp value Expr.pp condition
+      time
+
+  let pp fmt { time; records; _ } =
+    Fmt.pf fmt "Time: %d@;" time;
+    Fmt.pf fmt "Records:@;  @[<v 2>%a@]"
+      (Fmt.list (Fmt.parens pp_record))
+      records
+end
+
+module Memsight_backend' : Symbolic_memory_intf.M = Memsight_backend
+
+include Symbolic_memory_make.Make (Memsight_backend)

src/symbolic/thread_with_memory.ml

@@ -2,7 +2,7 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-include Thread.Make (Symbolic_memory_concretizing)
+include Thread.Make (Symbolic_memory_memsight)
 
 let project (th : t) : Thread_without_memory.t * _ =
   let projected =
@@ -25,7 +25,7 @@ let restore backup th =
   let pc = Thread_without_memory.pc th in
   let memories =
     if Thread_without_memory.memories th then
-      Symbolic_memory_concretizing.clone backup
+      Symbolic_memory_memsight.clone backup
     else backup
   in
   let tables = Thread_without_memory.tables th in

src/symbolic/thread_with_memory.mli

@@ -4,7 +4,7 @@
 
 (** @inline *)
 include
-  Thread.S with type Memory.collection = Symbolic_memory_concretizing.collection
+  Thread.S with type Memory.collection = Symbolic_memory_memsight.collection
 
 val project : t -> Thread_without_memory.t * Memory.collection
 

test/sym/memory/basic_store_load_single_address_01.wat

@@ -9,6 +9,7 @@
     i32.const 0x00000000
     i32.const 0x50ffc001
     i32.store
+    call $dump_memory
     i32.const 0x00000000
     i32.load
     i32.const 0x50ffc001