[wp] Tests that chunk constraints are added and usable

src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i

+/* 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){
+
+}

src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script

+(* 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.
+
+

src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle

+# 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).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle

+# 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%
+------------------------------------------------------------