From 66580620eb10ea96c31e9a95d8c823a10994347c Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 31 Jul 2024 13:17:20 +0200 Subject: [PATCH] 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 | 93 +++++++++++++++++++ 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, 156 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 3b449742b..fee633be9 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 f86403592..754b9fd2a 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..a69291019 --- /dev/null +++ b/src/symbolic/symbolic_memory_memsight.ml @@ -0,0 +1,93 @@ +(* 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 _ _ = + Fmt.epr "TODO: Symbolic_memory.free@."; + return () + + let realloc _m ~ptr ~size:_ = + (* Fmt.epr "TODO: Symbolic_memory.replace_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