From d4d23ab7daa8cb4d6027561665e8eb255365bd5c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 22 Jan 2020 09:21:02 +0100
Subject: [PATCH] [wp] frame conditions for compounds
# Conflicts:
# src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
# src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
---
src/plugins/wp/MemVar.ml | 38 ++++++++++++++-----
.../wp/tests/wp_acsl/oracle/equal.res.oracle | 31 ++++++++++-----
.../oracle/reference_and_struct.res.oracle | 2 +-
.../tests/wp_plugin/oracle/initarr.res.oracle | 6 +++
.../oracle/array_initialized.0.res.oracle | 2 +-
.../tests/wp_typed/oracle/frame.0.res.oracle | 6 ++-
.../tests/wp_typed/oracle/frame.1.res.oracle | 6 ++-
.../wp_typed/oracle_qualif/frame.res.oracle | 8 ++--
8 files changed, 71 insertions(+), 28 deletions(-)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 58845184bfd..81b87712410 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -913,6 +913,35 @@ struct
pretty l Vset.pp_bound a Vset.pp_bound b
end
+ (* -------------------------------------------------------------------------- *)
+ (* --- Framing --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let rec forall_pointers phi v t =
+ match Cil.unrollType t with
+ | TInt _ | TFloat _ | TVoid _ | TEnum _ | TNamed _ | TBuiltin_va_list _
+ -> F.p_true
+ | TPtr _ | TFun _ -> phi v
+ | TComp({ cfields },_,_) ->
+ F.p_all
+ (fun fd -> forall_pointers phi (e_getfield v (Cfield fd)) fd.ftype)
+ cfields
+ | TArray(elt,_,_,_) ->
+ let k = Lang.freshvar Qed.Logic.Int in
+ F.p_forall [k] (forall_pointers phi (e_get v (e_var k)) elt)
+
+ let frame sigma =
+ let hs = ref [] in
+ SIGMA.iter
+ (fun x chunk ->
+ if (x.vglob || x.vformal) then
+ let t = VAR.typ_of_chunk x in
+ let v = e_var chunk in
+ let h = forall_pointers (M.global sigma.mem) v t in
+ if not (F.eqp h F.p_true) then hs := h :: !hs
+ ) sigma.vars ;
+ !hs @ M.frame sigma.mem
+
(* -------------------------------------------------------------------------- *)
(* --- Scope --- *)
(* -------------------------------------------------------------------------- *)
@@ -926,15 +955,6 @@ struct
| ByRef | InContext | InArray | NotUsed -> false
| ByValue | ByShift | ByAddr -> true
- let frame sigma =
- let pool = ref [] in
- SIGMA.iter
- (fun x p ->
- if (x.vglob || x.vformal) && Cil.isPointerType (VAR.typ_of_chunk x)
- then pool := M.global sigma.mem (e_var p) :: !pool
- ) sigma.vars ;
- !pool @ M.frame sigma.mem
-
let alloc sigma xs =
let xm = List.filter is_mem xs in
let mem = M.alloc sigma.mem xm in
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
index a5e1f5ba07c..3b3cb513ee8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
@@ -46,16 +46,19 @@ Prove: EqS2_St(st0_0, st1_0).
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/equal.i, line 47) in 'with_ptr_and_array_struct':
-Let a = q0_0.F4_Q_qs.
-Let a_1 = q1_0.F4_Q_qs.
-Let a_2 = q0_0.F4_Q_qt.
-Let a_3 = q1_0.F4_Q_qt.
+Let a = q0_0.F4_Q_qp.
+Let a_1 = q1_0.F4_Q_qp.
+Let a_2 = q0_0.F4_Q_qs.
+Let a_3 = q1_0.F4_Q_qs.
+Let a_4 = q0_0.F4_Q_qt.
+Let a_5 = q1_0.F4_Q_qt.
Assume {
- Type: IsS4_Q(q0_0) /\ IsS4_Q(q1_0) /\ IsArray1_sint32(a_2) /\
- IsArray1_sint32(a_3) /\ IsS1_S(a) /\ IsS1_S(a_1).
+ Type: IsS4_Q(q0_0) /\ IsS4_Q(q1_0) /\ IsArray1_sint32(a_4) /\
+ IsArray1_sint32(a_5) /\ IsS1_S(a_2) /\ IsS1_S(a_3).
(* Goal *)
- When: ((q1_0.F4_Q_qp) = (q0_0.F4_Q_qp)) /\ EqS1_S(a, a_1) /\
- EqArray1_int(2, a_2, a_3).
+ When: (a_1 = a) /\ EqS1_S(a_2, a_3) /\ EqArray1_int(2, a_4, a_5).
+ (* Heap *)
+ Have: (region(a.base) <= 0) /\ (region(a_1.base) <= 0).
}
Prove: EqS4_Q(q0_0, q1_0).
@@ -68,6 +71,9 @@ Goal Post-condition (file tests/wp_acsl/equal.i, line 40) in 'with_ptr_array':
Assume {
(* Goal *)
When: forall i : Z. ((0 <= i) -> ((i <= 4) -> (tp1_0[i] = tp0_0[i]))).
+ (* Heap *)
+ Have: (forall i : Z. region(tp0_0[i].base) <= 0) /\
+ (forall i : Z. region(tp1_0[i].base) <= 0).
}
Prove: EqArray1_pointer(5, tp0_0, tp1_0).
@@ -77,7 +83,14 @@ Prove: EqArray1_pointer(5, tp0_0, tp1_0).
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/equal.i, line 34) in 'with_ptr_struct':
-Assume { (* Goal *) When: (sp1_0.F3_Sp_p) = (sp0_0.F3_Sp_p). }
+Let a = sp0_0.F3_Sp_p.
+Let a_1 = sp1_0.F3_Sp_p.
+Assume {
+ (* Goal *)
+ When: a_1 = a.
+ (* Heap *)
+ Have: (region(a.base) <= 0) /\ (region(a_1.base) <= 0).
+}
Prove: EqS3_Sp(sp0_0, sp1_0).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index e889fe4a673..c13e28c419a 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -205,7 +205,7 @@ Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Heap *)
- Have: linked(Malloc_0).
+ Have: linked(Malloc_0) /\ (forall i_1 : Z. region(tps_0[i_1].base) <= 0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, 10).
(* Call 'reset_5' *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle
index 3547749f04d..fc2ec450b36 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/initarr.res.oracle
@@ -26,6 +26,9 @@ Assume {
Init: (a.F1_f) = global(G_e_22).
(* Initializer *)
Init: (a.F1_g) = global(G_f_23).
+ (* Heap *)
+ Have: forall i_1 : Z. let a_4 = A[i_1] in (region(a_4.F1_f.base) <= 0) /\
+ (region(a_4.F1_g.base) <= 0).
(* Pre-condition *)
Have: (0 <= i) /\ (i <= 2).
}
@@ -46,6 +49,9 @@ Assume {
Init: (A[1].F1_f) = a_1.
(* Initializer *)
Init: (A[2].F1_f) = a.
+ (* Heap *)
+ Have: forall i_1 : Z. let a_4 = A[i_1] in (region(a_4.F1_f.base) <= 0) /\
+ (region(a_4.F1_g.base) <= 0).
(* Pre-condition *)
Have: (0 <= i) /\ (i <= 2).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
index d9091a09166..8599291ad47 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
@@ -255,7 +255,7 @@ Assume {
Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 499) ->
(p[i_1] = global(G_p0_28)))).
(* Heap *)
- Have: linked(Malloc_0).
+ Have: linked(Malloc_0) /\ (forall i_1 : Z. region(p[i_1].base) <= 0).
}
Prove: valid_rw(Malloc_0, p[i], 1).
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 f35d1e700da..ded97da9829 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
@@ -11,7 +11,8 @@ Goal Assertion 'SEP' (file tests/wp_typed/frame.i, line 10):
Assume {
Type: is_sint32(k).
(* Heap *)
- Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+ Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+ (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
}
@@ -26,7 +27,8 @@ Let x = Mint_0[a <- 4][a_1].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
(* Heap *)
- Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+ Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+ (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
(* Initializer *)
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 1549f0eda46..5a4bc40797c 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
@@ -11,7 +11,8 @@ Goal Assertion 'SEP' (file tests/wp_typed/frame.i, line 10):
Assume {
Type: is_sint32(k).
(* Heap *)
- Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+ Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+ (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
}
@@ -26,7 +27,8 @@ Let x = Mint_0[a <- 4][a_1].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
(* Heap *)
- Have: (region(Q.base) <= 0) /\ linked(Malloc_0).
+ Have: (region(Q.base) <= 0) /\ linked(Malloc_0) /\
+ (forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
(* Initializer *)
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 26df95322b6..aa5a8e8b26e 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
@@ -4,12 +4,12 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_compound_assert_SEP : Unsuccess
+[wp] [Alt-Ergo 2.0.0] Goal typed_compound_assert_SEP : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_compound_assert_RES : Valid
-[wp] Proved goals: 1 / 2
+[wp] Proved goals: 2 / 2
Qed: 0
- Alt-Ergo 2.0.0: 1 (unsuccess: 1)
+ Alt-Ergo 2.0.0: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- compound - 1 2 50.0%
+ compound - 2 2 100%
------------------------------------------------------------
--
GitLab