From b169eb33699c2a69ab42ff91fcf7d24d440cfb30 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 5 Oct 2021 13:33:07 +0200
Subject: [PATCH] [wp] Fix frame condition
---
.../wp/share/why3/frama_c_wp/memory.mlw | 2 +-
src/plugins/wp/tests/wp_typed/frame.i | 20 +++++++
.../tests/wp_typed/oracle/frame.0.res.oracle | 58 +++++++++++++++++++
.../tests/wp_typed/oracle/frame.1.res.oracle | 58 +++++++++++++++++++
.../wp_typed/oracle_qualif/frame.res.oracle | 12 +++-
.../init_t2_bis_v2_assigns_exit_part2.json | 4 +-
.../init_t2_bis_v2_assigns_normal_part2.json | 4 +-
.../init_t2_bis_v2_loop_assigns_part2.json | 4 +-
.../init_t2_bis_v2_loop_assigns_part3.json | 4 +-
9 files changed, 154 insertions(+), 12 deletions(-)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index c508fdae443..5489e17e49d 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -111,7 +111,7 @@ theory Memory
predicate linked (map int int)
predicate sconst (map addr int)
predicate framed (m : map addr addr) =
- forall p:addr [m[p]]. region(m[p].base) <= 0
+ forall p:addr [m[p]]. region(p.base) <= 0 -> region(m[p].base) <= 0
(* Properties *)
diff --git a/src/plugins/wp/tests/wp_typed/frame.i b/src/plugins/wp/tests/wp_typed/frame.i
index 8620e34f2bb..c68f9d167b3 100644
--- a/src/plugins/wp/tests/wp_typed/frame.i
+++ b/src/plugins/wp/tests/wp_typed/frame.i
@@ -14,3 +14,23 @@ void compound(int k) {
// NOTE:
// if we require \valid(comp[k].ptr) the goal is provable without frame conditions
// since it can not be aliased with 'm' at PRE, which is not (yet) valid.
+
+// For those two examples, we want the assert false to fail:
+// -> the frame condition must *not* introduce incoherence on initialization
+
+void local_region(void) {
+ char b[4] = {0};
+ char *x = b ;
+ char **in_memtyped = &x ; // be sure to put x in MemTyped
+ //@ assert A:X: \valid_read(x + (0..3));
+ //@ assert A:Y: \false ;
+}
+
+struct S { char b ; };
+
+void formal_region(struct S s) {
+ char *x = &s.b ;
+ char **in_memtyped = &x ; // be sure to put x in MemTyped
+ //@ assert A:X: \valid_read(x);
+ //@ assert A:Y: \false ;
+}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
index e433d6edd6b..64b8f12db9b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
@@ -38,3 +38,61 @@ Assume {
Prove: x = 1.
------------------------------------------------------------
+------------------------------------------------------------
+ Function formal_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 34):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+}
+Prove: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 35):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function local_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 25):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+}
+Prove: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 26):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
index f958319c4c3..d1ace9a6829 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
@@ -38,3 +38,61 @@ Assume {
Prove: x = 1.
------------------------------------------------------------
+------------------------------------------------------------
+ Function formal_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 34):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+}
+Prove: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 35):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shiftfield_F2_S_b(global(P_s_36)).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function local_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 25):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+}
+Prove: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 26):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+ (* Heap *)
+ Type: framed(Mptr_0) /\ linked(Malloc_0).
+ (* Initializer *)
+ Init: a = shift_sint8(global(L_b_31), 0).
+ (* Assertion 'A,X' *)
+ Have: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
index 96bb1c3037c..991ca84c401 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
@@ -2,13 +2,19 @@
[kernel] Parsing tests/wp_typed/frame.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_compound_assert_SEP : Unsuccess
[wp] [Alt-Ergo] Goal typed_compound_assert_RES : Valid
-[wp] Proved goals: 1 / 2
+[wp] [Alt-Ergo] Goal typed_local_region_assert_A_X : Valid
+[wp] [Alt-Ergo] Goal typed_local_region_assert_A_Y : Unsuccess
+[wp] [Alt-Ergo] Goal typed_formal_region_assert_A_X : Valid
+[wp] [Alt-Ergo] Goal typed_formal_region_assert_A_Y : Unsuccess
+[wp] Proved goals: 3 / 6
Qed: 0
- Alt-Ergo: 1 (unsuccess: 1)
+ Alt-Ergo: 3 (unsuccess: 3)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
compound - 1 2 50.0%
+ local_region - 1 2 50.0%
+ formal_region - 1 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index d6b2be2c19d..a187150cc64 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0109,
+ "verdict": "valid", "time": 0.0088,
"steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0114,
+ "verdict": "valid", "time": 0.0116,
"steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index d6b2be2c19d..a187150cc64 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0109,
+ "verdict": "valid", "time": 0.0088,
"steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0114,
+ "verdict": "valid", "time": 0.0116,
"steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index df90f71b8c9..baf7c5bf62b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0151,
+ "verdict": "valid", "time": 0.0279,
"steps": 41 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0147,
+ "verdict": "valid", "time": 0.021,
"steps": 41 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index ab6c0d166bb..cae89d2a942 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0115,
+ "verdict": "valid", "time": 0.009,
"steps": 29 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0117,
+ "verdict": "valid", "time": 0.0131,
"steps": 29 } ] } } ]
--
GitLab