Adds memsight memory model

src/cmd/cmd_sym.ml

@@ -26,8 +26,12 @@ let link_state =
        Link.extern_module' Link.empty_state ~name:"symbolic" ~func_typ
          Symbolic_wasm_ffi.symbolic_extern_module
      in
-     Link.extern_module' link_state ~name:"summaries" ~func_typ
-       Symbolic_wasm_ffi.summaries_extern_module )
+     let link_state =
+       Link.extern_module' link_state ~name:"summaries" ~func_typ
+         Symbolic_wasm_ffi.summaries_extern_module
+     in
+     Link.extern_module' link_state ~name:"introspection" ~func_typ
+       Symbolic_wasm_ffi.introspection_extern_module )
 
 let run_file ~unsafe ~optimize pc filename =
   let*/ m = Compile.File.until_typecheck ~unsafe filename in

src/concolic/concolic_wasm_ffi.ml

@@ -184,3 +184,7 @@ let summaries_extern_module =
     ]
   in
   { Link.functions }
+
+let introspection_extern_module =
+  let functions = [] in
+  { Link.functions }

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/intf/symbolic_memory_intf.ml

@@ -27,6 +27,8 @@ module type M = sig
     -> Smtml.Expr.t Symbolic_choice_without_memory.t
 
   val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
+
+  val pp : Fmt.formatter -> t -> unit
 end
 
 module type S = sig
@@ -118,6 +120,8 @@ module type S = sig
 
   val get_limit_max : t -> Smtml.Expr.t option
 
+  val pp : Fmt.formatter -> t -> unit
+
   module ITbl : sig
     type 'a t
 

src/intf/wasm_ffi_intf.ml

@@ -50,4 +50,6 @@ module type S = sig
   val symbolic_extern_module : extern_func Link.extern_module
 
   val summaries_extern_module : extern_func Link.extern_module
+
+  val introspection_extern_module : extern_func Link.extern_module
 end

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.ml

@@ -197,6 +197,18 @@ let free m base =
 
 let realloc m base size = Hashtbl.replace m.chunks base size
 
+let pp fmt m =
+  let pp_parent v =
+    Fmt.option
+      ~none:(fun fmt () -> Fmt.string fmt "None")
+      (fun fmt _v -> Fmt.string fmt "Some")
+      v
+  in
+  let pp_v fmt (a, b) = Fmt.pf fmt "0x%08ld %a" a Expr.pp b in
+  Fmt.pf fmt "size: %a@;" Expr.pp m.size;
+  Fmt.pf fmt "parent: %a@;" pp_parent m.parent;
+  Fmt.pf fmt "data:@;  @[<v>%a@]" (Fmt.hashtbl pp_v) m.data
+
 module ITbl = Hashtbl.Make (struct
   include Int
 

src/symbolic/symbolic_memory.mli

@@ -60,6 +60,8 @@ val size_in_pages : t -> Smtml.Expr.t
 
 val get_limit_max : t -> Smtml.Expr.t option
 
+val pp : Fmt.formatter -> t -> unit
+
 module ITbl : sig
   type 'a t
 

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
@@ -141,6 +93,14 @@ module Backend = struct
     let+ base = address ptr in
     Hashtbl.replace m.chunks base size;
     Expr.ptr base (Symbolic_value.const_i32 0l)
+
+  let rec pp fmt m =
+    let pp_parent =
+      Fmt.option ~none:(fun fmt () -> Fmt.string fmt "None (root mem)") pp
+    in
+    let pp_v fmt (a, b) = Fmt.pf fmt "0x%08lx %a" a Expr.pp b in
+    Fmt.pf fmt "@[<v>parent:@;@[<v 1> %a@]@;data:@;@[<v 1> %a@]@]" pp_parent
+      m.parent (Fmt.hashtbl pp_v) m.data
 end
 
 include Symbolic_memory_make.Make (Backend)

src/symbolic/symbolic_memory_make.ml

@@ -131,6 +131,10 @@ module Make (Backend : M) = struct
 
   let realloc m ~ptr ~size = Backend.realloc m.data ~ptr ~size
 
+  let pp fmt m =
+    Fmt.pf fmt "@[<v 1>Memory:@;size: %a@;backend:@;@[<v 1> %a@]@]"
+      Smtml.Expr.pp m.size Backend.pp m.data
+
   (* TODO: Move this into a separate module? *)
   module ITbl = Hashtbl.Make (struct
     include Int

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/symbolic_wasm_ffi.ml

@@ -105,3 +105,23 @@ let summaries_extern_module =
     ]
   in
   { Link.functions }
+
+let introspection_extern_module =
+  let dump_memory m : unit Choice.t =
+    Fmt.epr "%a@." Memory.pp m;
+    Choice.return ()
+  in
+
+  let print_i32 i32 : Symbolic_value.int32 Choice.t =
+    Fmt.pr "Print: %a@." Smtml.Expr.pp i32;
+    Choice.return i32
+  in
+  let functions =
+    [ ( "dump_memory"
+      , Symbolic.P.Extern_func.Extern_func (Func (Mem Res, R0), dump_memory) )
+    ; ( "print_i32"
+      , Symbolic.P.Extern_func.Extern_func
+          (Func (Arg (I32, Res), R1 I32), print_i32) )
+    ]
+  in
+  { Link.functions }

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