Create parametric symbolic memory functor

Parameterizes symbolic memory on an abstract backend with arbitrary
address types. Implements a concrete backend that always concretizes
symbolic expressions to concrete addresses.

src/dune

@@ -67,6 +67,9 @@
   symbolic_choice_without_memory
   symbolic_global
   symbolic_memory
+  symbolic_memory_concretizing
+  symbolic_memory_intf
+  symbolic_memory_make
   symbolic_table
   symbolic_value
   symbolic_wasm_ffi

src/intf/symbolic_memory_intf.ml

@@ -0,0 +1,138 @@
+module type M = sig
+  type t
+
+  type address
+
+  val address : Smtml.Expr.t -> address Symbolic_choice_without_memory.t
+
+  val address_i32 : Int32.t -> address
+
+  val make : unit -> t
+
+  val clone : t -> t
+
+  val loadn : t -> address -> int -> Smtml.Expr.t
+
+  val storen : t -> address -> Smtml.Expr.t -> int -> unit
+
+  val validate_address :
+       t
+    -> Smtml.Expr.t
+    -> (Smtml.Expr.t, Trap.t) result Symbolic_choice_without_memory.t
+
+  val realloc :
+       t
+    -> ptr:Smtml.Expr.t
+    -> size:Smtml.Expr.t
+    -> Smtml.Expr.t Symbolic_choice_without_memory.t
+
+  val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
+end
+
+module type S = sig
+  type t
+
+  type collection
+
+  val init : unit -> collection
+
+  val clone : collection -> collection
+
+  val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
+
+  (* val check_within_bounds : *)
+  (*   t -> Smtml.Expr.t -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result *)
+
+  val realloc :
+       t
+    -> ptr:Smtml.Expr.t
+    -> size:Smtml.Expr.t
+    -> Smtml.Expr.t Symbolic_choice_without_memory.t
+
+  val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
+
+  val load_8_s :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_8_u :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_16_s :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_16_u :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_32 :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_64 :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val store_8 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val store_16 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val store_32 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val store_64 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val grow : t -> Smtml.Expr.t -> unit
+
+  val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
+
+  val blit :
+       t
+    -> src:Smtml.Expr.t
+    -> dst:Smtml.Expr.t
+    -> len:Smtml.Expr.t
+    -> Smtml.Expr.t
+
+  val blit_string :
+       t
+    -> string
+    -> src:Smtml.Expr.t
+    -> dst:Smtml.Expr.t
+    -> len:Smtml.Expr.t
+    -> Smtml.Expr.t
+
+  val size : t -> Smtml.Expr.t
+
+  val size_in_pages : t -> Smtml.Expr.t
+
+  val get_limit_max : t -> Smtml.Expr.t option
+
+  module ITbl : sig
+    type 'a t
+
+    type key
+
+    val iter : (key -> 'a -> unit) -> 'a t -> unit
+  end
+
+  val iter : (t ITbl.t -> unit) -> collection -> unit
+end
+
+module type Intf = sig
+  module type M = M
+
+  module type S = S
+
+  module Make (_ : M) : S
+end

src/symbolic/symbolic.ml

@@ -3,15 +3,15 @@
 (* Written by the Owi programmers *)
 
 module MakeP
-    (Thread : Thread.S with type Memory.collection = Symbolic_memory.collection)
+    (Memory : Symbolic_memory_intf.S)
+    (Thread : Thread.S with type Memory.collection = Memory.collection)
     (Choice : Choice_intf.Complete
                 with module V := Symbolic_value
                  and type thread := Thread.t) =
 struct
   module Value = Symbolic_value
   module Choice = Choice
-  module Extern_func =
-    Concrete_value.Make_extern_func (Value) (Choice) (Symbolic_memory)
+  module Extern_func = Concrete_value.Make_extern_func (Value) (Choice) (Memory)
   module Global = Symbolic_global
   module Table = Symbolic_table
 
@@ -44,60 +44,27 @@ struct
   end
 
   module Memory = struct
-    include Symbolic_memory
+    include Memory
 
-    let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t =
-      let open Choice in
-      let open Smtml in
-      match Expr.view a with
-      (* Avoid unecessary re-hashconsing and allocation when the value
-         is already concrete. *)
-      | Val _ | Ptr { offset = { node = Val _; _ }; _ } -> return a
-      | Ptr { base; offset } ->
-        let+ offset = select_i32 offset in
-        Expr.ptr base (Symbolic_value.const_i32 offset)
-      | _ ->
-        let+ v = select_i32 a in
-        Symbolic_value.const_i32 v
-
-    let check_within_bounds m a =
-      match check_within_bounds m a with
-      | Error t -> Choice.trap t
-      | Ok (cond, ptr) ->
-        let open Choice in
-        let* out_of_bounds = select cond in
-        if out_of_bounds then trap Trap.Memory_heap_buffer_overflow
-        else return ptr
-
-    let with_concrete (m : t) a f : 'a Choice.t =
-      let open Choice in
-      let* addr = concretise a in
-      let+ ptr = check_within_bounds m addr in
-      f m ptr
-
-    let load_8_s m a = with_concrete m a load_8_s
+    let load_8_s m a = Choice.lift_mem @@ load_8_s m a
 
-    let load_8_u m a = with_concrete m a load_8_u
+    let load_8_u m a = Choice.lift_mem @@ load_8_u m a
 
-    let load_16_s m a = with_concrete m a load_16_s
+    let load_16_s m a = Choice.lift_mem @@ load_16_s m a
 
-    let load_16_u m a = with_concrete m a load_16_u
+    let load_16_u m a = Choice.lift_mem @@ load_16_u m a
 
-    let load_32 m a = with_concrete m a load_32
+    let load_32 m a = Choice.lift_mem @@ load_32 m a
 
-    let load_64 m a = with_concrete m a load_64
+    let load_64 m a = Choice.lift_mem @@ load_64 m a
 
-    let store_8 m ~addr v =
-      with_concrete m addr (fun m addr -> store_8 m ~addr v)
+    let store_8 m ~addr v = Choice.lift_mem @@ store_8 m ~addr v
 
-    let store_16 m ~addr v =
-      with_concrete m addr (fun m addr -> store_16 m ~addr v)
+    let store_16 m ~addr v = Choice.lift_mem @@ store_16 m ~addr v
 
-    let store_32 m ~addr v =
-      with_concrete m addr (fun m addr -> store_32 m ~addr v)
+    let store_32 m ~addr v = Choice.lift_mem @@ store_32 m ~addr v
 
-    let store_64 m ~addr v =
-      with_concrete m addr (fun m addr -> store_64 m ~addr v)
+    let store_64 m ~addr v = Choice.lift_mem @@ store_64 m ~addr v
   end
 
   module Data = struct
@@ -115,7 +82,7 @@ struct
       let orig_mem = Link_env.get_memory env id in
       let f (t : thread) =
         let memories = Thread.memories t in
-        Symbolic_memory.get_memory (Link_env.id env) orig_mem memories id
+        Memory.get_memory (Link_env.id env) orig_mem memories id
       in
       Choice.with_thread f
 
@@ -169,9 +136,11 @@ struct
 end
 
 module P =
-  MakeP [@inlined hint] (Thread_with_memory) (Symbolic_choice_with_memory)
+  MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory)
+    (Symbolic_choice_with_memory)
 module M =
-  MakeP [@inlined hint] (Thread_with_memory) (Symbolic_choice_minimalist)
+  MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory)
+    (Symbolic_choice_minimalist)
 
 let convert_module_to_run (m : 'f Link.module_to_run) =
   P.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run }

src/symbolic/symbolic_memory.ml

@@ -197,7 +197,7 @@ let free m base =
     Fmt.failwith "Memory leak double free";
   Hashtbl.remove m.chunks base
 
-let replace_size m base size = Hashtbl.replace m.chunks base size
+let realloc m base size = Hashtbl.replace m.chunks base size
 
 module ITbl = Hashtbl.Make (struct
   include Int

src/symbolic/symbolic_memory.mli

@@ -15,7 +15,7 @@ val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
 val check_within_bounds :
   t -> Smtml.Expr.t -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result
 
-val replace_size : t -> Int32.t -> Smtml.Expr.t -> unit
+val realloc : t -> Int32.t -> Smtml.Expr.t -> unit
 
 val free : t -> Int32.t -> unit