Commit 43120c5d authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] restore previous behaviour

parent 4d23ee4d
......@@ -370,11 +370,6 @@ sig
val lc_term : term -> lc_term
val lc_repr : lc_term -> term
[@@deprecated "Might be unsafe in presence of binders"]
(** Returns the list of head binders *)
val binders : term -> binder list
[@@deprecated "Useless function"]
(** {3 Recursion Scheme} *)
......@@ -385,10 +380,7 @@ sig
val f_iter : (int -> term -> unit) -> int -> term -> unit
val lc_map : (term -> term) -> term -> term
[@@deprecated "Might be unsafe in presence of binders"]
val lc_iter : (term -> unit) -> term -> unit
[@@deprecated "Might be unsafe in presence of binders"]
(** {3 Partial Typing} *)
......
......@@ -1984,9 +1984,9 @@ struct
Never re-compute simplifications, only renormalize with
respect to hash-consing.
*)
let lc_alpha f e =
match e.repr with
| Kint _ | Kreal _ | Fvar _ | Bvar _ | True | False -> e
let lc_alpha f e0 =
match e0.repr with
| Kint _ | Kreal _ | Fvar _ | Bvar _ | True | False -> e0
| Not e -> c_not (f e)
| Add xs -> c_add (List.map f xs)
| Mul xs -> c_mul (List.map f xs)
......@@ -2038,9 +2038,9 @@ struct
(* --- Non-Binding Morphism --- *)
(* -------------------------------------------------------------------------- *)
let rebuild f e =
match e.repr with
| Kint _ | Kreal _ | Fvar _ | True | False -> e
let rebuild f e0 =
match e0.repr with
| Kint _ | Kreal _ | Fvar _ | Bvar _ | True | False -> e0
| Not e -> e_not (f e)
| Add xs -> e_sum (List.map f xs)
| Mul xs -> e_prod (List.map f xs)
......@@ -2061,7 +2061,8 @@ struct
| Aset(x,y,z) -> e_set (f x) (f y) (f z)
| Rget(x,g) -> e_getfield (f x) g
| Rdef gxs -> e_record (List.map (fun (g,x) -> g, f x) gxs)
| Bvar _ | Bind _ | Apply _ -> assert false
| Bind(q,t,a) -> c_bind q t (f a)
| Apply(e,es) -> c_apply (f e) (List.map f es)
(* -------------------------------------------------------------------------- *)
(* --- General Substitution --- *)
......@@ -2086,32 +2087,23 @@ struct
let fresh sigma t = fresh sigma.pool t
let check v =
if not (lc_closed v) then raise (Invalid_argument "Qed.Sigma")
let checked v = check v ; v
let rec compute e = function
| EMPTY -> raise Not_found
| FUN(f,EMPTY) -> checked (f e)
| FUN(f,EMPTY) -> f e
| MAP(m,EMPTY) -> Tmap.find e m
| FUN(f,s) -> (try checked (f e) with Not_found -> compute e s)
| FUN(f,s) -> (try f e with Not_found -> compute e s)
| MAP(m,s) -> (try Tmap.find e m with Not_found -> compute e s)
let get sigma a = compute a sigma.shared
let add sigma a b =
check a ; check b ;
sigma.shared <- match sigma.shared with
| MAP(m,s) -> MAP (Tmap.add a b m,s)
| (FUN _ | EMPTY) as s -> MAP (Tmap.add a b Tmap.empty,s)
let add_map sigma m =
if not (Tmap.is_empty m) then
begin
Tmap.iter (fun a b -> check a ; check b) m ;
sigma.shared <- MAP(m,sigma.shared)
end
sigma.shared <- MAP(m,sigma.shared)
let add_fun sigma f =
sigma.shared <- FUN(f,sigma.shared)
......@@ -2126,25 +2118,25 @@ struct
let rec subst sigma alpha e =
let mu = cache () in
compute mu sigma alpha e
incache mu sigma alpha e
and incache mu sigma alpha e =
get mu (compute mu sigma alpha) e
and compute mu sigma alpha e =
try Subst.get sigma e with Not_found ->
let r =
match e.repr with
| Bvar(k,_) -> Intmap.find k alpha
| Bind _ ->
(* Not in cache *)
bind sigma alpha [] e
| Apply(e,es) ->
let phi = incache mu sigma alpha in
apply sigma Intmap.empty (phi e) (List.map phi es)
| _ -> rebuild (incache mu sigma alpha) e
in
(if lc_closed e && lc_closed r then Subst.add sigma e r) ; r
let r =
match e.repr with
| Bvar(k,_) -> Intmap.find k alpha
| Bind _ ->
(* Not in cache *)
bind sigma alpha [] e
| Apply(e,es) ->
let phi = incache mu sigma alpha in
apply sigma Intmap.empty (phi e) (List.map phi es)
| _ -> rebuild (incache mu sigma alpha) e
in
(if lc_closed e && lc_closed r then Subst.add sigma e r) ; r
and bind sigma alpha qs e =
match e.repr with
......@@ -2169,7 +2161,8 @@ struct
let k = Bvars.order g.bind in
apply sigma (Intmap.add k v beta) g vs
| _ ->
subst sigma beta f
let f' = if Intmap.is_empty beta then f else subst sigma beta f in
c_apply f' vs
let e_subst sigma e =
subst sigma Intmap.empty e
......@@ -2282,11 +2275,6 @@ struct
let e_exists = bind_xs Exists
let e_lambda = bind_xs Lambda
let rec binders e =
match e.repr with
| Bind(q,_,e) -> q :: binders e
| _ -> []
(* -------------------------------------------------------------------------- *)
(* --- Iterators --- *)
(* -------------------------------------------------------------------------- *)
......
......@@ -958,17 +958,15 @@ let lemma g =
let cc g = let hs,p = forall_intro g in sequence hs , p
in Lang.local ~vars:(F.varsp g) cc g
let introduction sequent =
let cc (hs,g) =
let flag = ref false in
let intro p = let q = exist_intro p in if q != p then flag := true ; q in
let hj = List.map (map_step intro) hs.seq_list in
let hi,p = forall_intro g in
if not !flag && hi == [] then
if p == g then None else Some (hs , p)
else
Some (sequence (hi @ hj) , p)
in Lang.local ~vars:(vars_seq sequent) cc sequent
let introduction (hs,g) =
let flag = ref false in
let intro p = let q = exist_intro p in if q != p then flag := true ; q in
let hj = List.map (map_step intro) hs.seq_list in
let hi,p = forall_intro g in
if not !flag && hi == [] then
if p == g then None else Some (hs , p)
else
Some (sequence (hi @ hj) , p)
let introduction_eq s = match introduction s with
| Some s' -> s'
......@@ -1074,6 +1072,8 @@ end
(* -------------------------------------------------------------------------- *)
let rec fixpoint limit solvers sigma s0 =
if limit > 0 then compute limit solvers sigma s0 else s0
and compute limit solvers sigma s0 =
!Db.progress ();
let s1 =
if Wp_parameters.Ground.get () then ground s0
......
......@@ -457,7 +457,7 @@ class tactic
method private status target =
List.iter (fun fd -> fd#select target) wfields ;
try tac#select (self :> feedback) target
try Lang.local ~pool:self#pool (tac#select (self :> feedback)) target
with Not_found | Exit -> Not_applicable
method select ~process ~browser ~composer ~tree
......
......@@ -361,7 +361,8 @@ struct
let create tree ~anchor tactic process =
let axioms , sequent = Wpo.compute anchor.goal in
let dseqs = process sequent in
let vars = Conditions.vars_seq sequent in
let dseqs = Lang.local ~vars process sequent in
let title = tactic.ProofScript.header in
let goals = List.map
(fun (part,s) -> part , mk_goal tree ~title ~part ~axioms s) dseqs
......
......@@ -65,7 +65,7 @@ let jconfigure (console : #Tactical.feedback) jtactic goal =
| Some(tactical,selection) ->
console#set_title "%s" tactical#title ;
let verdict =
try tactical#select console selection
try Lang.local ~pool:console#pool (tactical#select console) selection
with Not_found | Exit -> Not_applicable
in
begin
......
......@@ -25,14 +25,14 @@ open Strategy
let configure (console : #Tactical.feedback) strategy =
let { tactical ; selection ; arguments } = strategy in
let verdict =
let verdict () =
try
tactical#reset ;
Strategy.set_args tactical arguments ;
tactical#select console selection
with Not_found | Exit -> Not_applicable
in
match verdict with
match Lang.local ~pool:console#pool verdict () with
| Applicable process when not console#has_error ->
let title = tactical#title in
let script = ProofScript.jtactic ~title tactical selection in
......
......@@ -21,11 +21,11 @@
let m_1 = m[shift_sint32(a, 1) <- m[a_2]] : (addr,int) farray in
let m_2 = m_1[shift_sint32(a, 2) <- m_1[a_2]] : (addr,int) farray in
let m_3 = m_2[shift_sint32(a, 3) <- m_2[a_2]] : (addr,int) farray in
(0 <= i) ->
(0 <= i_1) ->
(0 <= i) ->
(region(a.base) <= 0) ->
(i <= 9) ->
(i_1 <= 9) ->
(i <= 9) ->
linked(t) ->
is_sint32(i) ->
valid_rw(t, a_1, 10) ->
......
......@@ -13,10 +13,10 @@
goal f_ensures:
forall i_3,i_2,i_1,i : int.
((match_bool((eqb(i_3, i_2)), 1, 0)) = (match_bool((eqb(i_1, i)), 1, 0))) ->
is_sint32(i) ->
is_sint32(i_1) ->
is_sint32(i_2) ->
is_sint32(i_3) ->
is_sint32(i_2) ->
is_sint32(i_1) ->
is_sint32(i) ->
((i_3 = i_2) <-> (i_1 = i))
[wp] 1 goal generated
------------------------------------------------------------
......
......@@ -98,7 +98,7 @@ Assume {
Have: i <= 19.
(* Call Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
(((j < i_1) \/ (i_1 < i)) -> (t2_0[i_1] = t2_1[i_1])))).
(((i_1 < i) \/ (j < i_1)) -> (t2_0[i_1] = t2_1[i_1])))).
(* Call Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
(((i_1 < i) \/ (20 <= i_1)) -> (t3_0[i_1] = t3_1[i_1])))).
......
......@@ -28,7 +28,7 @@ Assume: 'UNION_LIFT' 'UNION_EQ'
Prove: (0<=k_0) -> (k_0<=n_0)
-> (((k_0<n_0) -> (-1<=k_0)) /\ ((0<k_0) -> (k_0<=(1+n_0)))
/\ (forall i_0:int.
(i_0<=n_0) -> (0<=i_0)
(0<=i_0) -> (i_0<=n_0)
-> ((i_0=k_0) \/ ((k_0<i_0) /\ (i_0<=n_0))
\/ ((0<=i_0) /\ (i_0<k_0)))))
......
......@@ -35,7 +35,7 @@
[wp] Report out: 'tests/wp_acsl/result_qualif/arith.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma 20 1 (1..8) 21 100%
Lemma 20 1 (8..20) 21 100%
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
cast_sgn_usgn 1 - 1 100%
......
......@@ -26,6 +26,6 @@
[wp] Report out: 'tests/wp_acsl/result_qualif/simpl_is_type.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 3 6 (88..112) 9 100%
f 3 6 (96..120) 9 100%
g 3 3 (36..48) 6 100%
-------------------------------------------------------------
......@@ -19,8 +19,8 @@ goal myMain_assigns:
let a_2 = shiftfield_F1_FD_pos(a) : addr in
let x = t_1[a_2] : int in
(x <> i) ->
(region(a.base) <= 0) ->
(region(a_1.base) <= 0) ->
(region(a.base) <= 0) ->
linked(t) ->
is_sint32(i) ->
is_sint32(x) ->
......@@ -93,8 +93,8 @@ goal myMain_ensures_KO:
forall a_1,a : addr.
let a_2 = Load_S2_A(a_1, t_1) : S2_A in
let a_3 = Load_S2_A(a_1, havoc(t, t_1, a_1, 1)) : S2_A in
(region(a.base) <= 0) ->
(region(a_1.base) <= 0) ->
(region(a.base) <= 0) ->
IsS2_A(a_2) ->
IsS2_A(a_3) ->
EqS2_A(a_3, a_2)
......
......@@ -9,13 +9,9 @@
Goal Post-condition (file tests/wp_bts/bts_2159.i, line 5) in 'job':
Assume {
Type: is_sint32(s) /\ is_sint32(s_1) /\ is_sint32(s_2) /\ is_sint32(x).
Type: is_sint32(s) /\ is_sint32(s_1) /\ is_sint32(x).
If 0 <= x
Then {
If x <= 100
Then { Have: ((s + x) = s_1) /\ ((s_2 + x) = s_1). }
Else { Have: s_1 = s. }
}
Then { If x <= 100 Then { Have: (s + x) = s_1. } Else { Have: s_1 = s. } }
Else { Have: s_1 = s. }
}
Prove: (if ((0 <= x) & (x <= 100)) then L_Id(s + x) else L_Id(s)) = s_1.
......
......@@ -21,7 +21,7 @@
[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
exo1 6 4 (176..224) 10 100%
exo1 6 4 (176..200) 10 100%
-------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function exo1
......@@ -48,5 +48,5 @@ exo1 6 4 (176..224) 10 100%
[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
exo1 6 9 (176..224) 15 100%
exo1 6 9 (176..200) 15 100%
-------------------------------------------------------------
......@@ -37,7 +37,7 @@
[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo3_solved.simplified.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
pair 16 10 (104..128) 26 100%
pair 16 10 (88..112) 26 100%
-------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function pair
......
......@@ -24,8 +24,8 @@ Proof.
rewrite 2!Z.add_assoc.
apply H6; omega.
- apply Q_trans with (t_1:=t_1) (a_1:=shift_sint32 a_1 (-i)).
+ apply IHP_same_elements1. reflexivity. destruct a_1; unfold shift_sint32, shift; simpl. f_equal; omega.
+ apply IHP_same_elements2. destruct a_1; unfold shift_sint32, shift; simpl. f_equal; omega. reflexivity.
+ apply IHP_same_elements1. destruct a_1; unfold shift_sint32, shift; simpl. f_equal; omega. reflexivity.
+ apply IHP_same_elements2. reflexivity. destruct a_1; unfold shift_sint32, shift; simpl. f_equal; omega.
Qed.
Goal typed_lemma_test.
......@@ -37,3 +37,5 @@ destruct H.
- right. split;assumption.
(* auto with zarith. *)
Qed.
......@@ -147,8 +147,8 @@
((P_same_elements t_1 t a_1 a i_3%Z i%Z))
| Q_trans: forall (i_1 i : Z), forall (t_2 t_1 t : farray addr Z),
forall (a_2 a_1 a : addr),
((P_same_elements t_1 t a_2 a_1 i_1%Z i%Z)) ->
((P_same_elements t_2 t_1 a_1 a i_1%Z i%Z)) ->
((P_same_elements t_1 t a_2 a_1 i_1%Z i%Z)) ->
((P_same_elements t_2 t a_2 a i_1%Z i%Z)).
Goal
......
......@@ -16,8 +16,8 @@ Assume {
(* Pre-condition *)
Have: (0 <= m) /\ (0 <= n).
(* Invariant 'PI' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((i_2 < m) -> ((0 <= i_3) ->
((i_3 < i_1) ->
Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> ((0 <= i_2) ->
((i_2 < m) ->
(Mint_0[shift_sint32(p, i_3)] < Mint_0[shift_sint32(q, i_2)]))))).
(* Invariant 'I' *)
Have: (0 <= i_1) /\ (i_1 <= n).
......@@ -56,8 +56,8 @@ Assume {
(* Pre-condition *)
Have: (0 <= m) /\ (0 <= n).
(* Invariant 'PI' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((i_1 < m) -> ((0 <= i_2) ->
((i_2 < i) ->
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
((i_1 < m) ->
(Mint_0[shift_sint32(p, i_2)] < Mint_0[shift_sint32(q, i_1)]))))).
(* Invariant 'I' *)
Have: (0 <= i) /\ (i <= n).
......@@ -91,8 +91,8 @@ Assume {
(* Pre-condition *)
Have: (0 <= m) /\ (0 <= n).
(* Invariant 'PI' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((i_3 < m) -> ((0 <= i_4) ->
((i_4 < i_2) ->
Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i_2) -> ((0 <= i_3) ->
((i_3 < m) ->
(Mint_0[shift_sint32(p, i_4)] < Mint_0[shift_sint32(q, i_3)]))))).
(* Invariant 'I' *)
Have: (0 <= i_2) /\ (i_2 <= n).
......@@ -126,8 +126,8 @@ Assume {
(* Pre-condition *)
Have: (0 <= m) /\ (0 <= n).
(* Invariant 'PI' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((i_1 < m) -> ((0 <= i_2) ->
((i_2 < i) ->
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
((i_1 < m) ->
(Mint_0[shift_sint32(p, i_2)] < Mint_0[shift_sint32(q, i_1)]))))).
(* Invariant 'I' *)
Have: (0 <= i) /\ (i <= n).
......@@ -165,8 +165,8 @@ Assume {
(* Pre-condition *)
Have: (0 <= m) /\ (0 <= n).
(* Invariant 'PI' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((i_2 < m) -> ((0 <= i_3) ->
((i_3 < i) ->
Have: forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 < i) -> ((0 <= i_2) ->
((i_2 < m) ->
(Mint_0[shift_sint32(p, i_3)] < Mint_0[shift_sint32(q, i_2)]))))).
(* Invariant 'I' *)
Have: (0 <= i) /\ (i <= n).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment