Skip to content

Commit

Permalink
use a mutable field instead of a reference for symbolic memory data
Browse files Browse the repository at this point in the history
  • Loading branch information
zapashcanon committed Sep 5, 2024
1 parent 65fa3e8 commit 2b6c020
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 15 deletions.
14 changes: 6 additions & 8 deletions src/symbolic/symbolic_memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ open Expr
let page_size = Symbolic_value.const_i32 65_536l

type t =
{ data : (Int32.t, Value.int32) Hashtbl.t option ref
{ mutable data : (Int32.t, Value.int32) Hashtbl.t option
; parent : t option
; mutable size : Value.int32
; chunks : (Int32.t, Value.int32) Hashtbl.t
Expand Down Expand Up @@ -42,11 +42,11 @@ let fill _ = assert false
let blit _ = assert false

let replace m k v =
match !(m.data) with
match m.data with
| None ->
let tbl = Hashtbl.create 16 in
Hashtbl.add tbl k v;
m.data := Some tbl
m.data <- Some tbl
| Some tbl -> Hashtbl.replace tbl k v

let blit_string m str ~src ~dst ~len =
Expand All @@ -68,18 +68,16 @@ let blit_string m str ~src ~dst ~len =
end

let clone m =
let parent = if Option.is_none !(m.data) then m.parent else Some m in
{ data = ref None
let parent = if Option.is_none m.data then m.parent else Some m in
{ data = None
; parent
; size = m.size
; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *)
}

let rec load_byte { parent; data; _ } a =
try
match !data with
| None -> raise Not_found
| Some data -> Hashtbl.find data a
match data with None -> raise Not_found | Some data -> Hashtbl.find data a
with Not_found -> (
match parent with
| None -> make (Val (Num (I8 0)))
Expand Down
14 changes: 7 additions & 7 deletions src/symbolic/symbolic_memory_concretizing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,17 @@ module Backend = struct
type address = Int32.t

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

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

let clone m =
let parent = if Option.is_none !(m.data) then m.parent else Some m in
let parent = if Option.is_none m.data then m.parent else Some m in
(* TODO: Make chunk copying lazy *)
{ data = ref None; parent; chunks = Hashtbl.copy m.chunks }
{ data = None; parent; chunks = Hashtbl.copy m.chunks }

let address a =
let open Symbolic_choice_without_memory in
Expand All @@ -28,7 +28,7 @@ module Backend = struct

let rec load_byte { parent; data; _ } a =
try
match !data with
match data with
| None -> raise Not_found
| Some data -> Hashtbl.find data a
with Not_found -> (
Expand Down Expand Up @@ -97,11 +97,11 @@ module Backend = struct
| _ -> Expr.make (Extract (v, pos + 1, pos))

let replace m k v =
match !(m.data) with
match m.data with
| None ->
let tbl = Hashtbl.create 16 in
Hashtbl.add tbl k v;
m.data := Some tbl
m.data <- Some tbl
| Some tbl -> Hashtbl.replace tbl k v

let storen m a v n =
Expand Down

0 comments on commit 2b6c020

Please sign in to comment.