From 644aa499f73aa81eb78a437c153899a9aa180659 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Fri, 5 Jul 2024 16:36:54 +0200 Subject: [PATCH] Pass memory to external functions `malloc` and `free` --- src/concolic/concolic_wasm_ffi.ml | 35 ++++++++------------------ src/intf/wasm_ffi_intf.ml | 6 +++-- src/symbolic/symbolic_wasm_ffi.ml | 42 +++++++++++++------------------ 3 files changed, 32 insertions(+), 51 deletions(-) diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index 455250f1d..e1cba8924 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/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 diff --git a/src/intf/wasm_ffi_intf.ml b/src/intf/wasm_ffi_intf.ml index 5732f36e3..2581a802b 100644 --- a/src/intf/wasm_ffi_intf.ml +++ b/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 diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index e8ffd012e..da589cb4a 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/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) )