From dfe6509498dd6e1337ff3525440102e460527cd4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 12 Jun 2024 09:05:03 +0200
Subject: [PATCH] [region] adding tests
---
nix/plugins-tests.nix | 1 +
src/plugins/region/store.ml | 1 +
src/plugins/region/tests/ptests_config | 1 +
src/plugins/region/tests/region/fb_ADD.i | 22 +++++++++++
src/plugins/region/tests/region/fb_SORT.i | 38 +++++++++++++++++++
src/plugins/region/tests/region/garbled.i | 6 +++
.../tests/region/oracle/fb_ADD.res.oracle | 13 +++++++
.../tests/region/oracle/fb_SORT.res.oracle | 33 ++++++++++++++++
.../tests/region/oracle/garbled.res.oracle | 8 ++++
.../tests/region/oracle/swap.res.oracle | 13 +++++++
src/plugins/region/tests/region/swap.i | 29 ++++++++++++++
src/plugins/region/tests/test_config | 2 +
12 files changed, 167 insertions(+)
create mode 100644 src/plugins/region/tests/ptests_config
create mode 100644 src/plugins/region/tests/region/fb_ADD.i
create mode 100644 src/plugins/region/tests/region/fb_SORT.i
create mode 100644 src/plugins/region/tests/region/garbled.i
create mode 100644 src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
create mode 100644 src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
create mode 100644 src/plugins/region/tests/region/oracle/garbled.res.oracle
create mode 100644 src/plugins/region/tests/region/oracle/swap.res.oracle
create mode 100644 src/plugins/region/tests/region/swap.i
create mode 100644 src/plugins/region/tests/test_config
diff --git a/nix/plugins-tests.nix b/nix/plugins-tests.nix
index a500d6d0ce1..b6a83abadd1 100644
--- a/nix/plugins-tests.nix
+++ b/nix/plugins-tests.nix
@@ -24,6 +24,7 @@ mk_tests {
@src/plugins/markdown-report/tests/ptests \
@src/plugins/nonterm/tests/ptests \
@src/plugins/report/tests/ptests \
+ @src/plugins/region/tests/ptests \
@src/plugins/server/tests/ptests \
@src/plugins/variadic/tests/ptests
'';
diff --git a/src/plugins/region/store.ml b/src/plugins/region/store.ml
index 7e6121b5da9..4e964e42b37 100644
--- a/src/plugins/region/store.ml
+++ b/src/plugins/region/store.ml
@@ -32,6 +32,7 @@ type 'a store = 'a Imap.t ref
let new_store () = ref Imap.empty
let copy r = ref !r
let rid = ref 0
+
let make s v =
let k = incr rid ; !rid in
s := Imap.add k v !s ; k
diff --git a/src/plugins/region/tests/ptests_config b/src/plugins/region/tests/ptests_config
new file mode 100644
index 00000000000..31616617052
--- /dev/null
+++ b/src/plugins/region/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= region
diff --git a/src/plugins/region/tests/region/fb_ADD.i b/src/plugins/region/tests/region/fb_ADD.i
new file mode 100644
index 00000000000..8ceb168c7af
--- /dev/null
+++ b/src/plugins/region/tests/region/fb_ADD.i
@@ -0,0 +1,22 @@
+typedef struct N { double v ; int s ; } *SN ;
+typedef struct L { int v ; int s ; } *SL ;
+
+typedef struct Block {
+ SN prm ;
+ SN inp1 ;
+ SN inp2 ;
+ SN inp3 ;
+ SN out1 ;
+ SN out2 ;
+ SN out3 ;
+ SL idx1 ;
+ SL idx2 ;
+ SL idx3 ;
+ SN sum ;
+} FB ;
+
+void job(FB *fb)
+{
+ fb->out1->v = fb->out1->v + fb->out2->v ;
+ fb->out1->s = fb->out1->s | fb->out2->s ;
+}
diff --git a/src/plugins/region/tests/region/fb_SORT.i b/src/plugins/region/tests/region/fb_SORT.i
new file mode 100644
index 00000000000..4ef65d2cfb6
--- /dev/null
+++ b/src/plugins/region/tests/region/fb_SORT.i
@@ -0,0 +1,38 @@
+typedef struct N { double v ; int s ; } *SN ;
+typedef struct L { int v ; int s ; } *SL ;
+
+typedef struct Block {
+ SN prm ;
+ SN inp1 ;
+ SN inp2 ;
+ SN inp3 ;
+ SN out1 ;
+ SN out2 ;
+ SN out3 ;
+ SL idx1 ;
+ SL idx2 ;
+ SL idx3 ;
+ SN sum ;
+} FB ;
+
+void job(FB *fb)
+{
+ SN *inp = &(fb->inp1) ;
+ SN *out = &(fb->out1) ;
+ SL *idx = &(fb->idx1) ;
+
+ for (int i = 0; i < 3; i++) {
+ out[i]->v = inp[i]->v + fb->prm->v ;
+ out[i]->s = 0 ;
+ idx[i]->v = inp[i]->s ;
+ idx[i]->s = 0 ;
+ }
+
+ fb->sum->v =
+ fb->out1->v +
+ fb->out2->v +
+ fb->out3->v ;
+
+ fb->sum->s = 0 ;
+
+}
diff --git a/src/plugins/region/tests/region/garbled.i b/src/plugins/region/tests/region/garbled.i
new file mode 100644
index 00000000000..6b703ba4245
--- /dev/null
+++ b/src/plugins/region/tests/region/garbled.i
@@ -0,0 +1,6 @@
+
+
+float job(int *p,int *q)
+{
+ return *q + *(float*)p + *p ;
+}
diff --git a/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
new file mode 100644
index 00000000000..84e4fe84a13
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing fb_ADD.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0001: R-- fb (FB *) 64b (*R0003) ;
+ R0003: --- 704b 256..320 [1]: R0005 320..384 [1]: R0018 ;
+ R0005: R-- (struct N *) 64b (*R0008) ;
+ R0008: --- 128b 0..64 [1]: R000a 64..96 [1]: R0027 ;
+ R000a: RW- (double) 64b ;
+ R0027: RW- (int) 32b ;
+ R0018: R-- (struct N *) 64b (*R001b) ;
+ R001b: --- 128b 0..64 [1]: R001d 64..96 [1]: R003a ;
+ R001d: R-- (double) 64b ;
+ R003a: R-- (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
new file mode 100644
index 00000000000..eec439e3a9f
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
@@ -0,0 +1,33 @@
+[kernel] Parsing fb_SORT.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0003: R-- fb (FB *) 64b (*R0005) ;
+ R0005: ---
+ 704b
+ 0..128 [2]: R0007
+ 256..320 [1]: R000e
+ 320..384 [1]: R0066
+ 384..512 [2]: R0015
+ 640..704 [1]: R0053 ;
+ R0007: R-- (struct N *) 64b (*R0024) ;
+ R0024: --- 128b 0..64 [1]: R0026 64..96 [1]: R0046 ;
+ R0026: R-- (double) 64b ;
+ R0046: R-- (int) 32b ;
+ R000e: R-- (struct N *) 64b (*R001d) ;
+ R001d: --- 128b 0..64 [1]: R001f 64..96 [1]: R0038 ;
+ R001f: RW- (double) 64b ;
+ R0038: -W- (int) 32b ;
+ R0066: R-- (struct N *) 64b (*R0069) ;
+ R0069: --- 128b 0..64 [1]: R006b ;
+ R006b: R-- (double) 64b ;
+ R0015: R-- (struct N *) (struct L *) 64b (*R003e) ;
+ R003e: --- 64b 0..64 [2]: R0040 ;
+ R0040: RW- (int) (double) 32b ;
+ R0053: R-- (struct N *) 64b (*R0056) ;
+ 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) ;
+ R0018: RW- i (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/garbled.res.oracle b/src/plugins/region/tests/region/oracle/garbled.res.oracle
new file mode 100644
index 00000000000..024e97e7a34
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/garbled.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing garbled.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0007: R-- p (int *) 64b (*R0009) ;
+ R0009: R-- (int) (float) 32b ;
+ R0002: R-- q (int *) 64b (*R0004) ;
+ R0004: R-- (int) 32b ;
+ R0001: RW- __retres (float) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/swap.res.oracle b/src/plugins/region/tests/region/oracle/swap.res.oracle
new file mode 100644
index 00000000000..3117fb686d5
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/swap.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing swap.i (no preprocessing)
+[region] Analyzing regions
+[region] Function swap_aliased:
+ R0004: R-- a (int *) 64b (*R0007) ;
+ R0007: RW- R: (int) 32b ;
+ R0001: R-- b (int *) 64b (*R0007) ;
+ R0008: RW- tmp (int) 32b ;
+[region] Function swap_separated:
+ R0013: R-- a (int *) 64b (*R0016) ;
+ R0016: RW- A: (int) 32b ;
+ R0017: R-- b (int *) 64b (*R001a) ;
+ R001a: RW- B: (int) 32b ;
+ R001b: RW- tmp (int) 32b ;
diff --git a/src/plugins/region/tests/region/swap.i b/src/plugins/region/tests/region/swap.i
new file mode 100644
index 00000000000..04816ea5fd8
--- /dev/null
+++ b/src/plugins/region/tests/region/swap.i
@@ -0,0 +1,29 @@
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region A: *a, B: *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_separated(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
+
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region R: *a, *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_aliased(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
diff --git a/src/plugins/region/tests/test_config b/src/plugins/region/tests/test_config
new file mode 100644
index 00000000000..4772d6b3666
--- /dev/null
+++ b/src/plugins/region/tests/test_config
@@ -0,0 +1,2 @@
+PLUGIN: region
+OPT: -region
--
GitLab