From 865d79ce5eb3759cd416a58018973903e1e46026 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 24 Jul 2024 19:35:32 +0200
Subject: [PATCH] [region] copy instructions
---
src/plugins/region/code.ml | 11 +++++++++--
src/plugins/region/memory.ml | 4 ++++
src/plugins/region/memory.mli | 1 +
3 files changed, 14 insertions(+), 2 deletions(-)
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index 084809d43bd..1f0b29667ab 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -28,7 +28,7 @@ open Memory
(* --- L-Values & Expressions --- *)
(* -------------------------------------------------------------------------- *)
-type value = { from : node option ; ptr : node option }
+type scalar = { from : node option ; ptr : node option }
let integral = { from = None ; ptr = None }
let pointer m v =
match v.ptr with
@@ -57,7 +57,7 @@ and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
and add_value m s e = ignore (add_exp m s e)
-and add_exp (m: map) (s:stmt) (e:exp) : value =
+and add_exp (m: map) (s:stmt) (e:exp) : scalar =
match e.enode with
| AddrOf lv | StartOf lv ->
@@ -120,6 +120,13 @@ let add_instr (m:map) (s:stmt) (instr:instr) =
match instr with
| Skip _ | Code_annot _ -> ()
+ | Set(lv, { enode = Lval exp }, _) ->
+ let l = add_lval m s lv in
+ let r = add_lval m s exp in
+ Memory.read m l (Lval(s,exp)) ;
+ Memory.write m l (Lval(s,lv)) ;
+ Memory.merge_copy m ~l ~r
+
| Set(lv,e,_) ->
let r = add_lval m s lv in
let v = add_exp m s e in
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index d1dd5198156..e10914c98eb 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -444,6 +444,10 @@ let merge (m: map) (a: node) (b: node) : unit =
failwith_locked m "Region.Memory.merge" ;
merge_all m [a;b]
+let merge_copy (m: map) ~(l: node) ~(r: node) : unit =
+ let { clayout } = get m r in
+ merge_all m [ l; Ufind.make m.store { empty with clayout } ]
+
(* -------------------------------------------------------------------------- *)
(* --- Offset --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index e15853e9530..788ed51359d 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -87,6 +87,7 @@ val shift : map -> node -> Access.acs -> unit
val merge : map -> node -> node -> unit
val merge_all : map -> node list -> unit
+val merge_copy : map -> l:node -> r:node -> unit
(** @raise Not_found *)
val lval : map -> lval -> node
--
GitLab