From 435a1f7a75df27b52e9f18408383ae425590993d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 26 Jan 2022 10:16:14 +0100
Subject: [PATCH] [WP] fixes Qed types of \repeat
---
src/plugins/wp/Vlist.ml | 64 ++++++++++++++-----
.../wp/tests/wp_plugin/oracle/nth.res.oracle | 19 ++----
.../wp_plugin/oracle/sequence.res.oracle | 29 +--------
.../wp_plugin/oracle_qualif/nth.res.oracle | 18 +++---
.../oracle_qualif/sequence.0.res.oracle | 8 +--
.../oracle_qualif/sequence.1.res.oracle | 8 +--
6 files changed, 74 insertions(+), 72 deletions(-)
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index cd006e30368..76423f7fee8 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -147,7 +147,7 @@ let v_nil t = F.e_fun ~result:t f_nil []
let v_elt e = F.e_fun f_elt [e]
let v_concat es tau = F.e_fun f_concat es ~result:tau
let v_length l = F.e_fun f_length [l]
-let v_repeat s n = F.e_fun f_repeat [s;n]
+let v_repeat s n tau = F.e_fun f_repeat [s;n] ~result:tau
(* -------------------------------------------------------------------------- *)
(* --- Rewriters --- *)
@@ -167,7 +167,7 @@ let rewrite_length e =
F.e_if (F.e_leq e_zero n) (F.e_mul n (v_length u)) e_zero
| _ ->
(* NB. do not considers \Cons because they are removed *)
- raise Not_found
+ raise Not_found
let match_natural k =
match F.repr k with
@@ -228,7 +228,7 @@ let rewrite_repeat s n =
| L.Fun( repeat , [s0 ; n0] ) (* n0>=0 && n>=0 ==> ((s0 *^ n0) *^ n) == (s0 *^ (n0 * n)) *)
when (repeat == f_repeat) &&
(Cint.is_positive_or_null n) &&
- (Cint.is_positive_or_null n0) -> v_repeat s0 (F.e_mul n0 n)
+ (Cint.is_positive_or_null n0) -> v_repeat s0 (F.e_mul n0 n) (F.typeof s)
| _ -> raise Not_found
let rec leftmost a ms =
@@ -243,14 +243,14 @@ let rec leftmost a ms =
let u,us = leftmost u [] in
if F.decide (F.e_eq u b) then
(* u=b ==> ((u^us)*^n) ^ b ^ ms == u ^ (us^b)*^n) ^ ms *)
- Some (u, v_repeat (v_concat (us@[b]) (F.typeof a)) n :: ms)
+ Some (u, v_repeat (v_concat (us@[b]) (F.typeof a)) n (F.typeof a) :: ms)
else None
| _ -> None) with
| Some res -> res
| None ->
if F.decide (F.e_lt F.e_zero n) then
(* 0<n ==> (u*^n) ^ ms == u ^ (u*^(n-1)) ^ ms *)
- leftmost u (v_repeat u (F.e_sub n F.e_one) :: ms)
+ leftmost u (v_repeat u (F.e_sub n F.e_one) (F.typeof a) :: ms)
else a , ms
end
| _ -> a , ms
@@ -279,14 +279,14 @@ let rec rightmost ms a =
let us,u = rightmost [] u in
if F.decide (F.e_eq u b) then
(* u=b ==> (ms ^ b ^ (us^u)*^n) == ms ^ (b^us)*^n) ^ u *)
- Some (ms @ [ v_repeat (v_concat (b::us) (F.typeof a)) n ], u)
+ Some (ms @ [ v_repeat (v_concat (b::us) (F.typeof a)) n (F.typeof a)], u)
else None
| _ -> None) with
| Some res -> res
| None ->
if F.decide (F.e_lt F.e_zero n) then
(* 0<n ==> ms ^ (u*^n) == ms ^ (u*^(n-1)) ^ u *)
- rightmost (ms @ [v_repeat u (F.e_sub n F.e_one)]) u
+ rightmost (ms @ [v_repeat u (F.e_sub n F.e_one) (F.typeof a)]) u
else ms , a
end
| _ -> ms , a
@@ -330,7 +330,6 @@ let rightmost_eq a b =
else
raise Not_found
-
let rewrite_is_nil ~nil a =
let p_is_nil a = F.p_equal nil a in
match F.repr a with
@@ -344,7 +343,6 @@ let rewrite_is_nil ~nil a =
| _ ->
raise Not_found
-
(* Ensures xs to be a sub-sequence of ys, otherwise raise Not_found
In such a case, (concat xs = concat ys) <==> (forall r in result, r = nil) *)
let rec subsequence xs ys =
@@ -386,15 +384,15 @@ let repeat_eq a x n b y m =
(* x *^ n == y *^ n <==> ( x == y || n<=0 ) *)
F.p_or (F.p_leq n e_zero) (Lang.F.p_bool e_eq_x_y)
else if F.decide (e_eq (v_length x) (v_length y)) then
- (* \lenght(x)=\lenght(y) ==> ( x *^ n == y *^ m <==> ( m == n && x == y) || (x *^ n == [] && y *^ m == [] ) *)
+ (* \length(x)=\length(y) ==> ( x *^ n == y *^ m <==> ( m == n && x == y) || (x *^ n == [] && y *^ m == [] ) *)
let nil_a = v_nil (F.typeof a) in
let nil_b = v_nil (F.typeof b) in
F.p_or (F.p_and (F.p_bool e_eq_n_m) (Lang.F.p_bool e_eq_x_y))
(F.p_and (F.p_equal a nil_b) (F.p_equal nil_a b))
else raise Not_found
-let rewrite_eq a b =
- debug "Vlist.rewrite_eq: tries to rewrite %a@ = %a@.- left pattern: %a@.- right pattern: %a@."
+let rewrite_eq_sequence a b =
+ debug "Vlist.rewrite_eq_sequence: tries to rewrite %a@ = %a@.- left pattern: %a@.- right pattern: %a@."
Lang.F.pp_term a Lang.F.pp_term b
pp_pattern a pp_pattern b;
match F.repr a , F.repr b with
@@ -415,6 +413,40 @@ let rewrite_eq a b =
F.p_false
else raise Not_found
+let rewrite_eq_length a b =
+ match F.repr a , F.repr b with
+ | L.Fun(length_a,[_]), L.Fun(length_b,[_]) when length_a == f_length &&
+ length_b == f_length ->
+ (* N.B. cannot be simplified by the next patterns *)
+ raise Not_found
+ | _, L.Fun(length,[_]) when length == f_length &&
+ F.decide (e_lt a e_zero) ->
+ (* a < 0 ==> ( a=\length(b) <=> false ) *)
+ F.p_false
+ | L.Fun(length,[_]), _ when length == f_length &&
+ F.decide (e_lt b e_zero) ->
+ (* b < 0 ==> ( \length(a)<=b <=> false ) *)
+ F.p_false
+ | _ -> raise Not_found
+
+let rewrite_leq_length a b =
+ match F.repr a , F.repr b with
+ | L.Fun(length_a,[_]), L.Fun(length_b,[_]) when length_a == f_length &&
+ length_b == f_length ->
+ (* N.B. cannot be simplified by the next patterns *)
+ raise Not_found
+ | L.Fun(length,[_]), _ when length == f_length &&
+ F.decide (e_lt b e_zero) ->
+ (* b < 0 ==> ( \length(a)<=b <=> false ) *)
+ F.e_false
+ (* N.B. the next rule does not allow to split on the sign of \length(a) with TIP
+ | _, L.Fun(length,[_]) when length == f_length &&
+ F.decide (e_leq a e_zero) ->
+ (* a <= 0 ==> ( a<=\length(b) <=> true ) *)
+ F.e_true
+ *)
+ | _ -> raise Not_found
+
(* All Simplifications *)
@@ -425,9 +457,11 @@ let () =
F.set_builtin_2' f_cons rewrite_cons ;
F.set_builtin_2 f_repeat rewrite_repeat ;
F.set_builtin_1 f_length rewrite_length ;
- F.set_builtin_eqp f_concat rewrite_eq ;
- F.set_builtin_eqp f_repeat rewrite_eq ;
- F.set_builtin_eqp f_nil rewrite_eq ;
+ F.set_builtin_leq f_length rewrite_leq_length ;
+ F.set_builtin_eqp f_length rewrite_eq_length ;
+ F.set_builtin_eqp f_concat rewrite_eq_sequence ;
+ F.set_builtin_eqp f_repeat rewrite_eq_sequence ;
+ F.set_builtin_eqp f_nil rewrite_eq_sequence ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
index 765e683dcee..c93629cbb62 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
@@ -11,9 +11,7 @@ Prove: true
------------------------------------------------------------
Lemma left_shift_repeat1:
-Prove: let a_0 = (concat L_A L_B L_S) in
- (L_C=(concat (repeat a_0 L_N) L_A))=
- (L_C=(concat (repeat a_0 L_N) L_A))
+Prove: true
------------------------------------------------------------
@@ -23,9 +21,7 @@ Prove: true
------------------------------------------------------------
Lemma left_unfold_repeat1:
-Prove: let a_0 = (concat L_S L_A L_B) in
- (L_C=(concat L_A L_B (repeat a_0 2) L_A L_S))=
- (L_C=(concat L_A L_B (repeat a_0 2) L_A L_S))
+Prove: true
------------------------------------------------------------
@@ -50,9 +46,7 @@ Prove: true
------------------------------------------------------------
Lemma right_shift_repeat1:
-Prove: let a_0 = (concat L_S L_B L_A) in
- (L_C=(concat L_A (repeat a_0 L_N)))=
- (L_C=(concat L_A (repeat a_0 L_N)))
+Prove: true
------------------------------------------------------------
@@ -62,9 +56,7 @@ Prove: true
------------------------------------------------------------
Lemma right_unfold_repeat1:
-Prove: let a_0 = (concat L_B L_A L_S) in
- (L_C=(concat L_S L_A (repeat a_0 2) L_B L_A))=
- (L_C=(concat L_S L_A (repeat a_0 2) L_B L_A))
+Prove: true
------------------------------------------------------------
@@ -97,8 +89,7 @@ Prove: true
------------------------------------------------------------
Lemma repeat_repeated:
-Prove: let x_0 = ((land 1 L_N)*(land 2 L_M)) in
- (P_P (repeat L_S x_0)) <-> (P_P (repeat L_S x_0))
+Prove: true
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
index eaf6561ef18..fedcdb66fb6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
@@ -34,7 +34,7 @@ Assume {
(* Call 'f' *)
Have: L_call_obs(call_seq_3) = a_1.
}
-Prove: nth(a_1, 1 + length(a)) = z.
+Prove: nth(a_1, 1 + i) = z.
------------------------------------------------------------
@@ -181,30 +181,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition for 'g_called' 'ok,u1' in 'loops':
-Let a = ([ y ] *^ i).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x) /\ is_sint32(y) /\
- is_sint32(z).
- (* Heap *)
- Type: is_sint32(call_seq_0).
- (* Pre-condition *)
- Have: L_call_obs(call_seq_0) = nil.
- (* Pre-condition for 'g_called' *)
- Have: 0 < n.
- (* Call 'f' *)
- Have: L_call_obs(call_seq_1) = [ x ].
- (* Invariant 'ok,id_min' *)
- Have: 0 <= i.
- (* Invariant 'ok,id_max' *)
- Have: i <= n.
- (* Invariant 'ok,inv' *)
- Have: L_call_obs(call_seq_2) = [ x ] ^ a.
- (* Else *)
- Have: n <= i.
- (* Call 'f' *)
- Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ z ].
-}
-Prove: length(a) = i.
+Prove: true.
------------------------------------------------------------
@@ -240,7 +217,7 @@ Assume {
(* Call 'f' *)
Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ z ].
}
-Prove: length(a) = 0.
+Prove: i = 0.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
index 4916d86a523..d276407bd64 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
@@ -7,9 +7,9 @@
[wp] [Alt-Ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Valid
[wp] [Qed] Goal typed_check_lemma_constructor_elt_ok : Valid
[wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
-[wp] [Alt-Ergo] Goal typed_check_lemma_left_shift_repeat1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_left_shift_repeat1_ok : Valid
[wp] [Qed] Goal typed_check_lemma_left_shift_repeat2_ok : Valid
-[wp] [Alt-Ergo] Goal typed_check_lemma_left_unfold_repeat1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_left_unfold_repeat1_ok : Valid
[wp] [Qed] Goal typed_check_lemma_left_unfold_repeat2_ok : Valid
[wp] [Qed] Goal typed_check_lemma_negative_repeat_ok : Valid
[wp] [Qed] Goal typed_check_lemma_not_nil_elt_ok : Valid
@@ -22,18 +22,18 @@
[wp] [Qed] Goal typed_check_lemma_repeat2_ok : Valid
[wp] [Qed] Goal typed_check_lemma_repeat_nil_ok : Valid
[wp] [Qed] Goal typed_check_lemma_repeat_one_ok : Valid
-[wp] [Alt-Ergo] Goal typed_check_lemma_repeat_repeated_ok : Valid
-[wp] [Alt-Ergo] Goal typed_check_lemma_right_shift_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_repeat_repeated_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_right_shift_repeat1_ko : Valid
[wp] [Qed] Goal typed_check_lemma_right_shift_repeat2_ko : Valid
-[wp] [Alt-Ergo] Goal typed_check_lemma_right_unfold_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_right_unfold_repeat1_ko : Valid
[wp] [Qed] Goal typed_check_lemma_right_unfold_repeat2_ko : Valid
[wp] [Qed] Goal typed_check_lemma_subsequence1_ko : Valid
[wp] Proved goals: 25 / 26
- Qed: 17
- Alt-Ergo: 8 (unsuccess: 1)
+ Qed: 22
+ Alt-Ergo: 3 (unsuccess: 1)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Axiomatic Equality 9 4 13 100%
- Axiomatic MkRepeat 3 1 4 100%
+ Axiomatic Equality 13 - 13 100%
+ Axiomatic MkRepeat 4 - 4 100%
Axiomatic Nth 5 3 9 88.9%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
index 08751dc1962..7602867d078 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
@@ -38,16 +38,16 @@
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
+[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u2 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v1 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v2 : Valid
[wp] Proved goals: 39 / 39
- Qed: 25
- Alt-Ergo: 14
+ Qed: 26
+ Alt-Ergo: 13
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
no_calls 5 5 10 100%
sequence 8 2 10 100%
- loops 12 7 19 100%
+ loops 13 6 19 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index d2806020044..fb728b9fa94 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
@@ -33,16 +33,16 @@
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
+[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u2 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v1 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v2 : Valid
[wp] Proved goals: 34 / 34
- Qed: 22
- Alt-Ergo: 12
+ Qed: 23
+ Alt-Ergo: 11
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
no_calls 2 3 5 100%
sequence 8 2 10 100%
- loops 12 7 19 100%
+ loops 13 6 19 100%
------------------------------------------------------------
--
GitLab