From d0dd6b6a75b195c4b06f12deee5a5f324a4aa511 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Fri, 5 Jul 2024 19:11:29 +0200 Subject: [PATCH 1/3] Start making memory parametric --- src/dune | 1 + src/symbolic/symbolic_memory.ml | 404 ++++++++++++++------------- src/symbolic/symbolic_memory_intf.ml | 25 ++ 3 files changed, 241 insertions(+), 189 deletions(-) create mode 100644 src/symbolic/symbolic_memory_intf.ml diff --git a/src/dune b/src/dune index 4fa1fca25..671016abf 100644 --- a/src/dune +++ b/src/dune @@ -64,6 +64,7 @@ symbolic_choice_minimalist symbolic_global symbolic_memory + symbolic_memory_intf symbolic_table symbolic_value symbolic_wasm_ffi diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index dca85d11c..f7aac703a 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -9,195 +9,221 @@ 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 Smtml.Ty.equal (Ty_bitv 8) (ty sym) -> - 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 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 (Int32.lt 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 - Fmt.failwith "Memory leak double free"; - Hashtbl.remove m.chunks base - -let replace_size m base size = Hashtbl.replace m.chunks base size +module Backend : Symbolic_memory_intf.M = struct + type address = Int32.t + + type t = + { data : (address, Value.int32) Hashtbl.t + ; parent : t option + ; chunks : (address, Value.int32) Hashtbl.t + } + + let create () = + { data = Hashtbl.create 128; parent = None; chunks = Hashtbl.create 16 } + + let clone m = + { data = Hashtbl.create 16 + ; parent = Some m + ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) + } + + let address v = + match view v with + | Val (Num (I32 i)) -> i + | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v + + 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 extract v pos = + match 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 + 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 Smtml.Ty.equal (Ty_bitv 8) (ty sym) -> + sym + | _ -> make (Extract (v, pos + 1, pos)) + + let storen m addr v n = + for i = 0 to n - 1 do + let addr' = Int32.add addr (Int32.of_int i) in + let v' = extract v i in + Hashtbl.replace m.data addr' v' + done + + let is_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 (address offset) in + let upper_bound = + Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) + in + Ok + ( Value.Bool.(or_ (const (Int32.lt 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 + Fmt.failwith "Memory leak double free"; + Hashtbl.remove m.chunks base + + let realloc m base size = Hashtbl.replace m.chunks base size +end + +module Make (Backend : Symbolic_memory_intf.M) = struct + type t = + { data : Backend.t + ; mutable size : Value.int32 + } + + let create size = { data = Backend.create (); size = Value.const_i32 size } + + 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 = Backend.address (Value.const_i32 (Int32.of_int (dst + i))) in + Backend.storen m.data dst (value (Num (I8 byte))) 1 + done; + Value.Bool.const false + end + + let clone m = { data = Backend.clone m.data; size = m.size } + + let load_8_s m a = + let v = Backend.loadn m.data (Backend.address 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 = Backend.loadn m.data (Backend.address 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 = Backend.loadn m.data (Backend.address 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 = Backend.loadn m.data (Backend.address a) 2 in + match view v with + | Val (Num (I32 _)) -> v + | _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v + + let load_32 m a = Backend.loadn m.data (Backend.address a) 4 + + let load_64 m a = Backend.loadn m.data (Backend.address a) 8 + + let store_8 m ~addr v = Backend.storen m.data (Backend.address addr) v 1 + + let store_16 m ~addr v = Backend.storen m.data (Backend.address addr) v 2 + + let store_32 m ~addr v = Backend.storen m.data (Backend.address addr) v 4 + + let store_64 m ~addr v = Backend.storen m.data (Backend.address addr) v 8 + + let get_limit_max _m = None (* TODO *) + + let check_within_bounds m a = Backend.is_within_bounds m.data a + + let free m base = Backend.free m.data (Backend.address (Value.const_i32 base)) + + let replace_size m base size = + Backend.realloc m.data (Backend.address (Value.const_i32 base)) size +end + +include Make (Backend) module ITbl = Hashtbl.Make (struct include Int diff --git a/src/symbolic/symbolic_memory_intf.ml b/src/symbolic/symbolic_memory_intf.ml new file mode 100644 index 000000000..eb2297077 --- /dev/null +++ b/src/symbolic/symbolic_memory_intf.ml @@ -0,0 +1,25 @@ +module type M = sig + type t + + type address + + val create : unit -> t + + val clone : t -> t + + val address : Smtml.Expr.t -> address + + val loadn : t -> address -> int -> Smtml.Expr.t + + val storen : t -> address -> Smtml.Expr.t -> int -> unit + + (* TODO: return address instead *) + val is_within_bounds : + t -> Smtml.Expr.t -> (Smtml.Expr.t * Smtml.Expr.t, Trap.t) result + + val free : t -> address -> unit + + val realloc : t -> address -> Smtml.Expr.t -> unit +end + +module type S = sig end From 5d1f9bae1bffc56887fb78fa74fad52a12948693 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Tue, 9 Jul 2024 15:47:14 +0200 Subject: [PATCH 2/3] Expose address type in memory - Add symbolic memory `address` type to avoid explicit address manipulation. - Refactor symbolic memory heap allocation functions --- src/concolic/concolic.ml | 4 +- src/symbolic/symbolic.ml | 2 +- src/symbolic/symbolic_memory.ml | 63 ++++++++++++------- src/symbolic/symbolic_memory.mli | 69 +-------------------- src/symbolic/symbolic_memory_intf.ml | 93 ++++++++++++++++++++++++++-- src/symbolic/symbolic_wasm_ffi.ml | 27 ++------ 6 files changed, 136 insertions(+), 122 deletions(-) diff --git a/src/concolic/concolic.ml b/src/concolic/concolic.ml index 3889fc3dd..1be1265d7 100644 --- a/src/concolic/concolic.ml +++ b/src/concolic/concolic.ml @@ -122,14 +122,14 @@ module P = struct let open Choice in let+ a = Choice.select_i32 a in { concrete = f_c m.concrete a - ; symbolic = f_s m.symbolic (Symbolic_value.const_i32 a) + ; symbolic = f_s m.symbolic (S.address_i32 a) } let with_concrete_store m a f_c f_s v = let open Choice in let+ addr = Choice.select_i32 a in f_c m.concrete ~addr v.concrete; - f_s m.symbolic ~addr:(Symbolic_value.const_i32 addr) v.symbolic + f_s m.symbolic ~addr:(S.address_i32 addr) v.symbolic let load_8_s m a = with_concrete m a C.load_8_s S.load_8_s diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml index 8b64f67e9..875e3bb46 100644 --- a/src/symbolic/symbolic.ml +++ b/src/symbolic/symbolic.ml @@ -73,7 +73,7 @@ struct Symbolic_value.const_i32 v let check_within_bounds m a = - match check_within_bounds m a with + match is_within_bounds m a with | Error t -> Choice.trap t | Ok (cond, ptr) -> let open Choice in diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index f7aac703a..6b91f3be3 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -32,6 +32,13 @@ module Backend : Symbolic_memory_intf.M = struct | Val (Num (I32 i)) -> i | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v + let ptr v = + match view v with + | Ptr { base; _ } -> base + | _ -> Log.err {|free: cannot fetch pointer base of "%a"|} Expr.pp v + + let address_i32 i = i + let rec load_byte { parent; data; _ } a = try Hashtbl.find data a with Not_found -> ( @@ -103,7 +110,7 @@ module Backend : Symbolic_memory_intf.M = struct let is_within_bounds m a = match view a with - | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) + | Val (Num (I32 a)) -> 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 @@ -112,17 +119,18 @@ module Backend : Symbolic_memory_intf.M = struct let upper_bound = Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) in - Ok - ( Value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound) - , Value.const_i32 ptr ) ) + Ok (Value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound), ptr) ) | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a - let free m base = - if not @@ Hashtbl.mem m.chunks base then - Fmt.failwith "Memory leak double free"; - Hashtbl.remove m.chunks base + let free m ptr = + if not @@ Hashtbl.mem m.chunks ptr then + Error Trap.Memory_leak_use_after_free + (* failwith "Memory leak double free"; *) + else Ok (Hashtbl.remove m.chunks ptr) - let realloc m base size = Hashtbl.replace m.chunks base size + let realloc m ptr size = + Hashtbl.replace m.chunks ptr size; + Expr.ptr ptr (Symbolic_value.const_i32 0l) end module Make (Backend : Symbolic_memory_intf.M) = struct @@ -131,8 +139,16 @@ module Make (Backend : Symbolic_memory_intf.M) = struct ; mutable size : Value.int32 } + type address = Backend.address + let create size = { data = Backend.create (); size = Value.const_i32 size } + let ptr p = Backend.ptr p + + let address a = Backend.address a + + let address_i32 a = Backend.address_i32 a + let i32 v = match view v with | Val (Num (I32 i)) -> i @@ -169,7 +185,7 @@ module Make (Backend : Symbolic_memory_intf.M) = struct else begin for i = 0 to len - 1 do let byte = Char.code @@ String.get str (src + i) in - let dst = Backend.address (Value.const_i32 (Int32.of_int (dst + i))) in + let dst = Backend.address_i32 (Int32.of_int (dst + i)) in Backend.storen m.data dst (value (Num (I8 byte))) 1 done; Value.Bool.const false @@ -178,49 +194,48 @@ module Make (Backend : Symbolic_memory_intf.M) = struct let clone m = { data = Backend.clone m.data; size = m.size } let load_8_s m a = - let v = Backend.loadn m.data (Backend.address a) 1 in + let v = Backend.loadn m.data 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 = Backend.loadn m.data (Backend.address a) 1 in + let v = Backend.loadn m.data 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 = Backend.loadn m.data (Backend.address a) 2 in + let v = Backend.loadn m.data 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 = Backend.loadn m.data (Backend.address a) 2 in + let v = Backend.loadn m.data a 2 in match view v with | Val (Num (I32 _)) -> v | _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v - let load_32 m a = Backend.loadn m.data (Backend.address a) 4 + let load_32 m a = Backend.loadn m.data a 4 - let load_64 m a = Backend.loadn m.data (Backend.address a) 8 + let load_64 m a = Backend.loadn m.data a 8 - let store_8 m ~addr v = Backend.storen m.data (Backend.address addr) v 1 + let store_8 m ~addr v = Backend.storen m.data addr v 1 - let store_16 m ~addr v = Backend.storen m.data (Backend.address addr) v 2 + let store_16 m ~addr v = Backend.storen m.data addr v 2 - let store_32 m ~addr v = Backend.storen m.data (Backend.address addr) v 4 + let store_32 m ~addr v = Backend.storen m.data addr v 4 - let store_64 m ~addr v = Backend.storen m.data (Backend.address addr) v 8 + let store_64 m ~addr v = Backend.storen m.data addr v 8 let get_limit_max _m = None (* TODO *) - let check_within_bounds m a = Backend.is_within_bounds m.data a + let is_within_bounds m a = Backend.is_within_bounds m.data a - let free m base = Backend.free m.data (Backend.address (Value.const_i32 base)) + let free m ptr = Backend.free m.data ptr - let replace_size m base size = - Backend.realloc m.data (Backend.address (Value.const_i32 base)) size + let realloc m ptr size = Backend.realloc m.data ptr size end include Make (Backend) diff --git a/src/symbolic/symbolic_memory.mli b/src/symbolic/symbolic_memory.mli index 276272885..629a8dd9f 100644 --- a/src/symbolic/symbolic_memory.mli +++ b/src/symbolic/symbolic_memory.mli @@ -2,70 +2,5 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -type t - -type collection - -val init : unit -> collection - -val clone : collection -> collection - -val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t - -val check_within_bounds : - t -> Smtml.Expr.t -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result - -val replace_size : t -> Int32.t -> Smtml.Expr.t -> unit - -val free : t -> Int32.t -> unit - -val load_8_s : t -> Smtml.Expr.t -> Symbolic_value.int32 - -val load_8_u : t -> Smtml.Expr.t -> Symbolic_value.int32 - -val load_16_s : t -> Smtml.Expr.t -> Symbolic_value.int32 - -val load_16_u : t -> Smtml.Expr.t -> Symbolic_value.int32 - -val load_32 : t -> Smtml.Expr.t -> Symbolic_value.int32 - -val load_64 : t -> Smtml.Expr.t -> Symbolic_value.int32 - -val store_8 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit - -val store_16 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit - -val store_32 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit - -val store_64 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit - -val grow : t -> Smtml.Expr.t -> unit - -val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t - -val blit : - t -> src:Smtml.Expr.t -> dst:Smtml.Expr.t -> len:Smtml.Expr.t -> Smtml.Expr.t - -val blit_string : - t - -> string - -> src:Smtml.Expr.t - -> dst:Smtml.Expr.t - -> len:Smtml.Expr.t - -> Smtml.Expr.t - -val size : t -> Smtml.Expr.t - -val size_in_pages : t -> Smtml.Expr.t - -val get_limit_max : t -> Smtml.Expr.t option - -module ITbl : sig - type 'a t - - type key - - val iter : (key -> 'a -> unit) -> 'a t -> unit -end - -val iter : (t ITbl.t -> unit) -> collection -> unit +(** @inline *) +include Symbolic_memory_intf.S diff --git a/src/symbolic/symbolic_memory_intf.ml b/src/symbolic/symbolic_memory_intf.ml index eb2297077..3bc79bbb8 100644 --- a/src/symbolic/symbolic_memory_intf.ml +++ b/src/symbolic/symbolic_memory_intf.ml @@ -7,19 +7,102 @@ module type M = sig val clone : t -> t + val ptr : Smtml.Expr.t -> address + val address : Smtml.Expr.t -> address + val address_i32 : Int32.t -> address + val loadn : t -> address -> int -> Smtml.Expr.t val storen : t -> address -> Smtml.Expr.t -> int -> unit - (* TODO: return address instead *) val is_within_bounds : - t -> Smtml.Expr.t -> (Smtml.Expr.t * Smtml.Expr.t, Trap.t) result + t -> Smtml.Expr.t -> (Smtml.Expr.t * address, Trap.t) result - val free : t -> address -> unit + val free : t -> address -> (unit, Trap.t) result - val realloc : t -> address -> Smtml.Expr.t -> unit + val realloc : t -> address -> Smtml.Expr.t -> Smtml.Expr.t end -module type S = sig end +module type S = sig + type t + + type address + + type collection + + val init : unit -> collection + + val clone : collection -> collection + + val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t + + val is_within_bounds : + t -> Smtml.Expr.t -> (Smtml.Expr.t * address, Trap.t) result + + val ptr : Smtml.Expr.t -> address + + val address : Smtml.Expr.t -> address + + val address_i32 : Int32.t -> address + + val free : t -> address -> (unit, Trap.t) result + + val realloc : t -> address -> Smtml.Expr.t -> Smtml.Expr.t + + val load_8_s : t -> address -> Symbolic_value.int32 + + val load_8_u : t -> address -> Symbolic_value.int32 + + val load_16_s : t -> address -> Symbolic_value.int32 + + val load_16_u : t -> address -> Symbolic_value.int32 + + val load_32 : t -> address -> Symbolic_value.int32 + + val load_64 : t -> address -> Symbolic_value.int32 + + val store_8 : t -> addr:address -> Smtml.Expr.t -> unit + + val store_16 : t -> addr:address -> Smtml.Expr.t -> unit + + val store_32 : t -> addr:address -> Smtml.Expr.t -> unit + + val store_64 : t -> addr:address -> Smtml.Expr.t -> unit + + val grow : t -> Smtml.Expr.t -> unit + + val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t + + val blit : + t + -> src:Smtml.Expr.t + -> dst:Smtml.Expr.t + -> len:Smtml.Expr.t + -> Smtml.Expr.t + + val blit_string : + t + -> string + -> src:Smtml.Expr.t + -> dst:Smtml.Expr.t + -> len:Smtml.Expr.t + -> Smtml.Expr.t + + val size : t -> Smtml.Expr.t + + val size_in_pages : t -> Smtml.Expr.t + + val get_limit_max : t -> Smtml.Expr.t option + + module ITbl : sig + type 'a t + + type key + + val iter : (key -> 'a -> unit) -> 'a t -> unit + end + + val iter : (t ITbl.t -> unit) -> collection -> unit +end diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index 962dec31c..46ebd626b 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -39,34 +39,15 @@ module M : let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol - open Expr - let abort () : unit Choice.t = Choice.add_pc @@ Value.Bool.const false - let i32 v : int32 Choice.t = - match view v with - | Val (Num (I32 v)) -> Choice.return v - | _ -> - Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v; - Choice.bind (abort ()) (fun () -> assert false) - - let ptr v : int32 Choice.t = - match view v with - | Ptr { base; _ } -> Choice.return base - | _ -> - Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v; - Choice.bind (abort ()) (fun () -> assert false) - 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) + Choice.return (Memory.realloc m (Memory.address base) size) let free m (p : Value.int32) : unit Choice.t = - let open Choice in - let+ base = ptr p in - Memory.free m base + match Memory.free m (Memory.ptr p) with + | Error t -> Choice.trap t + | Ok () -> Choice.return () let exit (_p : Value.int32) : unit Choice.t = abort () end From 87297781cb34f42b96a900ed3a952f75ffa296cd Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Tue, 9 Jul 2024 16:15:10 +0200 Subject: [PATCH 3/3] Make symbolic memory backend parametric on choice monad --- src/dune | 2 + src/symbolic/symbolic_memory.ml | 128 +----------------------- src/symbolic/symbolic_memory_backend.ml | 127 +++++++++++++++++++++++ src/symbolic/symbolic_memory_choice.ml | 19 ++++ 4 files changed, 150 insertions(+), 126 deletions(-) create mode 100644 src/symbolic/symbolic_memory_backend.ml create mode 100644 src/symbolic/symbolic_memory_choice.ml diff --git a/src/dune b/src/dune index 671016abf..ec98f73e5 100644 --- a/src/dune +++ b/src/dune @@ -64,6 +64,8 @@ symbolic_choice_minimalist symbolic_global symbolic_memory + symbolic_memory_backend + symbolic_memory_choice symbolic_memory_intf symbolic_table symbolic_value diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index 6b91f3be3..c5f51e6a3 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -2,137 +2,12 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -module Value = Symbolic_value module Expr = Smtml.Expr -module Ty = Smtml.Ty +module Value = Symbolic_value open Expr let page_size = Symbolic_value.const_i32 65_536l -module Backend : Symbolic_memory_intf.M = struct - type address = Int32.t - - type t = - { data : (address, Value.int32) Hashtbl.t - ; parent : t option - ; chunks : (address, Value.int32) Hashtbl.t - } - - let create () = - { data = Hashtbl.create 128; parent = None; chunks = Hashtbl.create 16 } - - let clone m = - { data = Hashtbl.create 16 - ; parent = Some m - ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) - } - - let address v = - match view v with - | Val (Num (I32 i)) -> i - | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v - - let ptr v = - match view v with - | Ptr { base; _ } -> base - | _ -> Log.err {|free: cannot fetch pointer base of "%a"|} Expr.pp v - - let address_i32 i = i - - 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 extract v pos = - match 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 - 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 Smtml.Ty.equal (Ty_bitv 8) (ty sym) -> - sym - | _ -> make (Extract (v, pos + 1, pos)) - - let storen m addr v n = - for i = 0 to n - 1 do - let addr' = Int32.add addr (Int32.of_int i) in - let v' = extract v i in - Hashtbl.replace m.data addr' v' - done - - let is_within_bounds m a = - match view a with - | Val (Num (I32 a)) -> 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 (address offset) in - let upper_bound = - Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) - in - Ok (Value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound), ptr) ) - | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a - - let free m ptr = - if not @@ Hashtbl.mem m.chunks ptr then - Error Trap.Memory_leak_use_after_free - (* failwith "Memory leak double free"; *) - else Ok (Hashtbl.remove m.chunks ptr) - - let realloc m ptr size = - Hashtbl.replace m.chunks ptr size; - Expr.ptr ptr (Symbolic_value.const_i32 0l) -end - module Make (Backend : Symbolic_memory_intf.M) = struct type t = { data : Backend.t @@ -238,6 +113,7 @@ module Make (Backend : Symbolic_memory_intf.M) = struct let realloc m ptr size = Backend.realloc m.data ptr size end +module Backend = Symbolic_memory_backend.Make (Symbolic_memory_choice) include Make (Backend) module ITbl = Hashtbl.Make (struct diff --git a/src/symbolic/symbolic_memory_backend.ml b/src/symbolic/symbolic_memory_backend.ml new file mode 100644 index 000000000..220cdae78 --- /dev/null +++ b/src/symbolic/symbolic_memory_backend.ml @@ -0,0 +1,127 @@ +open Smtml.Expr +module Expr = Smtml.Expr +module Value = Symbolic_value + +module Make (_ : Choice_intf.Base) : Symbolic_memory_intf.M = struct + type address = Int32.t + + type t = + { data : (address, Value.int32) Hashtbl.t + ; parent : t option + ; chunks : (address, Value.int32) Hashtbl.t + } + + let create () = + { data = Hashtbl.create 128; parent = None; chunks = Hashtbl.create 16 } + + let clone m = + { data = Hashtbl.create 16 + ; parent = Some m + ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) + } + + let address v = + match view v with + | Val (Num (I32 i)) -> i + | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v + + let ptr v = + match view v with + | Ptr { base; _ } -> base + | _ -> Log.err {|free: cannot fetch pointer base of "%a"|} Expr.pp v + + let address_i32 i = i + + 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 = Smtml.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 extract v pos = + match 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 + 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 Smtml.Ty.equal (Ty_bitv 8) (ty sym) -> + sym + | _ -> make (Extract (v, pos + 1, pos)) + + let storen m addr v n = + for i = 0 to n - 1 do + let addr' = Int32.add addr (Int32.of_int i) in + let v' = extract v i in + Hashtbl.replace m.data addr' v' + done + + let is_within_bounds m a = + match view a with + | Val (Num (I32 a)) -> 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 (address offset) in + let upper_bound = + Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) + in + Ok (Value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound), ptr) ) + | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a + + let free m ptr = + if not @@ Hashtbl.mem m.chunks ptr then + Error Trap.Memory_leak_use_after_free + (* failwith "Memory leak double free"; *) + else Ok (Hashtbl.remove m.chunks ptr) + + let realloc m ptr size = + Hashtbl.replace m.chunks ptr size; + Expr.ptr ptr (Symbolic_value.const_i32 0l) +end diff --git a/src/symbolic/symbolic_memory_choice.ml b/src/symbolic/symbolic_memory_choice.ml new file mode 100644 index 000000000..9df22e676 --- /dev/null +++ b/src/symbolic/symbolic_memory_choice.ml @@ -0,0 +1,19 @@ +module V = Symbolic_value + +type 'a t = 'a + +let return a = a + +let bind a k = k a + +let ( let* ) = bind + +let map a k = k a + +let ( let+ ) = map + +let select _ = assert false + +let select_i32 _ = assert false + +let trap _ = assert false