Deactivate memory tracking once freed

CHANGES.md

@@ -1,5 +1,6 @@
 ## unreleased
 
+- Change `free` prototype to now return a pointer on which tracking is deactivated
 - add `--emit-file` option to `wasm2wat` to emit .wat files
 - adds flags `--fail-on-trap-only` and `fail-on-assertion-only`
 - parameterize the `Thread` module on the symbolic memory and the `Choice_monad` module on a Thread

src/concolic/concolic_wasm_ffi.ml

@@ -132,10 +132,11 @@ module M :
           ; symbolic = Expr.ptr base (Symbolic_value.const_i32 0l)
           } )
 
-  let free _ (p : Value.int32) : unit Choice.t =
+  let free _ (p : Value.int32) =
     (* WHAT ???? *)
-    let _base = ptr p in
-    Choice.return ()
+    let open Choice in
+    let+ base = ptr p in
+    Value.const_i32 base
 end
 
 type extern_func = Concolic.P.Extern_func.extern_func
@@ -179,7 +180,7 @@ let summaries_extern_module =
           (Func (Mem (Arg (I32, Arg (I32, Res))), R1 I32), alloc) )
     ; ( "dealloc"
       , Concolic.P.Extern_func.Extern_func
-          (Func (Mem (Arg (I32, Res)), R0), free) )
+          (Func (Mem (Arg (I32, Res)), R1 I32), free) )
     ; ("abort", Concolic.P.Extern_func.Extern_func (Func (UArg Res, R0), abort))
     ]
   in

src/intf/symbolic_memory_intf.ml

@@ -26,7 +26,7 @@ module type M = sig
     -> 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 free : t -> Smtml.Expr.t -> Smtml.Expr.t Symbolic_choice_without_memory.t
 end
 
 module type S = sig
@@ -49,7 +49,8 @@ module type S = sig
     -> 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 free :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
 
   val load_8_s :
     t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t

src/intf/wasm_ffi_intf.ml

@@ -39,7 +39,7 @@ module type S0 = sig
 
   val alloc : memory -> Value.int32 -> Value.int32 -> Value.int32 t
 
-  val free : memory -> Value.int32 -> unit t
+  val free : memory -> Value.int32 -> Value.int32 t
 
   val exit : Value.int32 -> unit t
 end

src/libc/include/owi.h

@@ -3,7 +3,7 @@
 
 __attribute__((import_module("summaries"), import_name("alloc"))) void *
 owi_malloc(void *, unsigned int);
-__attribute__((import_module("summaries"), import_name("dealloc"))) void
+__attribute__((import_module("summaries"), import_name("dealloc"))) void *
 owi_free(void *);
 
 __attribute__((import_module("symbolic"), import_name("i8_symbol"))) char

src/symbolic/symbolic_memory_concretizing.ml

@@ -134,7 +134,8 @@ module Backend = struct
     let+ base = ptr p in
     if not @@ Hashtbl.mem m.chunks base then
       Fmt.failwith "Memory leak double free";
-    Hashtbl.remove m.chunks base
+    Hashtbl.remove m.chunks base;
+    Symbolic_value.const_i32 base
 
   let realloc m ~ptr ~size =
     let open Symbolic_choice_without_memory in

src/symbolic/symbolic_wasm_ffi.ml

@@ -48,7 +48,7 @@ module M :
   let alloc m (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
     Choice.lift_mem @@ Memory.realloc m ~ptr:base ~size
 
-  let free m (ptr : Value.int32) : unit Choice.t =
+  let free m (ptr : Value.int32) : Value.int32 Choice.t =
     Choice.lift_mem @@ Memory.free m ptr
 
   let exit (_p : Value.int32) : unit Choice.t = abort ()
@@ -98,7 +98,7 @@ let summaries_extern_module =
           (Func (Mem (Arg (I32, Arg (I32, Res))), R1 I32), alloc) )
     ; ( "dealloc"
       , Symbolic.P.Extern_func.Extern_func
-          (Func (Mem (Arg (I32, Res)), R0), free) )
+          (Func (Mem (Arg (I32, Res)), R1 I32), 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) )