From 9bc721cfc35ddab861f9d567623c277527c6dff9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 9 Oct 2024 18:35:00 +0200
Subject: [PATCH] [wp/region] optimized array test
---
src/plugins/wp/tests/wp_region/array.c | 3 -
.../tests/wp_region/oracle/array.res.oracle | 129 ++++++------------
.../wp_region/oracle_qualif/array.res.oracle | 14 +-
3 files changed, 44 insertions(+), 102 deletions(-)
diff --git a/src/plugins/wp/tests/wp_region/array.c b/src/plugins/wp/tests/wp_region/array.c
index dcc7a41a65a..825ceb18aeb 100644
--- a/src/plugins/wp/tests/wp_region/array.c
+++ b/src/plugins/wp/tests/wp_region/array.c
@@ -18,9 +18,6 @@ void add_first4(struct S * a , struct S * b )
{
a->content[0] += b->content[0];
a->content[1] += b->content[1];
- note1:
a->content[2] += b->content[2];
- //@ assert a!=b ==> a->content[2] == \at(a->content[2],note1) + b->content[2];
- //@ assert a==b ==> a->content[2] == 2*\at(a->content[2],note1);
a->content[3] += b->content[3];
}
diff --git a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
index 1c937abfbab..58726365345 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
@@ -4,8 +4,6 @@
[wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
[wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
------------------------------------------------------------
Function add_first4
------------------------------------------------------------
@@ -14,38 +12,36 @@ Goal Post-condition (file array.c, line 12) in 'add_first4':
Let a_1 = shiftfield_F1_S_content(a).
Let a_2 = shift_sint32(a_1, 0).
Let x = Msint32_0[a_2].
-Let a_3 = shiftfield_F1_S_content(b).
-Let x_1 = Msint32_0[shift_sint32(a_3, 0)].
-Let m = Msint32_0[a_2 <- x + x_1].
-Let a_4 = shift_sint32(a_1, 1).
+Let a_3 = shift_sint32(a_1, 1).
+Let x_1 = Msint32_0[a_3].
+Let a_4 = shift_sint32(a_1, 2).
Let x_2 = Msint32_0[a_4].
-Let x_3 = m[shift_sint32(a_3, 1)].
-Let m_1 = m[a_4 <- x_2 + x_3].
-Let a_5 = shift_sint32(a_1, 2).
-Let x_4 = Msint32_0[a_5].
-Let a_6 = shift_sint32(a_3, 2).
-Let x_5 = m_1[a_6].
-Let x_6 = x_4 + x_5.
-Let m_2 = m_1[a_5 <- x_6].
-Let a_7 = shift_sint32(a_1, 3).
-Let x_7 = Msint32_0[a_7].
-Let x_8 = m_2[shift_sint32(a_3, 3)].
-Let x_9 = m_2[a_7 <- x_7 + x_8][a_6].
+Let a_5 = shift_sint32(a_1, 3).
+Let x_3 = Msint32_0[a_5].
+Let a_6 = shiftfield_F1_S_content(b).
+Let x_4 = Msint32_0[shift_sint32(a_6, 0)].
+Let a_7 = shift_sint32(a_6, 2).
+Let m = Msint32_0[a_2 <- x + x_4].
+Let x_5 = m[shift_sint32(a_6, 1)].
+Let m_1 = m[a_3 <- x_1 + x_5].
+Let x_6 = m_1[a_7].
+Let x_7 = x_2 + x_6.
+Let m_2 = m_1[a_4 <- x_7].
+Let x_8 = m_2[shift_sint32(a_6, 3)].
+Let x_9 = m_2[a_5 <- x_3 + x_8][a_7].
Assume {
- Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_4) /\ is_sint32(x_7) /\
- is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_1) /\
- is_sint32(Msint32_0[a_6]) /\ is_sint32(x_3) /\ is_sint32(x_5) /\
- is_sint32(x_6) /\ is_sint32(x_8) /\ is_sint32(x_9).
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_4) /\
+ is_sint32(Msint32_0[a_7]) /\ is_sint32(x_5) /\ is_sint32(x_6) /\
+ is_sint32(x_7) /\ is_sint32(x_8) /\ is_sint32(x_9).
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
(* Goal *)
When: b != a.
(* Pre-condition *)
Have: P_pointed(a, b).
- (* Assertion *)
- Have: m_2[a_6] = x_5.
}
-Prove: x_9 = x_5.
+Prove: x_9 = x_6.
------------------------------------------------------------
@@ -58,77 +54,30 @@ Goal Post-condition (file array.c, line 14) in 'add_first4':
Let a_1 = shiftfield_F1_S_content(a).
Let a_2 = shift_sint32(a_1, 0).
Let x = Msint32_0[a_2].
-Let a_3 = shiftfield_F1_S_content(b).
-Let x_1 = Msint32_0[shift_sint32(a_3, 0)].
-Let m = Msint32_0[a_2 <- x + x_1].
-Let a_4 = shift_sint32(a_1, 1).
-Let x_2 = Msint32_0[a_4].
-Let x_3 = m[shift_sint32(a_3, 1)].
-Let m_1 = m[a_4 <- x_2 + x_3].
-Let a_5 = shift_sint32(a_3, 2).
-Let x_4 = m_1[a_5].
-Let a_6 = shift_sint32(a_1, 2).
-Let x_5 = Msint32_0[a_6].
-Let x_6 = x_5 + x_4.
-Let m_2 = m_1[a_6 <- x_6].
-Let x_7 = m_2[a_5].
-Let a_7 = shift_sint32(a_1, 3).
-Let x_8 = Msint32_0[a_7].
-Let x_9 = Msint32_0[a_5].
-Let x_10 = m_2[shift_sint32(a_3, 3)].
-Assume {
- Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_8) /\
- is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_1) /\
- is_sint32(x_9) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x_6) /\
- is_sint32(x_7) /\ is_sint32(x_10) /\
- is_sint32(m_2[a_7 <- x_8 + x_10][a_5]).
- (* Heap *)
- Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
- (* Pre-condition *)
- Have: P_pointed(a, b).
- (* Assertion *)
- Have: ((b != a) -> (x_7 = x_4)).
- (* Assertion *)
- Have: ((b = a) -> (x_4 = x_5)).
-}
-Prove: x_4 = x_9.
-
-------------------------------------------------------------
-
-Goal Post-condition (file array.c, line 15) in 'add_first4':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (file array.c, line 23):
-Let a_1 = shiftfield_F1_S_content(a).
-Let a_2 = shift_sint32(a_1, 0).
-Let x = Msint32_0[a_2].
Let a_3 = shift_sint32(a_1, 1).
Let x_1 = Msint32_0[a_3].
Let a_4 = shift_sint32(a_1, 2).
Let x_2 = Msint32_0[a_4].
-Let a_5 = shiftfield_F1_S_content(b).
-Let x_3 = Msint32_0[shift_sint32(a_5, 0)].
-Let a_6 = shift_sint32(a_5, 2).
-Let m = Msint32_0[a_2 <- x + x_3].
-Let x_4 = m[shift_sint32(a_5, 1)].
-Let m_1 = m[a_3 <- x_1 + x_4].
-Let x_5 = m_1[a_6].
-Let x_6 = x_2 + x_5.
-Let m_2 = m_1[a_4 <- x_6].
-Let x_7 = m_2[a_6].
+Let a_5 = shift_sint32(a_1, 3).
+Let x_3 = Msint32_0[a_5].
+Let a_6 = shiftfield_F1_S_content(b).
+Let x_4 = Msint32_0[shift_sint32(a_6, 0)].
+Let a_7 = shift_sint32(a_6, 2).
+Let x_5 = Msint32_0[a_7].
+Let m = Msint32_0[a_2 <- x + x_4].
+Let x_6 = m[shift_sint32(a_6, 1)].
+Let m_1 = m[a_3 <- x_1 + x_6].
+Let x_7 = m_1[a_7].
+Let x_8 = x_2 + x_7.
+Let m_2 = m_1[a_4 <- x_8].
+Let x_9 = m_2[shift_sint32(a_6, 3)].
Assume {
- Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
- is_sint32(Msint32_0[shift_sint32(a_1, 3)]) /\
- is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_3) /\
- is_sint32(Msint32_0[a_6]) /\ is_sint32(x_4) /\ is_sint32(x_5) /\
- is_sint32(x_6) /\ is_sint32(x_7) /\
- is_sint32(m_2[shift_sint32(a_5, 3)]).
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_4) /\
+ is_sint32(x_5) /\ is_sint32(x_6) /\ is_sint32(x_7) /\ is_sint32(x_8) /\
+ is_sint32(x_9) /\ is_sint32(m_2[a_5 <- x_3 + x_9][a_7]).
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
- (* Goal *)
- When: b != a.
(* Pre-condition *)
Have: P_pointed(a, b).
}
@@ -136,7 +85,7 @@ Prove: x_7 = x_5.
------------------------------------------------------------
-Goal Assertion (file array.c, line 24):
+Goal Post-condition (file array.c, line 15) in 'add_first4':
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
index 6162ad43a5a..8111c5b2622 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
@@ -4,21 +4,17 @@
[wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
[wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[wp] 6 goals scheduled
+[wp] 4 goals scheduled
[wp] [Valid] region_add_first4_ensures (Alt-Ergo) (Cached)
[wp] [Valid] region_add_first4_ensures_2 (Qed)
[wp] [Valid] region_add_first4_ensures_3 (Alt-Ergo) (Cached)
[wp] [Valid] region_add_first4_ensures_4 (Qed)
-[wp] [Valid] region_add_first4_assert (Alt-Ergo) (Cached)
-[wp] [Valid] region_add_first4_assert_2 (Qed)
-[wp] Proved goals: 8 / 8
+[wp] Proved goals: 6 / 6
Terminating: 1
Unreachable: 1
- Qed: 3
- Alt-Ergo: 3
+ Qed: 2
+ Alt-Ergo: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- add_first4 3 3 6 100%
+ add_first4 2 2 4 100%
------------------------------------------------------------
--
GitLab