Skip to content

Commit

Permalink
Backup other things
Browse files Browse the repository at this point in the history
  • Loading branch information
chambart authored and zapashcanon committed Jun 5, 2024
1 parent 78939cd commit aab1ed6
Show file tree
Hide file tree
Showing 6 changed files with 40 additions and 2 deletions.
1 change: 1 addition & 0 deletions src/concolic/concolic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -263,4 +263,5 @@ let convert_module_to_run (m : 'f Link.module_to_run) =
P.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run }

let backup (m : P.Module_to_run.t) = Link_env.backup m.env

let recover b (m : P.Module_to_run.t) = Link_env.recover b m.env
6 changes: 6 additions & 0 deletions src/concrete/concrete_memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,12 @@ type t =
; mutable data : bytes
}

let backup t = { t with data = Bytes.copy t.data }

let recover ~from_ ~to_ =
to_.limits <- from_.limits;
to_.data <- from_.data

let init limits : t =
let data = Bytes.make (page_size * limits.min) '\x00' in
{ limits; data }
Expand Down
4 changes: 4 additions & 0 deletions src/concrete/concrete_memory.mli
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,10 @@
(** runtime memory *)
type t

val backup : t -> t

val recover : from_:t -> to_:t -> unit

val get_limit_max : t -> int64 option

val get_limits : t -> Types.limits
Expand Down
4 changes: 4 additions & 0 deletions src/concrete/concrete_table.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,10 @@ type t =
; mutable data : table
}

let backup t = { t with data = Array.copy t.data }

let recover ~from_ ~to_ = to_.data <- from_.data

let fresh =
let r = ref (-1) in
fun () ->
Expand Down
4 changes: 4 additions & 0 deletions src/concrete/concrete_table.mli
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,10 @@ type t =
; mutable data : table
}

val backup : t -> t

val recover : from_:t -> to_:t -> unit

val get : t -> int -> Concrete_value.ref_value

val set : t -> int -> Concrete_value.ref_value -> unit
Expand Down
23 changes: 21 additions & 2 deletions src/link/link_env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,21 @@ type 'ext t =

type 'ext backup = 'ext t

let backup_data (data : data) : data = { value = data.value }

let backup_elem (elem : elem) : elem = { value = elem.value }

let recover_data ~(from_ : data) ~(to_ : data) = to_.value <- from_.value

let recover_elem ~(from_ : elem) ~(to_ : elem) = to_.value <- from_.value

let backup t =
{ t with
globals = IMap.map Concrete_global.backup t.globals (* TODO tables/memory *)
globals = IMap.map Concrete_global.backup t.globals
; memories = IMap.map Concrete_memory.backup t.memories
; tables = IMap.map Concrete_table.backup t.tables
; data = IMap.map backup_data t.data
; elem = IMap.map backup_elem t.elem
}

let recover backup into =
Expand All @@ -47,7 +59,14 @@ let recover backup into =
let _ : _ IMap.t =
IMap.merge (apply Concrete_global.recover) backup.globals into.globals
in
(* TODO tables/memory *)
let _ : _ IMap.t =
IMap.merge (apply Concrete_memory.recover) backup.memories into.memories
in
let _ : _ IMap.t =
IMap.merge (apply Concrete_table.recover) backup.tables into.tables
in
let _ : _ IMap.t = IMap.merge (apply recover_data) backup.data into.data in
let _ : _ IMap.t = IMap.merge (apply recover_elem) backup.elem into.elem in
()

let id (env : _ t) = env.id
Expand Down

0 comments on commit aab1ed6

Please sign in to comment.