Merge branch 'feature/region/merge-copy' into 'master'

[region] merge copy

See merge request frama-c/frama-c!4691

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 r (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

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                                                             --- *)
 (* -------------------------------------------------------------------------- *)

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

src/plugins/region/tests/region/oracle/comp.res.oracle

 [kernel] Parsing comp.c (with preprocessing)
 [region] Analyzing regions
 [region] Function f:
-  R0003: --- s 192b { .x: R0004; #32b; .z: R0007; .arr: R000b; } ;
+  R0003: --- s 192b { .x: R0004; #32b; .z: R0008; .arr: R000c; } ;
   R0004: -W- (int) 32b ;
-  R0007: -W- (int *) 64b (*R0001) ;
+  R0008: -W- (int *) 64b (*R0001) ;
   R0001: RW- a (int) 32b ;
-  R000b: --- 64b { #64b: R000d[4]; } ;
-  R000d: -W- (short) 16b ;
+  R000c: --- 64b { #64b: R000e[4]; } ;
+  R000e: -W- (short) 16b ;

src/plugins/region/tests/region/oracle/fb_SORT.res.oracle

@@ -7,10 +7,10 @@
       .prm.inp1: R0007[2];
       #128b;
       .out1: R000e;
-      .out2: R0066;
+      .out2: R0067;
       .out3.idx1: R0015[2];
       #128b;
-      .sum: R0053;
+      .sum: R0054;
     } ;
   R0007: R-- (struct N *) 64b (*R0024) ;
   R0024: --- 128b { .v: R0026; .s: R0046; #32b; } ;
@@ -20,16 +20,16 @@
   R001d: --- 128b { .v: R001f; .s: R0038; #32b; } ;
   R001f: RW- (double) 64b ;
   R0038: -W- (int) 32b ;
-  R0066: R-- (struct N *) 64b (*R0069) ;
-  R0069: --- 128b { .v: R006b; #64b; } ;
-  R006b: R-- (double) 64b ;
+  R0067: R-- (struct N *) 64b (*R006a) ;
+  R006a: --- 128b { .v: R006c; #64b; } ;
+  R006c: R-- (double) 64b ;
   R0015: R-- (struct N *) (struct L *) 64b (*R003e) ;
   R003e: --- 64b { .v.s: R0040[2]; } ;
   R0040: RW- (int) (double) 32b ;
-  R0053: R-- (struct N *) 64b (*R0056) ;
-  R0056: --- 128b { .v: R0058; .s: R007f; #32b; } ;
-  R0058: -W- (double) 64b ;
-  R007f: -W- (int) 32b ;
+  R0054: R-- (struct N *) 64b (*R0057) ;
+  R0057: --- 128b { .v: R0059; .s: R0080; #32b; } ;
+  R0059: -W- (double) 64b ;
+  R0080: -W- (int) 32b ;
   R0001: RWA inp (SN *) 64b (*R0007) ;
   R000a: RWA out (SN *) 64b (*R000e) ;
   R0011: RWA idx (SL *) 64b (*R0015) ;