Pass memory to external functions malloc and free

CHANGES.md

@@ -1,5 +1,6 @@
 ## unreleased
 
+- adds a `Mem` argument to external function to allow direct manipulation of the memory.
 - support other solvers through the `--solver` option (Z3, Colibri2, Bitwuzla and CVC5)
 - support the extended constant expressions proposal
 - `owi opt` and `owi sym` can run on `.wasm` files directly

src/concolic/concolic_wasm_ffi.ml

@@ -4,14 +4,18 @@
 
 module Expr = Smtml.Expr
 module Choice = Concolic.P.Choice
+module Memory = Concolic.P.Memory
 
 (* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *)
 module M :
   Wasm_ffi_intf.S0
     with type 'a t = 'a Choice.t
+     and type memory = Memory.t
      and module Value = Concolic_value.V = struct
   type 'a t = 'a Choice.t
 
+  type memory = Memory.t
+
   module Value = Concolic_value.V
 
   let symbol_i32 () : Value.int32 Choice.t =
@@ -107,35 +111,17 @@ module M :
     ignore p;
     abort ()
 
-  let alloc (base : Value.int32) (_size : Value.int32) : Value.int32 Choice.t =
+  let alloc _ (base : Value.int32) (_size : Value.int32) : Value.int32 Choice.t
+      =
     Choice.bind (i32 base) (fun (base : int32) ->
         Choice.return
           { Concolic_value.concrete = base
           ; symbolic = Expr.ptr base (Symbolic_value.const_i32 0l)
           } )
-  (* WHAT ???? *)
-  (* Choice.with_thread (fun t : Value.int32 -> *)
-  (*     let memories = t.shared.memories in *)
-  (*     Symbolic_memory.iter *)
-  (*       (fun tbl -> *)
-  (*         Symbolic_memory.ITbl.iter *)
-  (*           (fun _ (m : Symbolic_memory.t) -> *)
-  (*             Symbolic_memory.replace_size m base size.s ) *)
-  (*           tbl ) *)
-  (*       memories; *)
-  (*     { c = base; s = Expr.make (Ptr (base, Symbolic_value.const_i32 0l)) }) *)
-
-  let free (p : Value.int32) : unit Choice.t =
+
+  let free _ (p : Value.int32) : unit Choice.t =
     (* WHAT ???? *)
     let _base = ptr p in
-    (* Choice.with_thread (fun t -> *)
-    (*     let memories = t.shared.memories in *)
-    (*     Symbolic_memory.iter *)
-    (*       (fun tbl -> *)
-    (*         Symbolic_memory.ITbl.iter *)
-    (*           (fun _ (m : Symbolic_memory.t) -> Symbolic_memory.free m base) *)
-    (*           tbl ) *)
-    (*       memories ) *)
     Choice.return ()
 end
 
@@ -177,9 +163,10 @@ let summaries_extern_module =
   let functions =
     [ ( "alloc"
       , Concolic.P.Extern_func.Extern_func
-          (Func (Arg (I32, Arg (I32, Res)), R1 I32), alloc) )
+          (Func (Mem (Arg (I32, Arg (I32, Res))), R1 I32), alloc) )
     ; ( "dealloc"
-      , Concolic.P.Extern_func.Extern_func (Func (Arg (I32, Res), R0), free) )
+      , Concolic.P.Extern_func.Extern_func
+          (Func (Mem (Arg (I32, Res)), R0), free) )
     ; ("abort", Concolic.P.Extern_func.Extern_func (Func (UArg Res, R0), abort))
     ]
   in

src/intf/wasm_ffi_intf.ml

@@ -5,6 +5,8 @@
 module type S0 = sig
   type 'a t
 
+  type memory
+
   module Value : sig
     type int32
 
@@ -33,9 +35,9 @@ module type S0 = sig
 
   val abort : unit -> unit t
 
-  val alloc : Value.int32 -> Value.int32 -> Value.int32 t
+  val alloc : memory -> Value.int32 -> Value.int32 -> Value.int32 t
 
-  val free : Value.int32 -> unit t
+  val free : memory -> Value.int32 -> unit t
 
   val exit : Value.int32 -> unit t
 end

src/symbolic/symbolic_wasm_ffi.ml

@@ -4,14 +4,18 @@
 
 module Expr = Smtml.Expr
 module Choice = Symbolic_choice
+module Memory = Symbolic_memory
 
 (* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *)
 module M :
   Wasm_ffi_intf.S0
     with type 'a t = 'a Choice.t
+     and type memory = Memory.t
      and module Value = Symbolic_value = struct
   type 'a t = 'a Choice.t
 
+  type memory = Memory.t
+
   module Value = Symbolic_value
 
   let assume_i32 (i : Value.int32) : unit Choice.t =
@@ -53,29 +57,16 @@ module M :
       Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v;
       Choice.bind (abort ()) (fun () -> assert false)
 
-  let alloc (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
-    Choice.bind (i32 base) (fun base ->
-        Choice.with_thread (fun t ->
-            let memories = Thread.memories t in
-            Symbolic_memory.iter
-              (fun tbl ->
-                Symbolic_memory.ITbl.iter
-                  (fun _ (m : Symbolic_memory.t) ->
-                    Symbolic_memory.replace_size m base size )
-                  tbl )
-              memories;
-            Expr.ptr base (Value.const_i32 0l) ) )
-
-  let free (p : Value.int32) : unit Choice.t =
-    Choice.bind (ptr p) (fun base ->
-        Choice.with_thread (fun t ->
-            let memories = Thread.memories t in
-            Symbolic_memory.iter
-              (fun tbl ->
-                Symbolic_memory.ITbl.iter
-                  (fun _ (m : Symbolic_memory.t) -> Symbolic_memory.free m base)
-                  tbl )
-              memories ) )
+  let alloc m (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
+    let open Choice in
+    let+ base = i32 base in
+    Memory.replace_size m base size;
+    Expr.ptr base (Value.const_i32 0l)
+
+  let free m (p : Value.int32) : unit Choice.t =
+    let open Choice in
+    let+ base = ptr p in
+    Memory.free m base
 
   let exit (p : Value.int32) : unit Choice.t =
     ignore p;
@@ -120,9 +111,10 @@ let summaries_extern_module =
   let functions =
     [ ( "alloc"
       , Symbolic.P.Extern_func.Extern_func
-          (Func (Arg (I32, Arg (I32, Res)), R1 I32), alloc) )
+          (Func (Mem (Arg (I32, Arg (I32, Res))), R1 I32), alloc) )
     ; ( "dealloc"
-      , Symbolic.P.Extern_func.Extern_func (Func (Arg (I32, Res), R0), free) )
+      , Symbolic.P.Extern_func.Extern_func
+          (Func (Mem (Arg (I32, Res)), R0), free) )
     ; ("abort", Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R0), abort))
     ; ( "exit"
       , Symbolic.P.Extern_func.Extern_func (Func (Arg (I32, Res), R0), exit) )