diff --git a/CHANGES.md b/CHANGES.md index a54f67b75..af9304922 100644 --- a/CHANGES.md +++ b/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 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) )