From 2b6c02007e533577a07d615561336344ae261c3e Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Thu, 5 Sep 2024 11:17:33 +0200 Subject: [PATCH] use a mutable field instead of a reference for symbolic memory data --- src/symbolic/symbolic_memory.ml | 14 ++++++-------- src/symbolic/symbolic_memory_concretizing.ml | 14 +++++++------- 2 files changed, 13 insertions(+), 15 deletions(-) diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index dd9861c0..165c6b81 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -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 @@ -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 = @@ -68,8 +68,8 @@ 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 *) @@ -77,9 +77,7 @@ let clone m = 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))) diff --git a/src/symbolic/symbolic_memory_concretizing.ml b/src/symbolic/symbolic_memory_concretizing.ml index 4ab43aa0..2b85f90d 100644 --- a/src/symbolic/symbolic_memory_concretizing.ml +++ b/src/symbolic/symbolic_memory_concretizing.ml @@ -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 @@ -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 -> ( @@ -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 =