From a8bc3da2964f8c4e8fc11ed5910530ede8b3a582 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 17 Jun 2024 14:39:49 +0200
Subject: [PATCH] [region] added shift access
---
src/plugins/region/code.ml | 50 +++++++++++--------
src/plugins/region/tests/region/array1.i | 8 +++
src/plugins/region/tests/region/array2.i | 8 +++
.../tests/region/oracle/array1.res.oracle | 9 ++++
.../tests/region/oracle/array2.res.oracle | 10 ++++
.../tests/region/oracle/fb_SORT.res.oracle | 6 +--
6 files changed, 66 insertions(+), 25 deletions(-)
create mode 100644 src/plugins/region/tests/region/array1.i
create mode 100644 src/plugins/region/tests/region/array2.i
create mode 100644 src/plugins/region/tests/region/oracle/array1.res.oracle
create mode 100644 src/plugins/region/tests/region/oracle/array2.res.oracle
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index 2e2aa7f154e..93bbc497df4 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -28,13 +28,23 @@ open Memory
(* --- L-Values & Expressions --- *)
(* -------------------------------------------------------------------------- *)
+type value = { from : node option ; ptr : node option }
+let integral = { from = None ; ptr = None }
+let pointer m v =
+ match v.ptr with
+ | Some p -> v, p
+ | None ->
+ let p = add_cell m () in
+ Option.iter (fun s -> Memory.add_points_to m s p) v.from ;
+ { v with ptr = Some p }, p
+
let rec add_lval (m:map) (s:stmt) (lv:lval) : node =
let h = fst lv in
add_loffset m s (add_lhost m s h) (Cil.typeOfLhost h) (snd lv)
and add_lhost (m:map) (s:stmt) = function
| Var x -> Memory.add_root m x
- | Mem e -> add_pointer m s e
+ | Mem e -> snd @@ pointer m @@ add_exp m s e
and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
| NoOffset -> r
@@ -43,47 +53,43 @@ and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
| Index(_,ofs) ->
add_loffset m s (add_index m r ty) (Cil.typeOf_array_elem ty) ofs
-and add_pointer m s e = match add_exp m s e with None -> add_cell m () | Some r -> r
-
and add_value m s e = ignore (add_exp m s e)
-and add_exp (m: map) (s:stmt) (e:exp) : node option =
+and add_exp (m: map) (s:stmt) (e:exp) : value =
match e.enode with
| AddrOf lv | StartOf lv ->
- let rv = add_lval m s lv in
- Some rv
+ let rv = Some (add_lval m s lv) in
+ { from = rv ; ptr = rv }
| Lval lv ->
let rv = add_lval m s lv in
Memory.read m rv (Lval(s,lv)) ;
- Memory.add_value m rv @@ Cil.typeOfLval lv
-
- | UnOp(_,e,_) ->
- add_value m s e ; None
+ let ptr = Memory.add_value m rv @@ Cil.typeOfLval lv in
+ { from = Some rv ; ptr }
| BinOp((PlusPI|MinusPI),p,k,_) ->
add_value m s k ;
- let r = add_pointer m s p in
- (*TODO: move the 'A' access on the source of the pointed region *)
- (*Memory.shift m r (Exp(s,p)) ;*)
- Some r
+ let v = add_exp m s p in
+ Option.iter (fun r -> Memory.shift m r (Exp(s,e))) v.from ; v
+
+ | UnOp(_,e,_) ->
+ add_value m s e ; integral
| BinOp(_,a,b,_) ->
- add_value m s a ;
- add_value m s b ;
- None
+ add_value m s a ; add_value m s b ; integral
| CastE(ty,p) ->
+ let v = add_exp m s p in
if Cil.isPointerType ty then
- Some (add_pointer m s p)
+ fst @@ pointer m @@ v
else
- (add_value m s p ; None)
+ integral
| Const _
| SizeOf _ | SizeOfE _ | SizeOfStr _
| AlignOf _ | AlignOfE _
- -> None
+ -> integral
(* -------------------------------------------------------------------------- *)
(* --- Initializers --- *)
@@ -95,7 +101,7 @@ let rec add_init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
| SingleInit e ->
let r = add_lval m s lv in
Memory.write m r acs ;
- Option.iter (Memory.add_points_to m r) (add_exp m s e)
+ Option.iter (Memory.add_points_to m r) (add_exp m s e).ptr
| CompoundInit(_,fvs) ->
List.iter
@@ -116,7 +122,7 @@ let add_instr (m:map) (s:stmt) (instr:instr) =
let r = add_lval m s lv in
let v = add_exp m s e in
Memory.write m r (Lval(s,lv)) ;
- Option.iter (Memory.add_points_to m r) v
+ Option.iter (Memory.add_points_to m r) v.ptr
| Local_init(x,AssignInit iv,_) ->
let acs = Access.Init(s,x) in
diff --git a/src/plugins/region/tests/region/array1.i b/src/plugins/region/tests/region/array1.i
new file mode 100644
index 00000000000..eac00551a13
--- /dev/null
+++ b/src/plugins/region/tests/region/array1.i
@@ -0,0 +1,8 @@
+//@ region *p, *q ;
+int job( int n, int * p , int * q )
+{
+ int s = 0 ;
+ for (int k = 0; k < n; k++)
+ s += p[k] * q[k] ;
+ return s ;
+}
diff --git a/src/plugins/region/tests/region/array2.i b/src/plugins/region/tests/region/array2.i
new file mode 100644
index 00000000000..a9cbb53d7ff
--- /dev/null
+++ b/src/plugins/region/tests/region/array2.i
@@ -0,0 +1,8 @@
+//@ region P: *p, Q: *q ;
+int job( int n, int * p , int * q )
+{
+ int s = 0 ;
+ for (int k = 0; k < n; k++)
+ s += p[k] * q[k] ;
+ return s ;
+}
diff --git a/src/plugins/region/tests/region/oracle/array1.res.oracle b/src/plugins/region/tests/region/oracle/array1.res.oracle
new file mode 100644
index 00000000000..32aa817c98c
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/array1.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing array1.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R000b: R-- n (int) 32b ;
+ R0004: R-A p (int *) 64b (*R0002) ;
+ R0002: R-- (int) 32b ;
+ R0001: R-A q (int *) 64b (*R0002) ;
+ R0007: RW- s (int) 32b ;
+ R0009: RW- k (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/array2.res.oracle b/src/plugins/region/tests/region/oracle/array2.res.oracle
new file mode 100644
index 00000000000..03db359956c
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/array2.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing array2.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R000d: R-- n (int) 32b ;
+ R0001: R-A p (int *) 64b (*R0004) ;
+ R0004: R-- P: (int) 32b ;
+ R0005: R-A q (int *) 64b (*R0008) ;
+ R0008: R-- Q: (int) 32b ;
+ R0009: RW- s (int) 32b ;
+ R000b: RW- k (int) 32b ;
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 eec439e3a9f..912201cee70 100644
--- a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
+++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
@@ -27,7 +27,7 @@
R0056: --- 128b 0..64 [1]: R0058 64..96 [1]: R007f ;
R0058: -W- (double) 64b ;
R007f: -W- (int) 32b ;
- R0001: RW- inp (SN *) 64b (*R0007) ;
- R000a: RW- out (SN *) 64b (*R000e) ;
- R0011: RW- idx (SL *) 64b (*R0015) ;
+ R0001: RWA inp (SN *) 64b (*R0007) ;
+ R000a: RWA out (SN *) 64b (*R000e) ;
+ R0011: RWA idx (SL *) 64b (*R0015) ;
R0018: RW- i (int) 32b ;
--
GitLab