wip

src/dune

@@ -67,9 +67,11 @@
   symbolic_choice_without_memory
   symbolic_global
   symbolic_memory
+  symbolic_memory_base
   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_base.ml

@@ -0,0 +1,50 @@
+open Smtml
+
+(* TODO: These functions should be in smtml *)
+
+(* TODO: don't rebuild so many values it generates unecessary hc lookups *)
+let merge_extracts (e1, h, m1) (e2, m2, l) =
+  let ty = Expr.ty e1 in
+  if m1 = m2 && Expr.equal e1 e2 then
+    if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l))
+  else
+    Expr.(make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))))
+
+let concat ~msb ~lsb offset =
+  assert (offset > 0 && offset <= 8);
+  match (Expr.view msb, Expr.view lsb) with
+  | Val (Num (I8 i1)), Val (Num (I8 i2)) ->
+    Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
+  | Val (Num (I8 i1)), Val (Num (I32 i2)) ->
+    let offset = offset * 8 in
+    if offset < 32 then
+      Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2)
+    else
+      let i1' = Int64.of_int i1 in
+      let i2' = Int64.of_int32 i2 in
+      Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
+  | Val (Num (I8 i1)), Val (Num (I64 i2)) ->
+    let offset = Int64.of_int (offset * 8) in
+    Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
+  | Extract (e1, h, m1), Extract (e2, m2, l) ->
+    merge_extracts (e1, h, m1) (e2, m2, l)
+  | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
+    Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)))
+  | _ -> Expr.make (Concat (msb, lsb))
+
+let extract v pos =
+  match Expr.view v with
+  | Val (Num (I8 _)) -> v
+  | Val (Num (I32 i)) ->
+    let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
+    Expr.value (Num (I8 i'))
+  | Val (Num (I64 i)) ->
+    let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
+    Expr.value (Num (I8 i'))
+  | Cvtop
+      (_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
+  | Cvtop
+      (_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
+    ->
+    sym
+  | _ -> Expr.make (Extract (v, pos + 1, pos))

src/symbolic/symbolic_memory_concretizing.ml

@@ -1,5 +1,6 @@
 module Backend = struct
   open Smtml
+  include Symbolic_memory_base
 
   type address = Int32.t
 
@@ -36,65 +37,16 @@ module Backend = struct
       | None -> Expr.value (Num (I8 0))
       | Some parent -> load_byte parent a )
 
-  (* TODO: don't rebuild so many values it generates unecessary hc lookups *)
-  let merge_extracts (e1, h, m1) (e2, m2, l) =
-    let ty = Expr.ty e1 in
-    if m1 = m2 && Expr.equal e1 e2 then
-      if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l))
-    else
-      Expr.(
-        make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) )
-
-  let concat ~msb ~lsb offset =
-    assert (offset > 0 && offset <= 8);
-    match (Expr.view msb, Expr.view lsb) with
-    | Val (Num (I8 i1)), Val (Num (I8 i2)) ->
-      Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
-    | Val (Num (I8 i1)), Val (Num (I32 i2)) ->
-      let offset = offset * 8 in
-      if offset < 32 then
-        Symbolic_value.const_i32
-          Int32.(logor (shl (of_int i1) (of_int offset)) i2)
-      else
-        let i1' = Int64.of_int i1 in
-        let i2' = Int64.of_int32 i2 in
-        Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
-    | Val (Num (I8 i1)), Val (Num (I64 i2)) ->
-      let offset = Int64.of_int (offset * 8) in
-      Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
-    | Extract (e1, h, m1), Extract (e2, m2, l) ->
-      merge_extracts (e1, h, m1) (e2, m2, l)
-    | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
-      Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)))
-    | _ -> Expr.make (Concat (msb, lsb))
-
   let loadn m a n =
-    let rec loop addr size i acc =
-      if i = size then acc
+    let rec loop addr i acc =
+      if i = n then acc
       else
         let addr' = Int32.(add addr (of_int i)) in
         let byte = load_byte m addr' in
-        loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
+        loop addr (i + 1) (concat i ~msb:byte ~lsb:acc)
     in
     let v0 = load_byte m a in
-    loop a n 1 v0
-
-  let extract v pos =
-    match Expr.view v with
-    | Val (Num (I8 _)) -> v
-    | Val (Num (I32 i)) ->
-      let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
-      Expr.value (Num (I8 i'))
-    | Val (Num (I64 i)) ->
-      let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
-      Expr.value (Num (I8 i'))
-    | Cvtop
-        (_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
-    | Cvtop
-        (_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
-      ->
-      sym
-    | _ -> Expr.make (Extract (v, pos + 1, pos))
+    loop a 1 v0
 
   let storen m a v n =
     for i = 0 to n - 1 do

src/symbolic/symbolic_memory_memsight.ml

@@ -0,0 +1,90 @@
+(* 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
+  include Symbolic_memory_base
+
+  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 load_byte mem addr =
+    let open Symbolic_value in
+    let v = Expr.value (Num (I8 0)) 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 loadn mem addr n =
+    let open Symbolic_value in
+    let rec loop i acc =
+      if i = n then acc
+      else
+        let addr' = I32.add addr (const_i32 (Int32.of_int i)) in
+        let byte = load_byte mem addr' in
+        loop (i + 1) (concat i ~msb:byte ~lsb:acc)
+    in
+    loop 1 (load_byte mem addr)
+
+  let storen mem addr v n =
+    let open Symbolic_value in
+    mem.time <- succ mem.time;
+    for i = n - 1 downto 0 do
+      let record =
+        { address = I32.add addr (const_i32 (Int32.of_int i))
+        ; value = extract v i
+        ; condition = Bool.const true
+        ; time = mem.time
+        }
+      in
+      mem.records <- record :: mem.records
+    done
+
+  let validate_address _m a = return (Ok a)
+
+  let free _ _ = return ()
+
+  let realloc _m ~ptr ~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