From bbeaa765f4a3f698461920de82544c723d7787f8 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Tue, 30 Jul 2024 12:46:35 +0200 Subject: [PATCH 1/2] Add basic memory tests and introspection external functions --- src/cmd/cmd_sym.ml | 8 +++- src/concolic/concolic_wasm_ffi.ml | 4 ++ src/intf/symbolic_memory_intf.ml | 4 ++ src/intf/wasm_ffi_intf.ml | 2 + src/symbolic/symbolic_memory.ml | 12 ++++++ src/symbolic/symbolic_memory.mli | 2 + src/symbolic/symbolic_memory_concretizing.ml | 8 ++++ src/symbolic/symbolic_memory_make.ml | 4 ++ src/symbolic/symbolic_wasm_ffi.ml | 20 ++++++++++ .../memory/alloc_dynamic_dealloc_reuse_07.wat | 35 ++++++++++++++++++ .../alloc_dynamic_multiple_blocks_06.wat | 37 +++++++++++++++++++ .../memory/alloc_dynamic_single_block_05.wat | 22 +++++++++++ .../alloc_dynamic_use_after_free_08.wat | 22 +++++++++++ .../memory/basic_load_uninitialized_02.wat | 10 +++++ .../memory/basic_store_last_address_03.wat | 7 ++++ .../basic_store_load_single_address_01.wat | 17 +++++++++ test/sym/memory/basic_store_overflow_04.wat | 7 ++++ 17 files changed, 219 insertions(+), 2 deletions(-) create mode 100644 test/sym/memory/alloc_dynamic_dealloc_reuse_07.wat create mode 100644 test/sym/memory/alloc_dynamic_multiple_blocks_06.wat create mode 100644 test/sym/memory/alloc_dynamic_single_block_05.wat create mode 100644 test/sym/memory/alloc_dynamic_use_after_free_08.wat create mode 100644 test/sym/memory/basic_load_uninitialized_02.wat create mode 100644 test/sym/memory/basic_store_last_address_03.wat create mode 100644 test/sym/memory/basic_store_load_single_address_01.wat create mode 100644 test/sym/memory/basic_store_overflow_04.wat diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 8c1af29cb..b407877fd 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -26,8 +26,12 @@ let link_state = Link.extern_module' Link.empty_state ~name:"symbolic" ~func_typ Symbolic_wasm_ffi.symbolic_extern_module in - Link.extern_module' link_state ~name:"summaries" ~func_typ - Symbolic_wasm_ffi.summaries_extern_module ) + let link_state = + Link.extern_module' link_state ~name:"summaries" ~func_typ + Symbolic_wasm_ffi.summaries_extern_module + in + Link.extern_module' link_state ~name:"introspection" ~func_typ + Symbolic_wasm_ffi.introspection_extern_module ) let run_file ~unsafe ~optimize pc filename = let*/ m = Compile.File.until_typecheck ~unsafe filename in diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index 4a7f16ab7..cece6c1d1 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/src/concolic/concolic_wasm_ffi.ml @@ -184,3 +184,7 @@ let summaries_extern_module = ] in { Link.functions } + +let introspection_extern_module = + let functions = [] in + { Link.functions } diff --git a/src/intf/symbolic_memory_intf.ml b/src/intf/symbolic_memory_intf.ml index 6d690fd8f..505eb8e5c 100644 --- a/src/intf/symbolic_memory_intf.ml +++ b/src/intf/symbolic_memory_intf.ml @@ -27,6 +27,8 @@ module type M = sig -> Smtml.Expr.t Symbolic_choice_without_memory.t val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t + + val pp : Fmt.formatter -> t -> unit end module type S = sig @@ -118,6 +120,8 @@ module type S = sig val get_limit_max : t -> Smtml.Expr.t option + val pp : Fmt.formatter -> t -> unit + module ITbl : sig type 'a t diff --git a/src/intf/wasm_ffi_intf.ml b/src/intf/wasm_ffi_intf.ml index 04c39052c..d2cd342c4 100644 --- a/src/intf/wasm_ffi_intf.ml +++ b/src/intf/wasm_ffi_intf.ml @@ -50,4 +50,6 @@ module type S = sig val symbolic_extern_module : extern_func Link.extern_module val summaries_extern_module : extern_func Link.extern_module + + val introspection_extern_module : extern_func Link.extern_module end diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index 69519e55e..3c89c1860 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -197,6 +197,18 @@ let free m base = let realloc m base size = Hashtbl.replace m.chunks base size +let pp fmt m = + let pp_parent v = + Fmt.option + ~none:(fun fmt () -> Fmt.string fmt "None") + (fun fmt _v -> Fmt.string fmt "Some") + v + in + let pp_v fmt (a, b) = Fmt.pf fmt "0x%08ld %a" a Expr.pp b in + Fmt.pf fmt "size: %a@;" Expr.pp m.size; + Fmt.pf fmt "parent: %a@;" pp_parent m.parent; + Fmt.pf fmt "data:@; @[%a@]" (Fmt.hashtbl pp_v) m.data + module ITbl = Hashtbl.Make (struct include Int diff --git a/src/symbolic/symbolic_memory.mli b/src/symbolic/symbolic_memory.mli index 3c35719fb..b69a81741 100644 --- a/src/symbolic/symbolic_memory.mli +++ b/src/symbolic/symbolic_memory.mli @@ -60,6 +60,8 @@ val size_in_pages : t -> Smtml.Expr.t val get_limit_max : t -> Smtml.Expr.t option +val pp : Fmt.formatter -> t -> unit + module ITbl : sig type 'a t diff --git a/src/symbolic/symbolic_memory_concretizing.ml b/src/symbolic/symbolic_memory_concretizing.ml index e2617d48e..c30a95dbe 100644 --- a/src/symbolic/symbolic_memory_concretizing.ml +++ b/src/symbolic/symbolic_memory_concretizing.ml @@ -141,6 +141,14 @@ module Backend = struct let+ base = address ptr in Hashtbl.replace m.chunks base size; Expr.ptr base (Symbolic_value.const_i32 0l) + + let rec pp fmt m = + let pp_parent = + Fmt.option ~none:(fun fmt () -> Fmt.string fmt "None (root mem)") pp + in + let pp_v fmt (a, b) = Fmt.pf fmt "0x%08lx %a" a Expr.pp b in + Fmt.pf fmt "@[parent:@;@[ %a@]@;data:@;@[ %a@]@]" pp_parent + m.parent (Fmt.hashtbl pp_v) m.data end include Symbolic_memory_make.Make (Backend) diff --git a/src/symbolic/symbolic_memory_make.ml b/src/symbolic/symbolic_memory_make.ml index ae4d0fe1a..b7bbedcb9 100644 --- a/src/symbolic/symbolic_memory_make.ml +++ b/src/symbolic/symbolic_memory_make.ml @@ -131,6 +131,10 @@ module Make (Backend : M) = struct let realloc m ~ptr ~size = Backend.realloc m.data ~ptr ~size + let pp fmt m = + Fmt.pf fmt "@[Memory:@;size: %a@;backend:@;@[ %a@]@]" + Smtml.Expr.pp m.size Backend.pp m.data + (* TODO: Move this into a separate module? *) module ITbl = Hashtbl.Make (struct include Int diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index 3999eb902..6a0ce9bd2 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -105,3 +105,23 @@ let summaries_extern_module = ] in { Link.functions } + +let introspection_extern_module = + let dump_memory m : unit Choice.t = + Fmt.epr "%a@." Memory.pp m; + Choice.return () + in + + let print_i32 i32 : Symbolic_value.int32 Choice.t = + Fmt.pr "Print: %a@." Smtml.Expr.pp i32; + Choice.return i32 + in + let functions = + [ ( "dump_memory" + , Symbolic.P.Extern_func.Extern_func (Func (Mem Res, R0), dump_memory) ) + ; ( "print_i32" + , Symbolic.P.Extern_func.Extern_func + (Func (Arg (I32, Res), R1 I32), print_i32) ) + ] + in + { Link.functions } diff --git a/test/sym/memory/alloc_dynamic_dealloc_reuse_07.wat b/test/sym/memory/alloc_dynamic_dealloc_reuse_07.wat new file mode 100644 index 000000000..02fb498bd --- /dev/null +++ b/test/sym/memory/alloc_dynamic_dealloc_reuse_07.wat @@ -0,0 +1,35 @@ +;; Reuse memory address chunk with different size +(module + (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32))) + (import "summaries" "dealloc" (func $free (param i32))) + (import "symbolic" "assert" (func $assert (param i32))) + (memory $m 1) + (global $__heap_base (mut i32) (i32.const 0x00000000)) + (func $start (local i32) + global.get $__heap_base + i32.const 0x00000004 + call $malloc + local.tee 0 + i32.const 0x0000002a + i32.store + local.get 0 + i32.load + i32.const 0x0000002a + i32.eq + call $assert + local.get 0 + call $free + global.get $__heap_base + i32.const 0x00000008 + call $malloc + local.tee 0 + i32.const 0x00000054 + i32.store + local.get 0 + i32.load + i32.const 0x00000054 + i32.eq + call $assert + local.get 0 + call $free) + (start $start)) diff --git a/test/sym/memory/alloc_dynamic_multiple_blocks_06.wat b/test/sym/memory/alloc_dynamic_multiple_blocks_06.wat new file mode 100644 index 000000000..f0dc3189c --- /dev/null +++ b/test/sym/memory/alloc_dynamic_multiple_blocks_06.wat @@ -0,0 +1,37 @@ +;; Allocate multiple chunks and check that they don't overlap +(module + (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32))) + (import "summaries" "dealloc" (func $free (param i32))) + (import "symbolic" "assert" (func $assert (param i32))) + (memory $m 1) + (global $__heap_base (mut i32) (i32.const 0x00000000)) + (func $start (local i32 i32) + global.get $__heap_base + i32.const 0x00000004 + call $malloc + local.tee 0 + global.get $__heap_base + i32.const 0x00000004 + i32.add + i32.const 0x00000008 + call $malloc + local.tee 1 + i32.const 0x0000000a + i32.store + i32.const 0x0000000b + i32.store + local.get 0 + i32.load + i32.const 0x0000000b + i32.eq + call $assert + local.get 1 + i32.load + i32.const 0x0000000a + i32.eq + call $assert + local.get 1 + call $free + local.get 0 + call $free) + (start $start)) diff --git a/test/sym/memory/alloc_dynamic_single_block_05.wat b/test/sym/memory/alloc_dynamic_single_block_05.wat new file mode 100644 index 000000000..1a3a5b8e7 --- /dev/null +++ b/test/sym/memory/alloc_dynamic_single_block_05.wat @@ -0,0 +1,22 @@ +;; Allocate a memory chunk, store and load same address +(module + (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32))) + (import "summaries" "dealloc" (func $free (param i32))) + (import "symbolic" "assert" (func $assert (param i32))) + (memory $m 1) + (global $__heap_base (mut i32) (i32.const 0x00000000)) + (func $start (local i32) + global.get $__heap_base + i32.const 0x00000004 + call $malloc + local.tee 0 + i32.const 0xdeadbeef + i32.store + local.get 0 + i32.load + i32.const 0xdeadbeef + i32.eq + call $assert + local.get 0 + call $free) + (start $start)) diff --git a/test/sym/memory/alloc_dynamic_use_after_free_08.wat b/test/sym/memory/alloc_dynamic_use_after_free_08.wat new file mode 100644 index 000000000..3a436bc91 --- /dev/null +++ b/test/sym/memory/alloc_dynamic_use_after_free_08.wat @@ -0,0 +1,22 @@ +;; Dereference of a free'd pointer should not be allowed +(module + (import "summaries" "alloc" (func $malloc (param i32 i32) (result i32))) + (import "summaries" "dealloc" (func $free (param i32))) + (import "symbolic" "assert" (func $assert (param i32))) + (memory $m 1) + (global $__heap_base (mut i32) (i32.const 0x00000000)) + (func $start (local i32) + global.get $__heap_base + i32.const 0x00000004 + call $malloc + local.tee 0 + i32.const 0x0000002a + i32.store + local.get 0 + call $free + local.get 0 + i32.load + i32.const 0x0000002a + i32.eq + call $assert) + (start $start)) diff --git a/test/sym/memory/basic_load_uninitialized_02.wat b/test/sym/memory/basic_load_uninitialized_02.wat new file mode 100644 index 000000000..4c1d985b2 --- /dev/null +++ b/test/sym/memory/basic_load_uninitialized_02.wat @@ -0,0 +1,10 @@ +(module + (import "symbolic" "assert" (func $assert (param i32))) + (memory $m 1) + (func $start + i32.const 0x00000000 + i32.load + i32.const 0x00000000 + i32.eq + call $assert) + (start $start)) diff --git a/test/sym/memory/basic_store_last_address_03.wat b/test/sym/memory/basic_store_last_address_03.wat new file mode 100644 index 000000000..3b570ef65 --- /dev/null +++ b/test/sym/memory/basic_store_last_address_03.wat @@ -0,0 +1,7 @@ +(module + (memory $m 1) + (func $start + i32.const 0x0000fffc + i32.const 0xbeefbabe + i32.store) + (start $start)) diff --git a/test/sym/memory/basic_store_load_single_address_01.wat b/test/sym/memory/basic_store_load_single_address_01.wat new file mode 100644 index 000000000..291cb87f8 --- /dev/null +++ b/test/sym/memory/basic_store_load_single_address_01.wat @@ -0,0 +1,17 @@ +(module + (import "symbolic" "i32_symbol" (func $i32_symbol (result i32))) + (import "symbolic" "assume" (func $assume (param i32))) + (import "symbolic" "assert" (func $assert (param i32))) + (import "introspection" "dump_memory" (func $dump_memory)) + (import "introspection" "print_i32" (func $print_i32 (param i32) (result i32))) + (memory $m 1) + (func $start + i32.const 0x00000000 + i32.const 0x50ffc001 + i32.store + i32.const 0x00000000 + i32.load + i32.const 0x50ffc001 + i32.eq + call $assert) + (start $start)) diff --git a/test/sym/memory/basic_store_overflow_04.wat b/test/sym/memory/basic_store_overflow_04.wat new file mode 100644 index 000000000..4fc5d3ed6 --- /dev/null +++ b/test/sym/memory/basic_store_overflow_04.wat @@ -0,0 +1,7 @@ +(module + (memory $m 1) + (func $start + i32.const 0x00010000 + i32.const 0xbaaaaaad + i32.store) + (start $start)) From 590c372679c5525e10fcdc7bed0b996fa6baa4cc Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 31 Jul 2024 13:17:20 +0200 Subject: [PATCH 2/2] wip --- src/dune | 2 + src/symbolic/symbolic.ml | 4 +- src/symbolic/symbolic_memory_base.ml | 50 +++++++++++ src/symbolic/symbolic_memory_concretizing.ml | 58 ++---------- src/symbolic/symbolic_memory_memsight.ml | 90 +++++++++++++++++++ src/symbolic/thread_with_memory.ml | 4 +- src/symbolic/thread_with_memory.mli | 2 +- .../basic_store_load_single_address_01.wat | 1 + 8 files changed, 153 insertions(+), 58 deletions(-) create mode 100644 src/symbolic/symbolic_memory_base.ml create mode 100644 src/symbolic/symbolic_memory_memsight.ml diff --git a/src/dune b/src/dune index cc8e4fad9..436385f3d 100644 --- a/src/dune +++ b/src/dune @@ -67,9 +67,11 @@ symbolic_choice_without_memory symbolic_global symbolic_memory + symbolic_memory_base symbolic_memory_concretizing symbolic_memory_intf symbolic_memory_make + symbolic_memory_memsight symbolic_table symbolic_value symbolic_wasm_ffi diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml index aab9ecc96..4841398d2 100644 --- a/src/symbolic/symbolic.ml +++ b/src/symbolic/symbolic.ml @@ -136,10 +136,10 @@ struct end module P = - MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory) + MakeP [@inlined hint] (Symbolic_memory_memsight) (Thread_with_memory) (Symbolic_choice_with_memory) module M = - MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory) + MakeP [@inlined hint] (Symbolic_memory_memsight) (Thread_with_memory) (Symbolic_choice_minimalist) let convert_module_to_run (m : 'f Link.module_to_run) = diff --git a/src/symbolic/symbolic_memory_base.ml b/src/symbolic/symbolic_memory_base.ml new file mode 100644 index 000000000..7c3047ff0 --- /dev/null +++ b/src/symbolic/symbolic_memory_base.ml @@ -0,0 +1,50 @@ +open Smtml + +(* TODO: These functions should be in smtml *) + +(* TODO: don't rebuild so many values it generates unecessary hc lookups *) +let merge_extracts (e1, h, m1) (e2, m2, l) = + let ty = Expr.ty e1 in + if m1 = m2 && Expr.equal e1 e2 then + if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l)) + else + Expr.(make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l))))) + +let concat ~msb ~lsb offset = + assert (offset > 0 && offset <= 8); + match (Expr.view msb, Expr.view lsb) with + | Val (Num (I8 i1)), Val (Num (I8 i2)) -> + Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2)) + | Val (Num (I8 i1)), Val (Num (I32 i2)) -> + let offset = offset * 8 in + if offset < 32 then + Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2) + else + let i1' = Int64.of_int i1 in + let i2' = Int64.of_int32 i2 in + Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2') + | Val (Num (I8 i1)), Val (Num (I64 i2)) -> + let offset = Int64.of_int (offset * 8) in + Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2) + | Extract (e1, h, m1), Extract (e2, m2, l) -> + merge_extracts (e1, h, m1) (e2, m2, l) + | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) -> + Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))) + | _ -> Expr.make (Concat (msb, lsb)) + +let extract v pos = + match Expr.view v with + | Val (Num (I8 _)) -> v + | Val (Num (I32 i)) -> + let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in + Expr.value (Num (I8 i')) + | Val (Num (I64 i)) -> + let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in + Expr.value (Num (I8 i')) + | Cvtop + (_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) + | Cvtop + (_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) + -> + sym + | _ -> Expr.make (Extract (v, pos + 1, pos)) diff --git a/src/symbolic/symbolic_memory_concretizing.ml b/src/symbolic/symbolic_memory_concretizing.ml index c30a95dbe..27d40c2be 100644 --- a/src/symbolic/symbolic_memory_concretizing.ml +++ b/src/symbolic/symbolic_memory_concretizing.ml @@ -1,5 +1,6 @@ module Backend = struct open Smtml + include Symbolic_memory_base type address = Int32.t @@ -36,65 +37,16 @@ module Backend = struct | None -> Expr.value (Num (I8 0)) | Some parent -> load_byte parent a ) - (* TODO: don't rebuild so many values it generates unecessary hc lookups *) - let merge_extracts (e1, h, m1) (e2, m2, l) = - let ty = Expr.ty e1 in - if m1 = m2 && Expr.equal e1 e2 then - if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l)) - else - Expr.( - make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) ) - - let concat ~msb ~lsb offset = - assert (offset > 0 && offset <= 8); - match (Expr.view msb, Expr.view lsb) with - | Val (Num (I8 i1)), Val (Num (I8 i2)) -> - Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2)) - | Val (Num (I8 i1)), Val (Num (I32 i2)) -> - let offset = offset * 8 in - if offset < 32 then - Symbolic_value.const_i32 - Int32.(logor (shl (of_int i1) (of_int offset)) i2) - else - let i1' = Int64.of_int i1 in - let i2' = Int64.of_int32 i2 in - Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2') - | Val (Num (I8 i1)), Val (Num (I64 i2)) -> - let offset = Int64.of_int (offset * 8) in - Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2) - | Extract (e1, h, m1), Extract (e2, m2, l) -> - merge_extracts (e1, h, m1) (e2, m2, l) - | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) -> - Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))) - | _ -> Expr.make (Concat (msb, lsb)) - let loadn m a n = - let rec loop addr size i acc = - if i = size then acc + let rec loop addr i acc = + if i = n then acc else let addr' = Int32.(add addr (of_int i)) in let byte = load_byte m addr' in - loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc) + loop addr (i + 1) (concat i ~msb:byte ~lsb:acc) in let v0 = load_byte m a in - loop a n 1 v0 - - let extract v pos = - match Expr.view v with - | Val (Num (I8 _)) -> v - | Val (Num (I32 i)) -> - let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in - Expr.value (Num (I8 i')) - | Val (Num (I64 i)) -> - let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in - Expr.value (Num (I8 i')) - | Cvtop - (_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) - | Cvtop - (_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) - -> - sym - | _ -> Expr.make (Extract (v, pos + 1, pos)) + loop a 1 v0 let storen m a v n = for i = 0 to n - 1 do diff --git a/src/symbolic/symbolic_memory_memsight.ml b/src/symbolic/symbolic_memory_memsight.ml new file mode 100644 index 000000000..5a1ee9a87 --- /dev/null +++ b/src/symbolic/symbolic_memory_memsight.ml @@ -0,0 +1,90 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +[@@@warning "-69"] + +module Memsight_backend = struct + open Smtml + open Symbolic_choice_without_memory + include Symbolic_memory_base + + type address = Symbolic_value.int32 + + type record = + { address : address + ; value : Symbolic_value.int32 + ; condition : Symbolic_value.vbool + ; time : int + } + + type t = + { mutable records : record list + ; mutable time : int + } + + let make () = { records = []; time = 0 } + + let clone { records; time } = { records; time } + + let address a = return a + + let address_i32 i = Symbolic_value.const_i32 i + + let load_byte mem addr = + let open Symbolic_value in + let v = Expr.value (Num (I8 0)) in + List.fold_right + (fun r acc -> + Bool.select_expr + (Bool.and_ (I32.eq addr r.address) r.condition) + ~if_true:r.value ~if_false:acc ) + mem.records v + + let loadn mem addr n = + let open Symbolic_value in + let rec loop i acc = + if i = n then acc + else + let addr' = I32.add addr (const_i32 (Int32.of_int i)) in + let byte = load_byte mem addr' in + loop (i + 1) (concat i ~msb:byte ~lsb:acc) + in + loop 1 (load_byte mem addr) + + let storen mem addr v n = + let open Symbolic_value in + mem.time <- succ mem.time; + for i = n - 1 downto 0 do + let record = + { address = I32.add addr (const_i32 (Int32.of_int i)) + ; value = extract v i + ; condition = Bool.const true + ; time = mem.time + } + in + mem.records <- record :: mem.records + done + + let validate_address _m a = return (Ok a) + + let free _ _ = return () + + let realloc _m ~ptr ~size:_ = + let+ base = select_i32 ptr in + Expr.ptr base (Symbolic_value.const_i32 0l) + + let pp_record fmt { address; value; condition; time } = + Fmt.pf fmt "%a, %a, %a, %d" Expr.pp address Expr.pp value Expr.pp condition + time + + let pp fmt { time; records; _ } = + Fmt.pf fmt "Time: %d@;" time; + Fmt.pf fmt "Records:@; @[%a@]" + (Fmt.list (Fmt.parens pp_record)) + records +end + +module Memsight_backend' : Symbolic_memory_intf.M = Memsight_backend + +include Symbolic_memory_make.Make (Memsight_backend) diff --git a/src/symbolic/thread_with_memory.ml b/src/symbolic/thread_with_memory.ml index 887c476f7..3940edac0 100644 --- a/src/symbolic/thread_with_memory.ml +++ b/src/symbolic/thread_with_memory.ml @@ -2,7 +2,7 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -include Thread.Make (Symbolic_memory_concretizing) +include Thread.Make (Symbolic_memory_memsight) let project (th : t) : Thread_without_memory.t * _ = let projected = @@ -25,7 +25,7 @@ let restore backup th = let pc = Thread_without_memory.pc th in let memories = if Thread_without_memory.memories th then - Symbolic_memory_concretizing.clone backup + Symbolic_memory_memsight.clone backup else backup in let tables = Thread_without_memory.tables th in diff --git a/src/symbolic/thread_with_memory.mli b/src/symbolic/thread_with_memory.mli index 7a3f88649..a4492e67d 100644 --- a/src/symbolic/thread_with_memory.mli +++ b/src/symbolic/thread_with_memory.mli @@ -4,7 +4,7 @@ (** @inline *) include - Thread.S with type Memory.collection = Symbolic_memory_concretizing.collection + Thread.S with type Memory.collection = Symbolic_memory_memsight.collection val project : t -> Thread_without_memory.t * Memory.collection diff --git a/test/sym/memory/basic_store_load_single_address_01.wat b/test/sym/memory/basic_store_load_single_address_01.wat index 291cb87f8..b748a0068 100644 --- a/test/sym/memory/basic_store_load_single_address_01.wat +++ b/test/sym/memory/basic_store_load_single_address_01.wat @@ -9,6 +9,7 @@ i32.const 0x00000000 i32.const 0x50ffc001 i32.store + call $dump_memory i32.const 0x00000000 i32.load i32.const 0x50ffc001