diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml index 084809d43bd2e06bce04f8841270269b391f166a..858b1a02cda82c4aa449c73ace700e7289e2da88 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 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 diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index d1dd5198156ed560a08d6e5000dfeee44d623134..e10914c98ebc6e5503c32ea4d5adc40d65b3a869 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 e15853e9530b642cef5d9dbb5ad2e6ace8314dcb..788ed51359df0959c63ffe2da17495f357ae9c63 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 diff --git a/src/plugins/region/tests/region/oracle/comp.res.oracle b/src/plugins/region/tests/region/oracle/comp.res.oracle index 11ade26af7604de77361f0715a788f2355f7b9be..f73256e38a6e7ec99715ae0edf5f6e15e2bb1da0 100644 --- a/src/plugins/region/tests/region/oracle/comp.res.oracle +++ b/src/plugins/region/tests/region/oracle/comp.res.oracle @@ -1,9 +1,9 @@ [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 ; diff --git a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle index 66f3883ad46b3b4827cb09b10c92c78b6276ff60..db2191393f4788d8cdd0d304779db01b93806d44 100644 --- a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle +++ b/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) ;