Skip to content

small optimisation of the lazy memory model #433

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

Merged
redianthus merged 6 commits into from
Mar 4, 2025
Merged

small optimisation of the lazy memory model #433

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
2ae3ae3
small optimisation of the lazy memory model
redianthus Sep 4, 2024
7e5f454
use a mutable field instead of a reference for symbolic memory data
redianthus Sep 5, 2024
fe6b190
make memory data immutable by using a Map
redianthus Feb 24, 2025
c311251
make memory chunks immutable by using a Map
redianthus Feb 25, 2025
f37833f
fix match-on-mutable-state-prevent-uncurry
redianthus Feb 27, 2025
715430a
remove useless Map.remove call
redianthus Mar 3, 2025
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
153 changes: 78 additions & 75 deletions src/symbolic/symbolic_memory.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,45 +2,45 @@
(* 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

module Map = Map.Make (struct
include Int32

(* TODO: define this in Int32 directly? *)
let compare i1 i2 = compare (Int32.to_int i1) (Int32.to_int i2)
end)

type t =
{ data : (Int32.t, Value.int32) Hashtbl.t
; parent : t option
; mutable size : Value.int32
; chunks : (Int32.t, Value.int32) Hashtbl.t
{ mutable data : Symbolic_value.int32 Map.t
; mutable size : Symbolic_value.int32
; mutable chunks : Symbolic_value.int32 Map.t
}

let create size =
{ data = Hashtbl.create 128
; parent = None
; size = Value.const_i32 size
; chunks = Hashtbl.create 16
}
{ data = Map.empty; size = Symbolic_value.const_i32 size; chunks = Map.empty }

let i32 v = match view v with Val (Num (I32 i)) -> i | _ -> assert false
let i32 v =
match Smtml.Expr.view v with Val (Num (I32 i)) -> i | _ -> assert false

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
let old_size = Symbolic_value.I32.mul m.size page_size in
let new_size = Symbolic_value.I32.(div (add old_size delta) page_size) in
m.size <-
Value.Bool.select_expr
(Value.I32.gt new_size m.size)
Symbolic_value.Bool.select_expr
(Symbolic_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 { size; _ } = Symbolic_value.I32.mul size page_size

let size_in_pages { size; _ } = size

let fill _ = assert false

let blit _ = assert false

let replace m k v = m.data <- Map.add k v m.data

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
Expand All @@ -49,121 +49,120 @@ let blit_string m str ~src ~dst ~len =
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
then Symbolic_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))))
replace m dst (Smtml.Expr.make (Val (Num (I8 byte))))
done;
Value.Bool.const false
Symbolic_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 clone { data; chunks; size } =
(* Caution, it is tempting not to rebuild the record here, but...
it must be! otherwise the mutable data points to the same location *)
{ data; chunks; size }

let rec load_byte { parent; data; _ } a =
match Hashtbl.find_opt data a with
| None -> begin
match parent with
| None -> make (Val (Num (I8 0)))
| Some parent -> load_byte parent a
end
let load_byte a { data; _ } =
match Map.find_opt a data with
| None -> Smtml.Expr.make (Val (Num (I8 0)))
| Some v -> v

(* 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 ty = Smtml.Expr.ty e1 in
if m1 = m2 && Smtml.Expr.equal e1 e2 then
if h - l = Smtml.Ty.size ty then e1 else Smtml.Expr.make (Extract (e1, h, l))
else
Smtml.Expr.make
(Concat
( Smtml.Expr.make (Extract (e1, h, m1))
, Smtml.Expr.make (Extract (e2, m2, l)) ) )

let concat ~msb ~lsb offset =
assert (offset > 0 && offset <= 8);
match (view msb, view lsb) with
match (Smtml.Expr.view msb, Smtml.Expr.view lsb) with
| Val (Num (I8 i1)), Val (Num (I8 i2)) ->
Value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int 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
Value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2)
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
Value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
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
Value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
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) ->
make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))
| _ -> make (Concat (msb, lsb))
Smtml.Expr.make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))
| _ -> Smtml.Expr.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
let byte = load_byte addr' m in
loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
in
let v0 = load_byte m a in
let v0 = load_byte a m 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
match Smtml.Expr.view v with
| Val (Num (I8 i8)) ->
Symbolic_value.const_i32 (Int32.extend_s 8 (Int32.of_int i8))
| _ -> Smtml.Expr.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
match Smtml.Expr.view v with
| Val (Num (I8 i)) -> Symbolic_value.const_i32 (Int32.of_int i)
| _ -> Smtml.Expr.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
match Smtml.Expr.view v with
| Val (Num (I32 i16)) -> Symbolic_value.const_i32 (Int32.extend_s 16 i16)
| _ -> Smtml.Expr.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
match Smtml.Expr.view v with
| Val (Num (I32 _)) -> v
| _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v
| _ -> Smtml.Expr.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
match Smtml.Expr.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'))
Smtml.Expr.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'))
Smtml.Expr.value (Num (I8 i'))
| Cvtop
( _
, (Zero_extend 24 | Sign_extend 24)
, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym) ) ->
sym
| _ -> make (Extract (v, pos + 1, pos))
| _ -> Smtml.Expr.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'
replace m addr' v'
done

let store_8 m ~addr v = storen m ~addr v 1
Expand All @@ -177,27 +176,31 @@ 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)
match Smtml.Expr.view a with
| Val (Num (I32 _)) -> Ok (Symbolic_value.Bool.const false, a)
| Ptr { base; offset } -> (
match Hashtbl.find_opt m.chunks base with
match Map.find_opt base m.chunks with
| None -> Error Trap.Memory_leak_use_after_free
| Some size ->
let ptr = Int32.add base (i32 offset) in
let upper_bound =
Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size))
Symbolic_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 ) )
( Symbolic_value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound)
, Symbolic_value.const_i32 ptr ) )
| _ -> assert false

let free m base =
if not @@ Hashtbl.mem m.chunks base then
Fmt.failwith "Memory leak double free";
Hashtbl.remove m.chunks base
if not @@ Map.mem base m.chunks then Fmt.failwith "Memory leak double free"
else begin
let chunks = Map.remove base m.chunks in
m.chunks <- chunks
end

let realloc m base size = Hashtbl.replace m.chunks base size
let realloc m base size =
let chunks = Map.add base size m.chunks in
m.chunks <- chunks

module ITbl = Hashtbl.Make (struct
include Int
Expand Down
57 changes: 31 additions & 26 deletions src/symbolic/symbolic_memory_concretizing.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,21 +1,24 @@
module Backend = struct
type address = Int32.t

module Map = Map.Make (struct
include Int32

(* TODO: define this in Int32 directly? *)
let compare i1 i2 = compare (Int32.to_int i1) (Int32.to_int i2)
end)

type t =
{ data : (address, Symbolic_value.int32) Hashtbl.t
; parent : t option
; chunks : (address, Symbolic_value.int32) Hashtbl.t
{ mutable data : Symbolic_value.int32 Map.t
; mutable chunks : Symbolic_value.int32 Map.t
}

let make () =
{ data = Hashtbl.create 16; parent = None; chunks = Hashtbl.create 16 }
let make () = { data = Map.empty; chunks = Map.empty }

let clone m =
(* TODO: Make chunk copying lazy *)
{ data = Hashtbl.create 16
; parent = Some m
; chunks = Hashtbl.copy m.chunks
}
let clone { data; chunks } =
(* Caution, it is tempting not to rebuild the record here, but...
it must be! otherwise the mutable data points to the same location *)
{ data; chunks }

let address a =
let open Symbolic_choice_without_memory in
Expand All @@ -27,13 +30,10 @@ module Backend = struct

let address_i32 a = a

let rec load_byte { parent; data; _ } a =
match Hashtbl.find_opt data a with
let load_byte a { data; _ } =
match Map.find_opt a data with
| None -> Smtml.Expr.value (Num (I8 0))
| Some v -> v
| None -> (
match parent with
| None -> Smtml.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) =
Expand Down Expand Up @@ -73,10 +73,10 @@ module Backend = struct
if i = size then acc
else
let addr' = Int32.(add addr (of_int i)) in
let byte = load_byte m addr' in
let byte = load_byte addr' m in
loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
in
let v0 = load_byte m a in
let v0 = load_byte a m in
loop a n 1 v0

let extract v pos =
Expand All @@ -96,11 +96,13 @@ module Backend = struct
sym
| _ -> Smtml.Expr.make (Extract (v, pos + 1, pos))

let replace m k v = m.data <- Map.add k v m.data

let storen m a v n =
for i = 0 to n - 1 do
let a' = Int32.add a (Int32.of_int i) in
let v' = extract v i in
Hashtbl.replace m.data a' v'
replace m a' v'
done

let validate_address m a range =
Expand All @@ -111,7 +113,7 @@ module Backend = struct
return (Ok a)
| Ptr { base; offset = start_offset } -> (
let open Symbolic_value in
match Hashtbl.find_opt m.chunks base with
match Map.find_opt base m.chunks with
| None -> return (Error Trap.Memory_leak_use_after_free)
| Some chunk_size ->
let+ is_out_of_bounds =
Expand Down Expand Up @@ -142,15 +144,18 @@ module Backend = struct
let free m p =
let open Symbolic_choice_without_memory in
let+ base = ptr p in
if not @@ Hashtbl.mem m.chunks base then
Fmt.failwith "Memory leak double free";
Hashtbl.remove m.chunks base;
Symbolic_value.const_i32 base
if not @@ Map.mem base m.chunks then Fmt.failwith "Memory leak double free"
else begin
let chunks = Map.remove base m.chunks in
m.chunks <- chunks;
Symbolic_value.const_i32 base
end

let realloc m ~ptr ~size =
let open Symbolic_choice_without_memory in
let+ base = address ptr in
Hashtbl.replace m.chunks base size;
let chunks = Map.add base size m.chunks in
m.chunks <- chunks;
Smtml.Expr.ptr base (Symbolic_value.const_i32 0l)
end

Expand Down
Loading