From f948e96ed0c6216d18ea12b66fd7736bbcffb107 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 29 May 2020 16:19:27 +0200
Subject: [PATCH] [wp] Tests that chunk constraints are added and usable
---
.../wp/tests/wp_acsl/chunk_typing_usable.i | 47 ++
.../tests/wp_acsl/chunk_typing_usable.script | 37 ++
.../oracle/chunk_typing_usable.res.oracle | 501 ++++++++++++++++++
.../chunk_typing_usable.res.oracle | 24 +
4 files changed, 609 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
create mode 100644 src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
new file mode 100644
index 00000000000..b06076ab167
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
@@ -0,0 +1,47 @@
+/* run.config
+ OPT: -wp-gen -wp-rte -wp-prover why3 -wp-msg-key print-generated
+*/
+/* run.config_qualif
+ OPT: -wp-rte -wp-coq-script tests/wp_acsl/chunk_typing_usable.script -wp-prover alt-ergo,native:coq
+*/
+
+/*@
+ axiomatic Occ{
+ logic integer occ{L}(int value, int* p, integer f, integer t)
+ reads p[f .. t-1];
+
+ axiom empty{L}:
+ \forall int v, int* p, integer f, t;
+ f >= t ==> occ{L}(v, p, f, t) == 0;
+
+ axiom is{L}:
+ \forall int v, int* p, integer f, t;
+ (f < t && p[t-1] == v) ==> occ(v,p,f,t) == 1+occ(v,p,f,t-1);
+
+ axiom isnt{L}:
+ \forall int v, int* p, integer f, t;
+ (f < t && p[t-1] != v) ==> occ(v,p,f,t) == occ(v,p,f,t-1);
+ }
+*/
+
+/*@
+ requires b < e <= 1000 ;
+ ensures \forall int v ; v != a[e-1] ==> occ(v,a,b,e) == occ(v,a,b,e-1);
+*/
+void usable_axiom(int* a, unsigned b, unsigned e){
+
+}
+
+/*@
+ lemma provable_lemma:
+ \forall int v, int* p, integer f, s, t;
+ f <= s <= t ==> occ(v,p,f,t) == occ(v,p,f,s) + occ(v,p,s,t) ;
+*/
+
+/*@
+ requires b < s <= e;
+ ensures \forall int v ; occ(v,a,b,e) == occ(v,a,b,s) + occ(v,a,s,e) ;
+*/
+void usable_lemma(int* a, unsigned b, unsigned s, unsigned e){
+
+}
diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script
new file mode 100644
index 00000000000..7e86db5b5e7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script
@@ -0,0 +1,37 @@
+(* Generated by Frama-C WP *)
+
+Goal typed_lemma_provable_lemma.
+Hint property,provable_lemma.
+Proof.
+ Import Compound.
+
+ Ltac norm := repeat(match goal with
+ | [ _ : _ |- context [ (?i + 1 - 1)%Z ]] => replace (i + 1 - 1)%Z with i by omega
+ | [ _ : _ |- context [ (0 + ?i)%Z ]] => replace (0 + i)%Z with i by omega
+ | [ _ : _ |- context [ (?i + 0)%Z ]] => replace (i + 0)%Z with i by omega
+ end).
+ intros e from cut to.
+ generalize dependent cut.
+ induction to using Z_induction with (m := from) ; intros cut mem page Hct Hfc Hm He.
+ * repeat(rewrite A_Occ.Q_empty ; auto ; try omega).
+ * assert(EqNeq: { mem.[ (shift_sint32 page to) ] = e } + { mem.[ (shift_sint32 page to) ] <> e }) by
+ repeat(decide equality).
+ assert(Cut: (cut < to + 1 \/ cut = to + 1)%Z ) by omega ; inversion Cut as [ Inf | Eq ].
+ + inversion_clear EqNeq as [ Eq | Neq ].
+ - rewrite <- Eq.
+ replace (mem .[ shift_sint32 page to]) with (mem .[ shift_sint32 page (to + 1 - 1)]) by (norm ; auto).
+ rewrite <- A_Occ.Q_is with (i := (to+1)%Z) ;
+ [ rewrite <- A_Occ.Q_is with (i := (to+1)%Z) | | | | |] ;
+ norm ; try rewrite Eq ; auto ; try omega.
+ assert(Simpl: forall x y z : Z, (x + y = z)%Z -> (1 + x + y = 1 + z)%Z) by (intros ; omega).
+ apply Simpl.
+ apply IHto ; auto ; omega.
+ - rewrite <- A_Occ.Q_isnt with (i := (to+1)%Z) ;
+ [ rewrite <- A_Occ.Q_isnt with (i := (to+1)%Z) | | | | |] ;
+ norm ; auto ; try omega.
+ apply IHto ; auto ; omega.
+ + rewrite Eq.
+ rewrite A_Occ.Q_empty ; auto ; try omega.
+Qed.
+
+
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
new file mode 100644
index 00000000000..f066a94e1eb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -0,0 +1,501 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function usable_axiom
+[rte] annotating function usable_lemma
+[wp] 3 goals scheduled
+---------------------------------------------
+--- Context 'typed_usable_lemma' Cluster 'Chunk'
+---------------------------------------------
+theory Chunk
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use frama_c_wp.cint.Cint *)
+
+ predicate is_sint32_chunk (m:addr -> int) =
+ forall a:addr. is_sint32 (get m a)
+end
+---------------------------------------------
+--- Context 'typed_usable_lemma' Cluster 'Compound'
+---------------------------------------------
+theory Compound
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ function shift_sint32 (p:addr) (k:int) : addr = shift p k
+end
+---------------------------------------------
+--- Context 'typed_usable_lemma' Cluster 'A_Occ'
+---------------------------------------------
+theory A_Occ
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ function L_occ (addr -> int) int addr int int : int
+
+ (* use Chunk *)
+
+ Q_empty :
+ forall mint:addr -> int, v:int, p:addr, f:int, t:int.
+ t <= f -> is_sint32_chunk mint -> is_sint32 v -> L_occ mint v p f t = 0
+
+ (* use Compound *)
+
+ Q_is :
+ forall mint:addr -> int, v:int, p:addr, f:int, t:int.
+ let x = (- 1) + t in
+ let x1 = get mint (shift_sint32 p x) in
+ x1 = v ->
+ f < t ->
+ is_sint32_chunk mint ->
+ is_sint32 v ->
+ is_sint32 x1 -> (1 + L_occ mint v p f x) = L_occ mint v p f t
+
+ Q_isnt :
+ forall mint:addr -> int, v:int, p:addr, f:int, t:int.
+ let x = (- 1) + t in
+ let x1 = get mint (shift_sint32 p x) in
+ not x1 = v ->
+ f < t ->
+ is_sint32_chunk mint ->
+ is_sint32 v -> is_sint32 x1 -> L_occ mint v p f x = L_occ mint v p f t
+end
+---------------------------------------------
+--- Context 'typed_usable_lemma' Cluster 'Axiomatic1'
+---------------------------------------------
+theory Axiomatic1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use Chunk *)
+
+ (* use A_Occ *)
+
+ lemma Q_provable_lemma :
+ forall mint:addr -> int, v:int, p:addr, f:int, s:int, t:int.
+ f <= s ->
+ s <= t ->
+ is_sint32_chunk mint ->
+ is_sint32 v ->
+ (L_occ mint v p f s + L_occ mint v p s t) = L_occ mint v p f t
+end
+[wp:print-generated]
+ theory WP
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use Axiomatic1 *)
+
+ goal wp_goal :
+ forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int.
+ i3 <= i1 ->
+ i < i3 ->
+ region (base a) <= 0 ->
+ is_sint32_chunk t ->
+ is_uint32 i3 ->
+ is_uint32 i1 ->
+ is_uint32 i ->
+ is_sint32 i2 ->
+ (L_occ t i2 a i i3 + L_occ t i2 a i3 i1) = L_occ t i2 a i i1
+ end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'Chunk'
+---------------------------------------------
+theory Chunk1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use frama_c_wp.memory.Memory1 *)
+
+ (* use frama_c_wp.cint.Cint1 *)
+
+ predicate is_sint32_chunk1 (m:addr1 -> int) =
+ forall a:addr1. is_sint321 (get1 m a)
+end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'Compound'
+---------------------------------------------
+theory Compound1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use frama_c_wp.memory.Memory1 *)
+
+ function shift_sint321 (p:addr1) (k:int) : addr1 = shift1 p k
+end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'A_Occ'
+---------------------------------------------
+theory A_Occ1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use frama_c_wp.memory.Memory1 *)
+
+ function L_occ1 (addr1 -> int) int addr1 int int : int
+
+ (* use Chunk1 *)
+
+ Q_empty1 :
+ forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
+ t <=' f ->
+ is_sint32_chunk1 mint -> is_sint321 v -> L_occ1 mint v p f t = 0
+
+ (* use Compound1 *)
+
+ Q_is1 :
+ forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
+ let x = (- 1) +' t in
+ let x1 = get1 mint (shift_sint321 p x) in
+ x1 = v ->
+ f <' t ->
+ is_sint32_chunk1 mint ->
+ is_sint321 v ->
+ is_sint321 x1 -> (1 +' L_occ1 mint v p f x) = L_occ1 mint v p f t
+
+ Q_isnt1 :
+ forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
+ let x = (- 1) +' t in
+ let x1 = get1 mint (shift_sint321 p x) in
+ not x1 = v ->
+ f <' t ->
+ is_sint32_chunk1 mint ->
+ is_sint321 v ->
+ is_sint321 x1 -> L_occ1 mint v p f x = L_occ1 mint v p f t
+end
+---------------------------------------------
+--- Context 'typed_usable_axiom' Cluster 'Axiomatic1'
+---------------------------------------------
+theory Axiomatic11
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use frama_c_wp.memory.Memory1 *)
+
+ (* use Chunk1 *)
+
+ (* use A_Occ1 *)
+
+ lemma Q_provable_lemma1 :
+ forall mint:addr1 -> int, v:int, p:addr1, f:int, s:int, t:int.
+ f <=' s ->
+ s <=' t ->
+ is_sint32_chunk1 mint ->
+ is_sint321 v ->
+ (L_occ1 mint v p f s +' L_occ1 mint v p s t) = L_occ1 mint v p f t
+end
+[wp:print-generated]
+ theory WP1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use Axiomatic11 *)
+
+ goal wp_goal :
+ forall t:addr1 -> int, a:addr1, i:int, i1:int, i2:int.
+ let x = (- 1) +' i1 in
+ not get1 t (shift_sint321 a x) = i2 ->
+ i <' i1 ->
+ region1 (base1 a) <=' 0 ->
+ i1 <=' 1000 ->
+ is_sint32_chunk1 t ->
+ is_uint321 i1 ->
+ is_uint321 i -> is_sint321 i2 -> L_occ1 t i2 a i x = L_occ1 t i2 a i i1
+ end
+---------------------------------------------
+--- Context 'typed' Cluster 'Chunk'
+---------------------------------------------
+theory Chunk2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool2 *)
+
+ (* use int.Int2 *)
+
+ (* use int.ComputerDivision2 *)
+
+ (* use real.RealInfix2 *)
+
+ (* use frama_c_wp.qed.Qed2 *)
+
+ (* use map.Map2 *)
+
+ (* use frama_c_wp.memory.Memory2 *)
+
+ (* use frama_c_wp.cint.Cint2 *)
+
+ predicate is_sint32_chunk2 (m:addr2 -> int) =
+ forall a:addr2. is_sint322 (get2 m a)
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'Compound'
+---------------------------------------------
+theory Compound2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool2 *)
+
+ (* use int.Int2 *)
+
+ (* use int.ComputerDivision2 *)
+
+ (* use real.RealInfix2 *)
+
+ (* use frama_c_wp.qed.Qed2 *)
+
+ (* use map.Map2 *)
+
+ (* use frama_c_wp.memory.Memory2 *)
+
+ function shift_sint322 (p:addr2) (k:int) : addr2 = shift2 p k
+end
+---------------------------------------------
+--- Context 'typed' Cluster 'A_Occ'
+---------------------------------------------
+theory A_Occ2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool2 *)
+
+ (* use int.Int2 *)
+
+ (* use int.ComputerDivision2 *)
+
+ (* use real.RealInfix2 *)
+
+ (* use frama_c_wp.qed.Qed2 *)
+
+ (* use map.Map2 *)
+
+ (* use frama_c_wp.memory.Memory2 *)
+
+ function L_occ2 (addr2 -> int) int addr2 int int : int
+
+ (* use Chunk2 *)
+
+ Q_empty2 :
+ forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
+ t <='' f ->
+ is_sint32_chunk2 mint -> is_sint322 v -> L_occ2 mint v p f t = 0
+
+ (* use Compound2 *)
+
+ Q_is2 :
+ forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
+ let x = (- 1) +'' t in
+ let x1 = get2 mint (shift_sint322 p x) in
+ x1 = v ->
+ f <'' t ->
+ is_sint32_chunk2 mint ->
+ is_sint322 v ->
+ is_sint322 x1 -> (1 +'' L_occ2 mint v p f x) = L_occ2 mint v p f t
+
+ Q_isnt2 :
+ forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
+ let x = (- 1) +'' t in
+ let x1 = get2 mint (shift_sint322 p x) in
+ not x1 = v ->
+ f <'' t ->
+ is_sint32_chunk2 mint ->
+ is_sint322 v ->
+ is_sint322 x1 -> L_occ2 mint v p f x = L_occ2 mint v p f t
+end
+[wp:print-generated]
+ theory WP2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool2 *)
+
+ (* use int.Int2 *)
+
+ (* use int.ComputerDivision2 *)
+
+ (* use real.RealInfix2 *)
+
+ (* use frama_c_wp.qed.Qed2 *)
+
+ (* use map.Map2 *)
+
+ (* use frama_c_wp.memory.Memory2 *)
+
+ (* use Chunk2 *)
+
+ (* use A_Occ2 *)
+
+ goal wp_goal :
+ forall t:addr2 -> int, i:int, a:addr2, i1:int, i2:int, i3:int.
+ i2 <='' i3 ->
+ i1 <='' i2 ->
+ is_sint32_chunk2 t ->
+ is_sint322 i ->
+ (L_occ2 t i a i1 i2 +'' L_occ2 t i a i2 i3) = L_occ2 t i a i1 i3
+ end
+[wp] 3 goals generated
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Lemma provable_lemma:
+Prove: (f_0<=s_0) -> (s_0<=t_0) -> (is_sint32_chunk Mint_0)
+ -> (is_sint32 v_0)
+ -> (((L_occ Mint_0 v_0 p_0 f_0 s_0)+(L_occ Mint_0 v_0 p_0 s_0 t_0))=
+ (L_occ Mint_0 v_0 p_0 f_0 t_0))
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function usable_axiom
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/chunk_typing_usable.i, line 29) in 'usable_axiom':
+Let x = e - 1.
+Assume {
+ Type: is_sint32_chunk(Mint_0) /\ is_uint32(b) /\ is_uint32(e).
+ (* Heap *)
+ Type: region(a.base) <= 0.
+ (* Goal *)
+ When: (Mint_0[shift_sint32(a, x)] != i) /\ is_sint32(i).
+ (* Pre-condition *)
+ Have: (b < e) /\ (e <= 1000).
+}
+Prove: L_occ(Mint_0, i, a, b, x) = L_occ(Mint_0, i, a, b, e).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function usable_lemma
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/chunk_typing_usable.i, line 43) in 'usable_lemma':
+Assume {
+ Type: is_sint32_chunk(Mint_0) /\ is_uint32(b) /\ is_uint32(e) /\
+ is_uint32(s).
+ (* Heap *)
+ Type: region(a.base) <= 0.
+ (* Goal *)
+ When: is_sint32(i).
+ (* Pre-condition *)
+ Have: (b < s) /\ (s <= e).
+}
+Prove: (L_occ(Mint_0, i, a, b, s) + L_occ(Mint_0, i, a, s, e))
+ = L_occ(Mint_0, i, a, b, e).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
new file mode 100644
index 00000000000..c503421c8a9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
@@ -0,0 +1,24 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_acsl/chunk_typing_usable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function usable_axiom
+[rte] annotating function usable_lemma
+[wp] Warning: native support for coq is deprecated, use tip instead
+[wp] 3 goals scheduled
+[wp] [Coq] Goal typed_lemma_provable_lemma : Saved script
+[wp] [Coq (native)] Goal typed_lemma_provable_lemma : Valid
+[wp] [Alt-Ergo] Goal typed_usable_axiom_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_usable_lemma_ensures : Valid
+[wp] Proved goals: 3 / 3
+ Qed: 0
+ Coq (native): 1
+ Alt-Ergo: 2 (unsuccess: 1)
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - - 1 100%
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ usable_axiom - 1 1 100%
+ usable_lemma - 1 1 100%
+------------------------------------------------------------
--
GitLab