Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] Make symbolic memory parametric #357

Closed
wants to merge 3 commits into from
Closed

[WIP] Make symbolic memory parametric #357

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d0dd6b6
Start making memory parametric
filipeom Jul 5, 2024
5d1f9ba
Expose address type in memory
filipeom Jul 9, 2024
8729778
Make symbolic memory backend parametric on choice monad
filipeom Jul 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/concolic/concolic.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
3 changes: 3 additions & 0 deletions src/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,9 @@
symbolic_choice_minimalist
symbolic_global
symbolic_memory
symbolic_memory_backend
symbolic_memory_choice
symbolic_memory_intf
symbolic_table
symbolic_value
symbolic_wasm_ffi
Expand Down
2 changes: 1 addition & 1 deletion src/symbolic/symbolic.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
299 changes: 108 additions & 191 deletions src/symbolic/symbolic_memory.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,202 +2,119 @@
(* 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

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 Make (Backend : Symbolic_memory_intf.M) = struct
type t =
{ data : Backend.t
; 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
| _ -> 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_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 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 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 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 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 a 4

let load_64 m a = Backend.loadn m.data a 8

let store_8 m ~addr v = Backend.storen m.data addr v 1

let store_16 m ~addr v = Backend.storen m.data addr v 2

let store_32 m ~addr v = Backend.storen m.data addr v 4

let store_64 m ~addr v = Backend.storen m.data addr v 8

let get_limit_max _m = None (* TODO *)

let is_within_bounds m a = Backend.is_within_bounds m.data a

let free m ptr = Backend.free m.data ptr

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
include Int
Expand Down
Loading
Loading