From d23288e37427d4cb0c637fd06cecaa1b2f1d8e32 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 27 Jun 2024 16:42:56 +0200 Subject: [PATCH] wip --- src/cmd/cmd_sym.ml | 25 +-- src/concolic/concolic_wasm_ffi.ml | 4 + src/intf/wasm_ffi_intf.ml | 2 + src/symbolic/symbolic.ml | 53 ++---- src/symbolic/symbolic.old.ml | 189 ++++++++++++++++++++++ src/symbolic/symbolic_memory.ml | 241 ++++++++-------------------- src/symbolic/symbolic_memory.mli | 4 +- src/symbolic/symbolic_memory.old.ml | 241 ++++++++++++++++++++++++++++ src/symbolic/symbolic_wasm_ffi.ml | 27 ++++ test/sym/memory/store_load.wat | 26 +++ 10 files changed, 586 insertions(+), 226 deletions(-) create mode 100644 src/symbolic/symbolic.old.ml create mode 100644 src/symbolic/symbolic_memory.old.ml create mode 100644 test/sym/memory/store_load.wat diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 1c916a308..0827bae8e 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -17,8 +17,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:"debug" ~func_typ + Symbolic_wasm_ffi.debug_extern_module ) let run_binary_modul ~unsafe ~optimize (pc : unit Result.t Choice.t) (m : Binary.modul) = @@ -81,9 +85,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values Format.pp_std "Assert failure: %a@\n" Expr.pp assertion; Format.pp_std "Model:@\n @[%a@]@." (Smtml.Model.pp ~no_values) model in - let rec print_and_count_failures count_acc results = + let rec print_and_count_failures (failures_acc, paths_acc) results = match results () with - | Seq.Nil -> Ok count_acc + | Seq.Nil -> Ok (failures_acc, paths_acc) | Seq.Cons ((result, _thread), tl) -> let* model = let open Symbolic_choice in @@ -98,7 +102,8 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values failwith "unreachable: callback should have filtered eval ok out." | EVal (Error e) -> Error e in - let count_acc = succ count_acc in + let paths_acc = succ paths_acc in + let failures_acc = succ failures_acc in let* () = if not no_values then let testcase = @@ -107,8 +112,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values Cmd_utils.write_testcase ~dir:workspace testcase else Ok () in - if no_stop_at_failure then print_and_count_failures count_acc tl - else Ok count_acc + if no_stop_at_failure then + print_and_count_failures (failures_acc, paths_acc) tl + else Ok (failures_acc, paths_acc) in let results = if deterministic_result_order then @@ -121,8 +127,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values |> List.to_seq |> Seq.map fst else results in - let* count = print_and_count_failures 0 results in - if count > 0 then Error (`Found_bug count) + let* failures, paths = print_and_count_failures (0, 0) results in + Format.pp_std "Completed paths: %d@." paths; + if failures > 0 then Error (`Found_bug failures) else begin Format.pp_std "All OK"; Ok () diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index 455250f1d..68046374a 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 debug_extern_module = + let functions = [] in + { Link.functions } diff --git a/src/intf/wasm_ffi_intf.ml b/src/intf/wasm_ffi_intf.ml index 5732f36e3..a8a3d3c2f 100644 --- a/src/intf/wasm_ffi_intf.ml +++ b/src/intf/wasm_ffi_intf.ml @@ -46,4 +46,6 @@ module type S = sig val symbolic_extern_module : extern_func Link.extern_module val summaries_extern_module : extern_func Link.extern_module + + val debug_extern_module : extern_func Link.extern_module end diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml index 841edc337..52aed5291 100644 --- a/src/symbolic/symbolic.ml +++ b/src/symbolic/symbolic.ml @@ -57,58 +57,25 @@ struct module Memory = struct include Symbolic_memory - let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t = - let open Choice in - let open Smtml in - match Expr.view a with - (* Avoid unecessary re-hashconsing and allocation when the value - is already concrete. *) - | Val _ | Ptr { offset = { node = Val _; _ }; _ } -> return a - | Ptr { base; offset } -> - let+ offset = select_i32 offset in - Expr.ptr base (Symbolic_value.const_i32 offset) - | _ -> - let+ v = select_i32 a in - Symbolic_value.const_i32 v - - let check_within_bounds m a = - match check_within_bounds m a with - | Error t -> Choice.trap t - | Ok (cond, ptr) -> - let open Choice in - let* out_of_bounds = select cond in - if out_of_bounds then trap Trap.Memory_heap_buffer_overflow - else return ptr - - let with_concrete (m : t) a f : 'a Choice.t = - let open Choice in - let* addr = concretise a in - let+ ptr = check_within_bounds m addr in - f m ptr - - let load_8_s m a = with_concrete m a load_8_s + let load_8_s m a = Choice.return @@ load_8_s m a - let load_8_u m a = with_concrete m a load_8_u + let load_8_u m a = Choice.return @@ load_8_u m a - let load_16_s m a = with_concrete m a load_16_s + let load_16_s m a = Choice.return @@ load_16_s m a - let load_16_u m a = with_concrete m a load_16_u + let load_16_u m a = Choice.return @@ load_16_u m a - let load_32 m a = with_concrete m a load_32 + let load_32 m a = Choice.return @@ load_32 m a - let load_64 m a = with_concrete m a load_64 + let load_64 m a = Choice.return @@ load_64 m a - let store_8 m ~addr v = - with_concrete m addr (fun m addr -> store_8 m ~addr v) + let store_8 m ~addr v = Choice.return @@ store_8 m ~addr v - let store_16 m ~addr v = - with_concrete m addr (fun m addr -> store_16 m ~addr v) + let store_16 m ~addr v = Choice.return @@ store_16 m ~addr v - let store_32 m ~addr v = - with_concrete m addr (fun m addr -> store_32 m ~addr v) + let store_32 m ~addr v = Choice.return @@ store_32 m ~addr v - let store_64 m ~addr v = - with_concrete m addr (fun m addr -> store_64 m ~addr v) + let store_64 m ~addr v = Choice.return @@ store_64 m ~addr v end module Data = struct diff --git a/src/symbolic/symbolic.old.ml b/src/symbolic/symbolic.old.ml new file mode 100644 index 000000000..bb6bed299 --- /dev/null +++ b/src/symbolic/symbolic.old.ml @@ -0,0 +1,189 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +module type Thread = sig + type t + + val memories : t -> Symbolic_memory.collection + + val tables : t -> Symbolic_table.collection + + val globals : t -> Symbolic_global.collection + + val pc : t -> Symbolic_value.vbool list +end + +module MakeP + (Thread : Thread) + (Choice : Choice_intf.Complete + with module V := Symbolic_value + and type thread := Thread.t) = +struct + module Value = Symbolic_value + module Choice = Choice + module Extern_func = Concrete_value.Make_extern_func (Value) (Choice) + module Global = Symbolic_global + module Table = Symbolic_table + + type thread = Thread.t + + let select (c : Value.vbool) ~(if_true : Value.t) ~(if_false : Value.t) : + Value.t Choice.t = + match (if_true, if_false) with + | I32 if_true, I32 if_false -> + Choice.return (Value.I32 (Value.Bool.select_expr c ~if_true ~if_false)) + | I64 if_true, I64 if_false -> + Choice.return (Value.I64 (Value.Bool.select_expr c ~if_true ~if_false)) + | F32 if_true, F32 if_false -> + Choice.return (Value.F32 (Value.Bool.select_expr c ~if_true ~if_false)) + | F64 if_true, F64 if_false -> + Choice.return (Value.F64 (Value.Bool.select_expr c ~if_true ~if_false)) + | Ref _, Ref _ -> + let open Choice in + let+ b = select c in + if b then if_true else if_false + | _, _ -> assert false + + module Elem = struct + type t = Link_env.elem + + let get (elem : t) i : Value.ref_value = + match elem.value.(i) with Funcref f -> Funcref f | _ -> assert false + + let size (elem : t) = Array.length elem.value + end + + module Memory = struct + include Symbolic_memory + + let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t = + let open Choice in + let open Smtml in + match Expr.view a with + (* Avoid unecessary re-hashconsing and allocation when the value + is already concrete. *) + | Val _ | Ptr { offset = { node = Val _; _ }; _ } -> return a + | Ptr { base; offset } -> + let+ offset = select_i32 offset in + Expr.ptr base (Symbolic_value.const_i32 offset) + | _ -> + let+ v = select_i32 a in + Symbolic_value.const_i32 v + + let check_within_bounds m a = + match is_out_of_bounds m a with + | Error t -> Choice.trap t + | Ok (cond, ptr) -> + let open Choice in + let* out_of_bounds = select cond in + if out_of_bounds then trap Trap.Memory_heap_buffer_overflow + else return ptr + + let with_concrete (m : t) a f : 'a Choice.t = + let open Choice in + let* addr = concretise a in + let+ ptr = check_within_bounds m addr in + f m ptr + + let load_8_s m a = with_concrete m a load_8_s + + let load_8_u m a = with_concrete m a load_8_u + + let load_16_s m a = with_concrete m a load_16_s + + let load_16_u m a = with_concrete m a load_16_u + + let load_32 m a = with_concrete m a load_32 + + let load_64 m a = with_concrete m a load_64 + + let store_8 m ~addr v = + with_concrete m addr (fun m addr -> store_8 m ~addr v) + + let store_16 m ~addr v = + with_concrete m addr (fun m addr -> store_16 m ~addr v) + + let store_32 m ~addr v = + with_concrete m addr (fun m addr -> store_32 m ~addr v) + + let store_64 m ~addr v = + with_concrete m addr (fun m addr -> store_64 m ~addr v) + end + + module Data = struct + type t = Link_env.data + + let value data = data.Link_env.value + end + + module Env = struct + type t = Extern_func.extern_func Link_env.t + + type t' = Env_id.t + + let get_memory env id = + let orig_mem = Link_env.get_memory env id in + let f (t : thread) = + let memories = Thread.memories t in + Symbolic_memory.get_memory (Link_env.id env) orig_mem memories id + in + Choice.with_thread f + + let get_func = Link_env.get_func + + let get_extern_func = Link_env.get_extern_func + + let get_table (env : t) i : Table.t Choice.t = + let orig_table = Link_env.get_table env i in + let f (t : thread) = + let tables = Thread.tables t in + Symbolic_table.get_table (Link_env.id env) orig_table tables i + in + Choice.with_thread f + + let get_elem env i = Link_env.get_elem env i + + let get_data env n = + let data = Link_env.get_data env n in + Choice.return data + + let get_global (env : t) i : Global.t Choice.t = + let orig_global = Link_env.get_global env i in + let f (t : thread) = + let globals = Thread.globals t in + Symbolic_global.get_global (Link_env.id env) orig_global globals i + in + Choice.with_thread f + + let drop_elem _ = + (* TODO *) + () + + let drop_data = Link_env.drop_data + end + + module Module_to_run = struct + (** runnable module *) + type t = + { modul : Binary.modul + ; env : Env.t + ; to_run : Types.binary Types.expr list + } + + let env (t : t) = t.env + + let modul (t : t) = t.modul + + let to_run (t : t) = t.to_run + end +end + +module P = MakeP [@inlined hint] (Thread) (Symbolic_choice) +module M = MakeP [@inlined hint] (Thread) (Symbolic_choice_minimalist) + +let convert_module_to_run (m : 'f Link.module_to_run) = + P.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run } + +let convert_module_to_run_minimalist (m : 'f Link.module_to_run) = + M.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run } diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index 3ac62f85e..e2c9f8964 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -2,41 +2,29 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -module Value = Symbolic_value -module Expr = Smtml.Expr -module Ty = Smtml.Ty -open Expr +[@@@warning "-69"] let page_size = Symbolic_value.const_i32 65_536l -type t = - { data : (Int32.t, Value.int32) Hashtbl.t - ; parent : t option - ; mutable size : Value.int32 - ; chunks : (Int32.t, Value.int32) Hashtbl.t +type record = + { address : Symbolic_value.int32 + ; value : Symbolic_value.int32 + ; condition : Symbolic_value.int32 + ; time : int } -let create size = - { data = Hashtbl.create 128 - ; parent = None - ; size = Value.const_i32 size - ; chunks = Hashtbl.create 16 +type t = + { size : Symbolic_value.int32 + ; mutable records : record list + ; mutable time : int } -let i32 v = - match view v with - | Val (Num (I32 i)) -> i - | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v +let create size = + { size = Symbolic_value.const_i32 size; records = []; time = 0 } -let grow m delta = - let old_size = Value.I32.mul m.size page_size in - let new_size = Value.I32.(div (add old_size delta) page_size) in - m.size <- - Value.Bool.select_expr - (Value.I32.gt new_size m.size) - ~if_true:new_size ~if_false:m.size +let grow _m _delta = assert false -let size { size; _ } = Value.I32.mul size page_size +let size { size; _ } = Symbolic_value.I32.mul size page_size let size_in_pages { size; _ } = size @@ -44,158 +32,65 @@ let fill _ = assert false let blit _ = assert false -let blit_string m str ~src ~dst ~len = - (* This function is only used in memory init so everything will be concrete *) - let str_len = String.length str in - let mem_len = Int32.(to_int (i32 m.size) * to_int (i32 page_size)) in - let src = Int32.to_int @@ i32 src in - let dst = Int32.to_int @@ i32 dst in - let len = Int32.to_int @@ i32 len in - if src < 0 || dst < 0 || len < 0 || src + len > str_len || dst + len > mem_len - then Value.Bool.const true - else begin - for i = 0 to len - 1 do - let byte = Char.code @@ String.get str (src + i) in - let dst = Int32.of_int (dst + i) in - Hashtbl.replace m.data dst (make (Val (Num (I8 byte)))) - done; - Value.Bool.const false - end - -let clone m = - { data = Hashtbl.create 16 - ; parent = Some m - ; size = m.size - ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) - } +let blit_string _m _str ~src:_ ~dst:_ ~len:_ = assert false + +let clone _ = assert false + +let load_8_s _ = assert false + +let load_8_u _ = assert false + +let load_16_s _ = assert false + +let load_16_u _ = assert false -let rec load_byte { parent; data; _ } a = - try Hashtbl.find data a - with Not_found -> ( - match parent with - | None -> make (Val (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 make (Extract (e1, h, l)) - else make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) - -let concat ~msb ~lsb offset = - assert (offset > 0 && offset <= 8); - match (view msb, view lsb) with - | Val (Num (I8 i1)), Val (Num (I8 i2)) -> - 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 - 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 - 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 - 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) -> - make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)) - | _ -> make (Concat (msb, lsb)) - -let loadn m a n = - let rec loop addr size i acc = - if i = size 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) +let load_32 mem addr = + let open Symbolic_value in + let v = const_i32 0l 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 load_64 _ = assert false + +let store_8 _ ~addr:_ _ = assert false + +let store_16 _ ~addr:_ _ = assert false + +let store_32 mem ~addr v = + mem.time <- succ mem.time; + let record = + { address = addr + ; value = v + ; condition = Smtml.Expr.Bool.true_ + ; time = mem.time + } in - let v0 = load_byte m a in - loop a n 1 v0 - -let load_8_s m a = - let v = loadn m (i32 a) 1 in - match view v with - | Val (Num (I8 i8)) -> Value.const_i32 (Int32.extend_s 8 (Int32.of_int i8)) - | _ -> cvtop (Ty_bitv 32) (Sign_extend 24) v - -let load_8_u m a = - let v = loadn m (i32 a) 1 in - match view v with - | Val (Num (I8 i)) -> Value.const_i32 (Int32.of_int i) - | _ -> cvtop (Ty_bitv 32) (Zero_extend 24) v - -let load_16_s m a = - let v = loadn m (i32 a) 2 in - match view v with - | Val (Num (I32 i16)) -> Value.const_i32 (Int32.extend_s 16 i16) - | _ -> cvtop (Ty_bitv 32) (Sign_extend 16) v - -let load_16_u m a = - let v = loadn m (i32 a) 2 in - match view v with - | Val (Num (I32 _)) -> v - | _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v - -let load_32 m a = loadn m (i32 a) 4 - -let load_64 m a = loadn m (i32 a) 8 - -let extract v pos = - match view v with - | Val (Num (I32 i)) -> - let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in - value (Num (I8 i')) - | Val (Num (I64 i)) -> - let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in - value (Num (I8 i')) - | Cvtop (_, Zero_extend 24, ({ node = Symbol _; _ } as sym)) - | Cvtop (_, Sign_extend 24, ({ node = Symbol _; _ } as sym)) - when ty sym = Ty_bitv 8 -> - sym - | _ -> make (Extract (v, pos + 1, pos)) - -let storen m ~addr v n = - let a0 = i32 addr in - for i = 0 to n - 1 do - let addr' = Int32.add a0 (Int32.of_int i) in - let v' = extract v i in - Hashtbl.replace m.data addr' v' - done - -let store_8 m ~addr v = storen m ~addr v 1 - -let store_16 m ~addr v = storen m ~addr v 2 - -let store_32 m ~addr v = storen m ~addr v 4 - -let store_64 m ~addr v = storen m ~addr v 8 + mem.records <- record :: mem.records + +let store_64 _ ~addr:_ _ = assert false let get_limit_max _m = None (* TODO *) -let check_within_bounds m a = - match view a with - | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) - | Ptr { base; offset } -> ( - match Hashtbl.find m.chunks base with - | exception Not_found -> Error Trap.Memory_leak_use_after_free - | size -> - let ptr = Int32.add base (i32 offset) in - let upper_bound = - Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) - in - Ok (Value.Bool.(or_ (const (ptr < base)) upper_bound), Value.const_i32 ptr) - ) - | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a - -let free m base = - if not @@ Hashtbl.mem m.chunks base then failwith "Memory leak double free"; - Hashtbl.remove m.chunks base - -let replace_size m base size = Hashtbl.replace m.chunks base size +let is_out_of_bounds _ = assert false + +let free _ = assert false + +let replace_size _ = assert false + +let pp_v = Smtml.Expr.pp + +let pp_record fmt { address; value; condition; time } = + Format.pp fmt "(%a, %a, %a, %d)" pp_v address pp_v value pp_v condition time + +let pp fmt { time; records; _ } = + Format.pp fmt "Time: %d@\n" time; + Format.pp fmt "Records:@\n@[ %a@]" + (Format.pp_list ~pp_sep:Format.pp_newline pp_record) + records module ITbl = Hashtbl.Make (struct include Int diff --git a/src/symbolic/symbolic_memory.mli b/src/symbolic/symbolic_memory.mli index 276272885..a5759ff01 100644 --- a/src/symbolic/symbolic_memory.mli +++ b/src/symbolic/symbolic_memory.mli @@ -12,7 +12,7 @@ val clone : collection -> collection val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t -val check_within_bounds : +val is_out_of_bounds : t -> Smtml.Expr.t -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result val replace_size : t -> Int32.t -> Smtml.Expr.t -> unit @@ -60,6 +60,8 @@ val size_in_pages : t -> Smtml.Expr.t val get_limit_max : t -> Smtml.Expr.t option +val pp : Format.formatter -> t -> unit + module ITbl : sig type 'a t diff --git a/src/symbolic/symbolic_memory.old.ml b/src/symbolic/symbolic_memory.old.ml new file mode 100644 index 000000000..d8ae4a7f1 --- /dev/null +++ b/src/symbolic/symbolic_memory.old.ml @@ -0,0 +1,241 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +module Value = Symbolic_value +module Expr = Smtml.Expr +module Ty = Smtml.Ty +open Expr + +let page_size = Symbolic_value.const_i32 65_536l + +type t = + { data : (Int32.t, Value.int32) Hashtbl.t + ; parent : t option + ; mutable size : Value.int32 + ; chunks : (Int32.t, Value.int32) Hashtbl.t + } + +let create size = + { data = Hashtbl.create 128 + ; parent = None + ; size = Value.const_i32 size + ; chunks = Hashtbl.create 16 + } + +let i32 v = + match view v with + | Val (Num (I32 i)) -> i + | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v + +let grow m delta = + let old_size = Value.I32.mul m.size page_size in + let new_size = Value.I32.(div (add old_size delta) page_size) in + m.size <- + Value.Bool.select_expr + (Value.I32.gt new_size m.size) + ~if_true:new_size ~if_false:m.size + +let size { size; _ } = Value.I32.mul size page_size + +let size_in_pages { size; _ } = size + +let fill _ = assert false + +let blit _ = assert false + +let blit_string m str ~src ~dst ~len = + (* This function is only used in memory init so everything will be concrete *) + let str_len = String.length str in + let mem_len = Int32.(to_int (i32 m.size) * to_int (i32 page_size)) in + let src = Int32.to_int @@ i32 src in + let dst = Int32.to_int @@ i32 dst in + let len = Int32.to_int @@ i32 len in + if src < 0 || dst < 0 || len < 0 || src + len > str_len || dst + len > mem_len + then Value.Bool.const true + else begin + for i = 0 to len - 1 do + let byte = Char.code @@ String.get str (src + i) in + let dst = Int32.of_int (dst + i) in + Hashtbl.replace m.data dst (make (Val (Num (I8 byte)))) + done; + Value.Bool.const false + end + +let clone m = + { data = Hashtbl.create 16 + ; parent = Some m + ; size = m.size + ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) + } + +let rec load_byte { parent; data; _ } a = + try Hashtbl.find data a + with Not_found -> ( + match parent with + | None -> make (Val (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 make (Extract (e1, h, l)) + else make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) + +let concat ~msb ~lsb offset = + assert (offset > 0 && offset <= 8); + match (view msb, view lsb) with + | Val (Num (I8 i1)), Val (Num (I8 i2)) -> + 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 + 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 + 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 + 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) -> + make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)) + | _ -> make (Concat (msb, lsb)) + +let loadn m a n = + let rec loop addr size i acc = + if i = size 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) + in + let v0 = load_byte m a in + loop a n 1 v0 + +let load_8_s m a = + let v = loadn m (i32 a) 1 in + match view v with + | Val (Num (I8 i8)) -> Value.const_i32 (Int32.extend_s 8 (Int32.of_int i8)) + | _ -> cvtop (Ty_bitv 32) (Sign_extend 24) v + +let load_8_u m a = + let v = loadn m (i32 a) 1 in + match view v with + | Val (Num (I8 i)) -> Value.const_i32 (Int32.of_int i) + | _ -> cvtop (Ty_bitv 32) (Zero_extend 24) v + +let load_16_s m a = + let v = loadn m (i32 a) 2 in + match view v with + | Val (Num (I32 i16)) -> Value.const_i32 (Int32.extend_s 16 i16) + | _ -> cvtop (Ty_bitv 32) (Sign_extend 16) v + +let load_16_u m a = + let v = loadn m (i32 a) 2 in + match view v with + | Val (Num (I32 _)) -> v + | _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v + +let load_32 m a = loadn m (i32 a) 4 + +let load_64 m a = loadn m (i32 a) 8 + +let extract v pos = + match view v with + | Val (Num (I32 i)) -> + let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in + value (Num (I8 i')) + | Val (Num (I64 i)) -> + let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in + value (Num (I8 i')) + | Cvtop (_, Zero_extend 24, ({ node = Symbol _; _ } as sym)) + | Cvtop (_, Sign_extend 24, ({ node = Symbol _; _ } as sym)) + when ty sym = Ty_bitv 8 -> + sym + | _ -> make (Extract (v, pos + 1, pos)) + +let storen m ~addr v n = + let a0 = i32 addr in + for i = 0 to n - 1 do + let addr' = Int32.add a0 (Int32.of_int i) in + let v' = extract v i in + Hashtbl.replace m.data addr' v' + done + +let store_8 m ~addr v = storen m ~addr v 1 + +let store_16 m ~addr v = storen m ~addr v 2 + +let store_32 m ~addr v = storen m ~addr v 4 + +let store_64 m ~addr v = storen m ~addr v 8 + +let get_limit_max _m = None (* TODO *) + +let is_out_of_bounds m a = + match view a with + | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) + | Ptr { base; offset } -> ( + match Hashtbl.find m.chunks base with + | exception Not_found -> Error Trap.Memory_leak_use_after_free + | size -> + let ptr = Int32.add base (i32 offset) in + let upper_bound = + Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) + in + Ok (Value.Bool.(or_ (const (ptr < base)) upper_bound), Value.const_i32 ptr) + ) + | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a + +let free m base = + if not @@ Hashtbl.mem m.chunks base then failwith "Memory leak double free"; + Hashtbl.remove m.chunks base + +let replace_size m base size = Hashtbl.replace m.chunks base size + +module ITbl = Hashtbl.Make (struct + include Int + + let hash x = x +end) + +type collection = t ITbl.t Env_id.Tbl.t + +let init () = Env_id.Tbl.create 0 + +let iter f collection = Env_id.Tbl.iter (fun _ tbl -> f tbl) collection + +let clone collection = + (* TODO: this is ugly and should be rewritten *) + let s = Env_id.Tbl.to_seq collection in + Env_id.Tbl.of_seq + @@ Seq.map + (fun (i, t) -> + let s = ITbl.to_seq t in + (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone a)) s) ) + s + +let convert (orig_mem : Concrete_memory.t) : t = + let s = Concrete_memory.size_in_pages orig_mem in + create s + +let get_env env_id memories = + match Env_id.Tbl.find_opt memories env_id with + | Some env -> env + | None -> + let t = ITbl.create 0 in + Env_id.Tbl.add memories env_id t; + t + +let get_memory env_id (orig_memory : Concrete_memory.t) collection g_id = + let env = get_env env_id collection in + match ITbl.find_opt env g_id with + | Some t -> t + | None -> + let t = convert orig_memory in + ITbl.add env g_id t; + t diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index e8ffd012e..45dce7330 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -129,3 +129,30 @@ let summaries_extern_module = ] in { Link.functions } + +let debug_extern_module = + let dump_memory () : unit Choice.t = + 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) -> + Format.pp_err "Memory:@\n@[ %a@]@." Symbolic_memory.pp m + ) + tbl ) + memories ) + in + let print_i32 i32 : Symbolic_value.int32 Choice.t = + Format.pp_std "Print: %a@." Smtml.Expr.pp i32; + Choice.return i32 + in + let functions = + [ ( "dump_memory" + , Symbolic.P.Extern_func.Extern_func (Func (UArg 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/store_load.wat b/test/sym/memory/store_load.wat new file mode 100644 index 000000000..ec0c196a2 --- /dev/null +++ b/test/sym/memory/store_load.wat @@ -0,0 +1,26 @@ +(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 "debug" "dump_memory" (func $dump_memory)) + (import "debug" "print_i32" (func $print_i32 (param i32) (result i32))) + + (memory $m 1) + + (func $start + (local $x i32) + i32.const 42 + i32.const 0xdeadc0de + i32.store + + call $dump_memory + + i32.const 42 + i32.load + call $print_i32 + i32.const 0xdeadc0de + i32.eq + call $assert + ) + (start $start))