diff --git a/src/plugins/qed/logic.mli b/src/plugins/qed/logic.mli
index f481bf9030c29a002df93d1d4996e8d67236adfe..96351d95a36f89d362d2afa30bf2afe4a592ed49 100644
--- a/src/plugins/qed/logic.mli
+++ b/src/plugins/qed/logic.mli
@@ -324,6 +324,9 @@ sig
val e_forall : var list -> term -> term
val e_exists : var list -> term -> term
val e_lambda : var list -> term -> term
+ val e_close_forall : term -> term
+ val e_close_exists : term -> term
+ val e_close_lambda : term -> term
val e_apply : term -> term list -> term
val e_bind : binder -> var -> term -> term
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 188886fc5ff3f2e249a3c361f148555afab81d7d..f6ba7a4013634b982f5183f44b039aa2d74e08d3 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2143,6 +2143,38 @@ struct
set mu (e_var x) (c_bvar k t) ;
walk mu x lc
+ (* Alpha-convert free-variables in xs with the top-most bound variables *)
+ (* Only activate flag subset if lc.vars is a subset of xs *)
+ (* Warning: ~reversed:false needs to compute the length of xs *)
+ let lc_close_xs ?(subset = false) ~reversed xs (lc : lc_term) : lc_term =
+ let mu = cache () in
+ begin
+ if reversed then
+ let n = Bvars.order lc.bind in
+ List.iteri (fun i x ->
+ set mu (e_var x) (c_bvar (n+i) (tau_of_var x))
+ ) xs
+ else
+ let n = Bvars.order lc.bind + List.length xs -1 in
+ List.iteri (fun i x ->
+ set mu (e_var x) (c_bvar (n-i) (tau_of_var x))
+ ) xs
+ end;
+ (* if Vars.subset lc.vars xs then*)
+ if subset then
+ let rec walk mu lc =
+ if not (Vars.is_empty lc.vars) then
+ get mu (lc_alpha (walk mu)) lc
+ else lc in
+ walk mu lc
+ else
+ let xs = List.fold_left (fun xs x -> Vars.add x xs) Vars.empty xs in
+ let rec walk mu lc =
+ if Vars.intersect xs lc.vars then
+ get mu (lc_alpha (walk mu)) lc
+ else lc in
+ walk mu lc
+
(* Alpha-convert top-most bound variable with free-variable x *)
let lc_open x (lc : lc_term) : lc_term =
let rec walk mu k lc =
@@ -2269,6 +2301,15 @@ struct
let filter sigma e =
Subst.filter sigma e || not (Bvars.is_empty e.bind)
+ let bind_qxs qxs e =
+ let qxs = List.filter (function
+ | Lambda, _ -> true
+ | Forall, x | Exists, x -> Vars.mem x e.vars
+ ) qxs in
+ let rxs = List.map (fun (_q, x) -> x) qxs in
+ let e = lc_close_xs ~reversed:true rxs e in
+ List.fold_left (fun e (q, x) -> c_bind q (tau_of_var x) e) e qxs
+
let rec subst sigma alpha e =
if filter sigma e then
incache (Subst.cache sigma) sigma alpha e
@@ -2304,21 +2345,7 @@ struct
let alpha = Intmap.add k (e_var x) alpha in
let qs = (q,x) :: qs in
bind sigma alpha qs a
- | _ ->
- (* HERE:
- This final binding of variables could be parallelized
- if Bvars is precise enough *)
- List.fold_left
- (fun e (q,x) ->
- if Vars.mem x e.vars then
- let t = tau_of_var x in
- (* HERE:
- possible to insert a recursive call to let-intro
- it will use a new instance of e_subst_var that
- will work on a different sigma *)
- c_bind q t (lc_close x e)
- else e
- ) (subst sigma alpha e) qs
+ | _ -> bind_qxs qs (subst sigma alpha e)
and apply sigma beta f vs =
match f.repr, vs with
@@ -2504,13 +2531,47 @@ struct
let e_close qs a = List.fold_left (fun b (q,x) -> e_bind q x b) a qs
- let rec bind_xs q xs e =
- match xs with [] -> e | x::xs -> e_bind q x (bind_xs q xs e)
+ let bind_xs q xs e =
+ let xs = match q with
+ | Lambda -> xs
+ | Forall | Exists -> List.filter (fun x -> Vars.mem x e.vars) xs
+ in (* let_intro_case have to be called sequentially because of cases like
+ '\forall x y, 42 = x + y -> P' where we detect two let-in variables in parralel
+ but we can only simplify one in practice.*)
+ let rec aux e xs =
+ let e, xs, changed = List.fold_right (fun x (e, xs', b) ->
+ match let_intro_case q x e with
+ | None -> e, x::xs', b
+ | Some v -> e_subst_var x v e, xs', true
+ ) xs (e, [], false) in
+ if changed then aux e xs else e, xs
+ in
+ let e, xs = aux e xs in
+ let e = lc_close_xs ~reversed:false xs e in
+ List.fold_right (fun x e -> c_bind q (tau_of_var x) e) xs e
let e_forall = bind_xs Forall
let e_exists = bind_xs Exists
let e_lambda = bind_xs Lambda
+ let bind_all q e =
+ let rec aux e =
+ let e, changed = Vars.fold (fun x (e, b) ->
+ match let_intro_case q x e with
+ | None -> e, b
+ | Some v -> e_subst_var x v e, true
+ ) e.vars (e, false) in
+ if changed then aux e else e
+ in
+ let e = aux e in
+ let rxs = List.sort (fun x y -> POOL.compare y x) (Vars.elements e.vars) in
+ let e = lc_close_xs ~subset:true ~reversed:true rxs e in
+ List.fold_left (fun e x -> c_bind q (tau_of_var x) e) e rxs
+
+ let e_close_forall = bind_all Forall
+ let e_close_exists = bind_all Exists
+ let e_close_lambda = bind_all Lambda
+
(* -------------------------------------------------------------------------- *)
(* --- Iterators --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index eabb6008c81ca45170de446d1244c53128f7e8e7..7869f466d863f94344ca26fb4337f80d7d76551e 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -825,7 +825,7 @@ struct
let e_vars e = List.sort Var.compare (Vars.elements (vars e))
let p_vars = e_vars
let p_call = e_fun ~result:Prop
- let p_close p = p_forall (p_vars p) p
+ let p_close = e_close_forall
let occurs x t = Vars.mem x (vars t)
let intersect a b = Vars.intersect (vars a) (vars b)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index df29522c76ece81e57062b386000ae24c92c0429..2aa95174028d023e0f7831b5cb8d8e0656e045f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -4,9 +4,9 @@
[rte:annot] annotating function foo
[wp] 2 goals scheduled
---------------------------------------------
---- Context 'typed_foo' Cluster 'Init_S1_X'
+--- Context 'typed_foo' Cluster 'Chunk'
---------------------------------------------
-theory Init_S1_X
+theory Chunk
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
@@ -21,8 +21,18 @@ theory Init_S1_X
(* use map.Map *)
- type Init_S1_X =
- | Init_S1_X1 (Init_F1_X_a:bool) (Init_F1_X_b:bool) (Init_F1_X_c:bool)
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use frama_c_wp.cint.Cint *)
+
+ predicate is_sint8_chunk (m:addr -> int) =
+ forall a:addr. is_sint8 (get m a)
+
+ predicate is_sint16_chunk (m:addr -> int) =
+ forall a:addr. is_sint16 (get m a)
+
+ predicate is_sint32_chunk (m:addr -> int) =
+ forall a:addr. is_sint32 (get m a)
end
---------------------------------------------
--- Context 'typed_foo' Cluster 'S1_X'
@@ -51,6 +61,27 @@ theory S1_X
(is_sint8 (F1_X_a s) /\ is_sint16 (F1_X_b s)) /\ is_sint32 (F1_X_c s)
end
---------------------------------------------
+--- Context 'typed_foo' Cluster 'Init_S1_X'
+---------------------------------------------
+theory Init_S1_X
+ (* 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 *)
+
+ type Init_S1_X =
+ | Init_S1_X1 (Init_F1_X_a:bool) (Init_F1_X_b:bool) (Init_F1_X_c:bool)
+end
+---------------------------------------------
--- Context 'typed_foo' Cluster 'Compound'
---------------------------------------------
theory Compound
@@ -177,37 +208,6 @@ theory Compound
separated p 3 q n ->
Load_Init_S1_X p (havoc init1 init q n) = Load_Init_S1_X p init
end
----------------------------------------------
---- Context 'typed_foo' 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_sint8_chunk (m:addr -> int) =
- forall a:addr. is_sint8 (get m a)
-
- predicate is_sint16_chunk (m:addr -> int) =
- forall a:addr. is_sint16 (get m a)
-
- predicate is_sint32_chunk (m:addr -> int) =
- forall a:addr. is_sint32 (get m a)
-end
[wp:print-generated]
theory WP
(* use why3.BuiltIn.BuiltIn *)
@@ -226,16 +226,15 @@ end
(* use frama_c_wp.memory.Memory *)
- (* use Init_S1_X *)
+ (* use Chunk *)
- (* use Compound *)
+ (* use S1_X *)
- (* use Chunk *)
+ (* use Compound *)
goal wp_goal :
- forall t:addr -> bool, x:Init_S1_X, t1:int -> int, t2:addr -> int, t3:
- addr -> int, t4:addr -> int, a:addr.
- Load_Init_S1_X a t = x ->
+ forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
+ addr -> int, a:addr.
region (a.base) <= 0 ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->