From 150618d5e290ef8a5a62a85a6fb5fc874310ee67 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 21 Jan 2021 17:44:32 +0100
Subject: [PATCH] [wp] Add tests for nesting with -wp-unfold-assigns
---
.../oracle/unfold_assigns.0.res.oracle | 175 +++++++++++++++++-
.../oracle/unfold_assigns.1.res.oracle | 159 +++++++++++++++-
.../wp/tests/wp_plugin/unfold_assigns.i | 50 ++++-
3 files changed, 371 insertions(+), 13 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
index 8178bf2d553..830f0028545 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
@@ -25,6 +25,66 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFO
Effect at line 59
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 92
+Assume {
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, s, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 92
+Assume {
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, s, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
+Call Effect at line 98
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, s, 4).
+ (* Pre-condition *)
+ Have: 3 <= n.
+}
+Prove: included(s, 4, shift_sint32(shiftfield_F2_With_array_t(s), 1), n).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
+Call Effect at line 98
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, s, 4).
+ (* Pre-condition *)
+ Have: 3 <= n.
+}
+Prove: included(s, 4, shift_sint32(shiftfield_F2_With_array_t(s), 1), n).
+
------------------------------------------------------------
------------------------------------------------------------
Function NO_UNFOLD_KO
@@ -99,11 +159,38 @@ Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function PARTIAL_ASSIGNS
+ Function PARTIAL_ASSIGNS_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 73
+Assume {
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_sint32(p, 0), 5).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 73
+Assume {
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_sint32(p, 0), 5).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function PARTIAL_ASSIGNS_VARS
------------------------------------------------------------
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
-Call Effect at line 74
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 79
Let a = shift_sint32(p, 0).
Let x = 1 + n.
Assume {
@@ -121,8 +208,8 @@ Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
------------------------------------------------------------
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
-Call Effect at line 74
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 79
Let a = shift_sint32(p, 0).
Let x = 1 + n.
Assume {
@@ -138,6 +225,84 @@ Assume {
Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
included(a, x, shift_sint32(p, n), 1).
+------------------------------------------------------------
+------------------------------------------------------------
+ Function RANGE_NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 109
+Assume {
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_S2_With_array(s, 0), 12).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 109
+Assume {
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_S2_With_array(s, 0), 12).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function RANGE_NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 118
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 1).
+Let a_2 = shiftfield_F2_With_array_t(a).
+Assume {
+ Type: is_uint32(m) /\ is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, x_1).
+ (* Pre-condition *)
+ Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, shift_S2_With_array(s, 2), x - 4) \/
+ included(a, x_1, shiftfield_F2_With_array_x(a_1), 1) \/
+ included(a, x_1, shift_sint32(a_2, 0), 1) \/
+ included(a, x_1, shift_sint32(a_2, 1), m) \/
+ included(a, x_1, shift_sint32(shiftfield_F2_With_array_t(a_1), 0), 1 + m).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 118
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 1).
+Let a_2 = shiftfield_F2_With_array_t(a).
+Assume {
+ Type: is_uint32(m) /\ is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, x_1).
+ (* Pre-condition *)
+ Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, shift_S2_With_array(s, 2), x - 4) \/
+ included(a, x_1, shiftfield_F2_With_array_x(a_1), 1) \/
+ included(a, x_1, shift_sint32(a_2, 0), 1) \/
+ included(a, x_1, shift_sint32(a_2, 1), m) \/
+ included(a, x_1, shift_sint32(shiftfield_F2_With_array_t(a_1), 0), 1 + m).
+
------------------------------------------------------------
------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
index cb15fe7af3f..67d30e1a6e8 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
@@ -19,6 +19,56 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFO
Effect at line 59
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 92
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 92
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
+Call Effect at line 98
+Let a = shiftfield_F2_With_array_t(s).
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, s, 4).
+ (* Pre-condition *)
+ Have: 3 <= n.
+}
+Prove: (0 < n) /\ included(shift_sint32(a, 2), 1, shift_sint32(a, 1), n).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
+Call Effect at line 98
+Let a = shiftfield_F2_With_array_t(s).
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, s, 4).
+ (* Pre-condition *)
+ Have: 3 <= n.
+}
+Prove: (0 < n) /\ included(shift_sint32(a, 2), 1, shift_sint32(a, 1), n).
+
------------------------------------------------------------
------------------------------------------------------------
Function NO_UNFOLD_KO
@@ -81,11 +131,26 @@ Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function PARTIAL_ASSIGNS
+ Function PARTIAL_ASSIGNS_STATIC
------------------------------------------------------------
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
-Call Effect at line 74
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 73
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 73
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function PARTIAL_ASSIGNS_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 79
Assume {
Type: is_uint32(n).
(* Heap *)
@@ -101,8 +166,8 @@ Prove: (i = 0) \/ (n = i) \/
------------------------------------------------------------
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
-Call Effect at line 74
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 79
Assume {
Type: is_uint32(n).
(* Heap *)
@@ -116,6 +181,90 @@ Assume {
Prove: (i = 0) \/ (n = i) \/
included(shift_sint32(p, i), 1, shift_sint32(p, 1), n - 1).
+------------------------------------------------------------
+------------------------------------------------------------
+ Function RANGE_NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 109
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 109
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function RANGE_NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 118
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let a_1 = shift_S2_With_array(s, i).
+Let a_2 = shiftfield_F2_With_array_t(a_1).
+Let a_3 = shift_sint32(a_2, 1).
+Let a_4 = shift_S2_With_array(s, 2).
+Let x_1 = x - 4.
+Let a_5 = shift_sint32(shiftfield_F2_With_array_t(a), 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(shift_S2_With_array(s, 1)),
+ 0).
+Let x_2 = 1 + m.
+Let a_7 = shift_sint32(a_2, 2).
+Let a_8 = shiftfield_F2_With_array_x(a_1).
+Assume {
+ Type: is_uint32(m) /\ is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, 4 + x)).
+ (* Pre-condition *)
+ Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (included(a_3, 1, a_4, x_1) \/ included(a_3, 1, a_5, m) \/
+ included(a_3, 1, a_6, x_2)) /\
+ (included(a_7, 1, a_4, x_1) \/ included(a_7, 1, a_5, m) \/
+ included(a_7, 1, a_6, x_2)) /\
+ ((i = 0) \/ (i = 1) \/ included(a_8, 1, a_4, x_1) \/
+ included(a_8, 1, a_5, m) \/ included(a_8, 1, a_6, x_2)).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 118
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let a_1 = shift_S2_With_array(s, i).
+Let a_2 = shiftfield_F2_With_array_t(a_1).
+Let a_3 = shift_sint32(a_2, 1).
+Let a_4 = shift_S2_With_array(s, 2).
+Let x_1 = x - 4.
+Let a_5 = shift_sint32(shiftfield_F2_With_array_t(a), 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(shift_S2_With_array(s, 1)),
+ 0).
+Let x_2 = 1 + m.
+Let a_7 = shift_sint32(a_2, 2).
+Let a_8 = shiftfield_F2_With_array_x(a_1).
+Assume {
+ Type: is_uint32(m) /\ is_uint32(n).
+ (* Heap *)
+ Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, 4 + x)).
+ (* Pre-condition *)
+ Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (included(a_3, 1, a_4, x_1) \/ included(a_3, 1, a_5, m) \/
+ included(a_3, 1, a_6, x_2)) /\
+ (included(a_7, 1, a_4, x_1) \/ included(a_7, 1, a_5, m) \/
+ included(a_7, 1, a_6, x_2)) /\
+ ((i = 0) \/ (i = 1) \/ included(a_8, 1, a_4, x_1) \/
+ included(a_8, 1, a_5, m) \/ included(a_8, 1, a_6, x_2)).
+
------------------------------------------------------------
------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
index 24c9a9347bd..ee722b12771 100644
--- a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
+++ b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
@@ -66,10 +66,54 @@ void ASSIGN_NO_UNFOLD_KO(struct S *s) {
}
/*@ assigns *(p+(0..n)); */
-void f_assigns_array(int *p, unsigned n);
+void f_assigns_range(int *p, unsigned n);
+
+/*@ assigns *(p+0), *(p+(1..3)), *(p+4); */
+void PARTIAL_ASSIGNS_STATIC(int *p) {
+ f_assigns_range(p, 4);
+}
/*@ requires n > 4 ;
assigns *(p+0), *(p+(1..n-1)), *(p+n); */
-void PARTIAL_ASSIGNS(int *p, unsigned n) {
- f_assigns_array(p, n);
+void PARTIAL_ASSIGNS_VARS(int *p, unsigned n) {
+ f_assigns_range(p, n);
+}
+
+struct With_array {
+ int x ;
+ int t [3] ;
+};
+
+//@ assigns *s ;
+void f_assigns_with_array(struct With_array* s);
+
+//@ assigns s->x, s->t[0], s->t[1..2] ;
+void NESTED_ARRAY_STATIC(struct With_array *s){
+ f_assigns_with_array(s);
+}
+
+/*@ requires n > 2 ;
+ assigns s->x, s->t[0], s->t[1..n] ; */
+void NESTED_ARRAY_VARS(struct With_array *s, unsigned n){
+ f_assigns_with_array(s);
+}
+
+//@ assigns *(s+(0..n)) ;
+void f_assigns_range_with_array(struct With_array* s, unsigned n);
+
+/*@ assigns s[0].x, s[0].t[0], s[0].t[1..2],
+ s[1].x, s[1].t[0..2],
+ s[2];
+*/
+void RANGE_NESTED_ARRAY_STATIC(struct With_array* s){
+ f_assigns_range_with_array(s, 2);
+}
+
+/*@ requires n > 2 && m > 3 ;
+ assigns s[0].x, s[0].t[0], s[0].t[1..m],
+ s[1].x, s[1].t[0..m],
+ s[2 .. n];
+*/
+void RANGE_NESTED_ARRAY_VARS(struct With_array* s, unsigned n, unsigned m){
+ f_assigns_range_with_array(s, n);
}
--
GitLab