From d83bfa3c7a28651af4918ce52268cecdcd3d1189 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 8 Jul 2021 09:50:46 +0200
Subject: [PATCH] [wp] fix collection of chunks for opaque structs
---
src/plugins/wp/MemTyped.ml | 2 +-
src/plugins/wp/tests/wp_acsl/opaque_struct.i | 18 +++
.../wp_acsl/oracle/opaque_struct.res.oracle | 109 +++++++++++++-----
.../oracle_qualif/opaque_struct.res.oracle | 39 +++++--
4 files changed, 127 insertions(+), 41 deletions(-)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index abf67a6cb7c..bb1369e9ffc 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -211,7 +211,7 @@ and footprint_comp { cfields } =
and all_value_chunks () =
let ints =
- List.fold_left (fun l i -> M_int i :: l) []
+ List.fold_left (fun l i -> m_int i :: l) []
[ Ctypes.CBool ;
SInt8 ; UInt8 ; SInt16 ; UInt16 ; SInt32 ; UInt32 ; SInt64 ; UInt64 ]
in
diff --git a/src/plugins/wp/tests/wp_acsl/opaque_struct.i b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
index c1e457182f2..40b9c7626f9 100644
--- a/src/plugins/wp/tests/wp_acsl/opaque_struct.i
+++ b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
@@ -1,3 +1,10 @@
+/* run.config
+ OPT: -wp-rte
+*/
+/* run.config_qualif
+ OPT: -wp-rte
+*/
+
struct S;
extern struct S S1;
@@ -63,3 +70,14 @@ void assigns_effect(int* p, float* q, char* c, struct S *a){
//@ check fail: *q == \at(*q, Pre);
//@ check succeed: *c == \at(*c, Pre);
}
+
+// regression on MemTyped chunk typing
+
+void use(struct S * s);
+
+//@ requires \valid(uc) && \valid_read(sc) ;
+void chunk_typing(unsigned char* uc, signed char* sc){
+ struct S* s ;
+ *uc = *sc ;
+ use(s) ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
index 519985dbf06..d75a5ef79bd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
@@ -1,7 +1,14 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
+[rte] annotating function assigned_via_pointer
+[rte] annotating function assigns
+[rte] annotating function assigns_effect
+[rte] annotating function chunk_typing
+[rte] annotating function initialized_assigns
+[rte] annotating function uninitialized_assigns
+[kernel:annot:missing-spec] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Neither code nor specification for function use, generating default assigns from the prototype
------------------------------------------------------------
Axiomatic 'test'
------------------------------------------------------------
@@ -24,38 +31,46 @@ Prove: 0<=BytesLength_of_S1_S
Function assigned_via_pointer
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 53):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 60):
+Let a = havoc(Mint_undef_0, Mint_0, p, Length_of_S1_S).
+Let a_1 = havoc(Mint_undef_3, Mint_3, p, Length_of_S1_S).
+Let a_2 = havoc(Mint_undef_5, Mint_5, p, Length_of_S1_S).
+Let a_3 = havoc(Mint_undef_7, Mint_7, p, Length_of_S1_S).
+Let a_4 = havoc(Mchar_undef_0, Mchar_0, p, Length_of_S1_S).
+Let a_5 = havoc(Mint_undef_2, Mint_2, p, Length_of_S1_S).
+Let a_6 = havoc(Mint_undef_4, Mint_4, p, Length_of_S1_S).
+Let a_7 = havoc(Mint_undef_6, Mint_6, p, Length_of_S1_S).
+Let a_8 = havoc(Mint_undef_1, Mint_1, p, Length_of_S1_S).
Assume {
+ Type: is_bool_chunk(Mint_0) /\ is_sint16_chunk(Mint_3) /\
+ is_sint32_chunk(Mint_5) /\ is_sint64_chunk(Mint_7) /\
+ is_sint8_chunk(Mchar_0) /\ is_uint16_chunk(Mint_2) /\
+ is_uint32_chunk(Mint_4) /\ is_uint64_chunk(Mint_6) /\
+ is_uint8_chunk(Mint_1) /\ is_bool_chunk(a) /\ is_sint16_chunk(a_1) /\
+ is_sint32_chunk(a_2) /\ is_sint64_chunk(a_3) /\ is_sint8_chunk(a_4) /\
+ is_uint16_chunk(a_5) /\ is_uint32_chunk(a_6) /\ is_uint64_chunk(a_7) /\
+ is_uint8_chunk(a_8).
(* Heap *)
Type: (region(p.base) <= 0) /\ framed(Mptr_0) /\ sconst(Mchar_0).
}
-Prove: EqS1_S(Load_S1_S(p, havoc(Mchar_undef_0, Mchar_0, p, Length_of_S1_S),
- havoc(Mint_undef_0, Mint_0, p, Length_of_S1_S),
- havoc(Mint_undef_1, Mint_1, p, Length_of_S1_S),
- havoc(Mint_undef_2, Mint_2, p, Length_of_S1_S),
- havoc(Mint_undef_3, Mint_3, p, Length_of_S1_S),
- havoc(Mint_undef_4, Mint_4, p, Length_of_S1_S),
- havoc(Mint_undef_5, Mint_5, p, Length_of_S1_S),
- havoc(Mint_undef_6, Mint_6, p, Length_of_S1_S),
- havoc(Mint_undef_7, Mint_7, p, Length_of_S1_S),
- havoc(Mint_undef_8, Mint_8, p, Length_of_S1_S),
+Prove: EqS1_S(Load_S1_S(p, a_4, a, a_8, a_5, a_1, a_6, a_2, a_7, a_3,
havoc(Mf32_undef_0, Mf32_0, p, Length_of_S1_S),
havoc(Mf64_undef_0, Mf64_0, p, Length_of_S1_S),
havoc(Mptr_undef_0, Mptr_0, p, Length_of_S1_S)),
Load_S1_S(p, Mchar_0, Mint_0, Mint_1, Mint_2, Mint_3, Mint_4,
- Mint_5, Mint_6, Mint_7, Mint_8, Mf32_0, Mf64_0, Mptr_0)).
+ Mint_5, Mint_6, Mint_7, Mf32_0, Mf64_0, Mptr_0)).
------------------------------------------------------------
------------------------------------------------------------
Function assigns
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 17):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 24):
Prove: EqS1_S(S1_0, S1_1).
------------------------------------------------------------
-Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 18):
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 25):
Prove: true.
------------------------------------------------------------
@@ -63,22 +78,24 @@ Prove: true.
Function assigns_effect
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 62):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 69):
Let x = Mint_0[p].
-Let a_1 = havoc(Mint_undef_0, Mint_0, a, Length_of_S1_S)[p].
+Let a_1 = havoc(Mint_undef_0, Mint_0, a, Length_of_S1_S).
+Let a_2 = a_1[p].
Assume {
- Type: is_sint32(x) /\ is_sint32(a_1).
+ Type: is_sint32_chunk(Mint_0) /\ is_sint32(x) /\ is_sint32_chunk(a_1) /\
+ is_sint32(a_2).
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(p.base) <= 0).
(* Pre-condition *)
Have: separated(a, Length_of_S1_S, c, 1).
}
-Prove: a_1 = x.
+Prove: a_2 = x.
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 63):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 70):
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
@@ -91,24 +108,39 @@ Prove: of_f32(havoc(Mf32_undef_0, Mf32_0, a, Length_of_S1_S)[q])
------------------------------------------------------------
-Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 64):
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 71):
Let x = Mchar_0[c].
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, Length_of_S1_S)[c].
+Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, Length_of_S1_S).
+Let a_2 = a_1[c].
Assume {
- Type: is_sint8(x) /\ is_sint8(a_1).
+ Type: is_sint8_chunk(Mchar_0) /\ is_sint8(x) /\ is_sint8_chunk(a_1) /\
+ is_sint8(a_2).
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: separated(a, Length_of_S1_S, c, 1).
}
-Prove: a_1 = x.
+Prove: a_2 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function chunk_typing
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/opaque_struct.i, line 81):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/opaque_struct.i, line 81):
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function initialized_assigns
------------------------------------------------------------
-Goal Check 'fails' (file tests/wp_acsl/opaque_struct.i, line 31):
+Goal Check 'fails' (file tests/wp_acsl/opaque_struct.i, line 38):
Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
@@ -124,7 +156,7 @@ Prove: IsInit_S1_S(p, a).
------------------------------------------------------------
-Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 32):
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 39):
Let x = p.base.
Assume {
(* Heap *)
@@ -139,7 +171,7 @@ Prove: 0 <= (BytesLength_of_S1_S * (Malloc_0[x] / Length_of_S1_S)).
Function uninitialized_assigns
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 47):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 54):
Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
@@ -153,7 +185,7 @@ Prove: !IsInit_S1_S(p, a).
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 48):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 55):
Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
@@ -166,17 +198,17 @@ Assume {
Prove: IsInit_S1_S(p, a).
------------------------------------------------------------
-[wp] tests/wp_acsl/opaque_struct.i:24: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:31: Warning:
Memory model hypotheses for function 'g':
/*@ behavior wp_typed:
requires \separated(p, &S1, &S2, &p); */
void g(void);
-[wp] tests/wp_acsl/opaque_struct.i:57: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:64: Warning:
Memory model hypotheses for function 'assign':
/*@ behavior wp_typed:
requires \separated(a, &S1, &S2); */
void assign(struct S *a);
-[wp] tests/wp_acsl/opaque_struct.i:60: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:67: Warning:
Memory model hypotheses for function 'assigns_effect':
/*@
behavior wp_typed:
@@ -186,3 +218,16 @@ Prove: IsInit_S1_S(p, a).
requires \separated(q, &S1, &S2);
*/
void assigns_effect(int *p_0, float *q, char *c, struct S *a);
+[wp] tests/wp_acsl/opaque_struct.i:76: Warning:
+ Memory model hypotheses for function 'use':
+ /*@ behavior wp_typed:
+ requires \separated(s, &S1, &S2); */
+ void use(struct S *s);
+[wp] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Memory model hypotheses for function 'chunk_typing':
+ /*@
+ behavior wp_typed:
+ requires \separated(sc, &S1, &S2);
+ requires \separated(uc, &S1, &S2);
+ */
+ void chunk_typing(unsigned char *uc, signed char *sc);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
index ffca345397b..de7c9982ada 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
@@ -1,8 +1,15 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 13 goals scheduled
+[rte] annotating function assigned_via_pointer
+[rte] annotating function assigns
+[rte] annotating function assigns_effect
+[rte] annotating function chunk_typing
+[rte] annotating function initialized_assigns
+[rte] annotating function uninitialized_assigns
+[kernel:annot:missing-spec] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Neither code nor specification for function use, generating default assigns from the prototype
+[wp] 15 goals scheduled
[wp] [Alt-Ergo] Goal typed_check_lemma_fail : Unsuccess
[wp] [Qed] Goal typed_check_lemma_succeed_L1 : Valid
[wp] [Alt-Ergo] Goal typed_check_lemma_succeed_L2 : Valid
@@ -16,8 +23,10 @@
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_succeed : Valid
-[wp] Proved goals: 5 / 13
- Qed: 2
+[wp] [Qed] Goal typed_chunk_typing_assert_rte_mem_access : Valid
+[wp] [Qed] Goal typed_chunk_typing_assert_rte_mem_access_2 : Valid
+[wp] Proved goals: 7 / 15
+ Qed: 4
Alt-Ergo: 3 (unsuccess: 8)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
@@ -29,18 +38,19 @@
uninitialized_assigns - - 2 0.0%
assigned_via_pointer - - 1 0.0%
assigns_effect - 1 3 33.3%
+ chunk_typing 2 - 2 100%
------------------------------------------------------------
-[wp] tests/wp_acsl/opaque_struct.i:24: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:31: Warning:
Memory model hypotheses for function 'g':
/*@ behavior wp_typed:
requires \separated(p, &S1, &S2, &p); */
void g(void);
-[wp] tests/wp_acsl/opaque_struct.i:57: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:64: Warning:
Memory model hypotheses for function 'assign':
/*@ behavior wp_typed:
requires \separated(a, &S1, &S2); */
void assign(struct S *a);
-[wp] tests/wp_acsl/opaque_struct.i:60: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:67: Warning:
Memory model hypotheses for function 'assigns_effect':
/*@
behavior wp_typed:
@@ -50,3 +60,16 @@
requires \separated(q, &S1, &S2);
*/
void assigns_effect(int *p_0, float *q, char *c, struct S *a);
+[wp] tests/wp_acsl/opaque_struct.i:76: Warning:
+ Memory model hypotheses for function 'use':
+ /*@ behavior wp_typed:
+ requires \separated(s, &S1, &S2); */
+ void use(struct S *s);
+[wp] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Memory model hypotheses for function 'chunk_typing':
+ /*@
+ behavior wp_typed:
+ requires \separated(sc, &S1, &S2);
+ requires \separated(uc, &S1, &S2);
+ */
+ void chunk_typing(unsigned char *uc, signed char *sc);
--
GitLab