Commit d83bd3db authored by Heiko Becker's avatar Heiko Becker

Fix ssa predicate to compute proper "live variables"

parent 7bd27dc4
......@@ -97,33 +97,34 @@ Proof.
auto.
Qed. *)
Inductive ssa (V:Type): (expr V) -> NatSet.t -> NatSet.t -> Prop :=
| ssaVar x inVars outVars:
(x inVars) ->
(NatSet.Equal inVars outVars) ->
ssa (Var _ x) inVars outVars
| ssaConst m v inVars outVars:
(NatSet.Equal inVars outVars) ->
ssa (Const m v) inVars outVars
| ssaUnop u e inVars outVars:
ssa e inVars outVars ->
ssa (Unop u e) inVars outVars
| ssaBinop b e1 e2 inVars outVars:
ssa e1 inVars outVars ->
ssa e2 inVars outVars ->
ssa (Binop b e1 e2) inVars outVars
| ssaFma e1 e2 e3 inVars outVars:
ssa e1 inVars outVars ->
ssa e2 inVars outVars ->
ssa e3 inVars outVars ->
ssa (Fma e1 e2 e3) inVars outVars
| ssaBinop b e1 e2 inVars outVars1 outVars2:
ssa e1 inVars outVars1 ->
ssa e2 inVars outVars2 ->
ssa (Binop b e1 e2) inVars (NatSet.union outVars1 outVars2)
| ssaFma e1 e2 e3 inVars outVars1 outVars2 outVars3:
ssa e1 inVars outVars1 ->
ssa e2 inVars outVars2 ->
ssa e3 inVars outVars3 ->
ssa (Fma e1 e2 e3) inVars (NatSet.union outVars1 (NatSet.union outVars2 outVars3))
| ssaDowncast m e inVars outVars:
ssa e inVars outVars ->
ssa (Downcast m e) inVars outVars
| ssaLet m x e s inVars outVars:
| ssaLet m x e s inVars outVars1 outVars2:
NatSet.mem x inVars = false ->
ssa e inVars outVars ->
ssa s (NatSet.add x inVars) outVars ->
ssa (Let m x e s) inVars outVars
ssa e inVars outVars1 ->
ssa s (NatSet.add x inVars) outVars2 ->
ssa (Let m x e s) inVars (NatSet.union outVars1 outVars2)
(*
| ssaCond e1 e2 e3 inVars outVars:
ssa e1 inVars outVars ->
......@@ -153,13 +154,20 @@ Lemma ssa_equal_set V (f:expr V) inVars inVars' outVars:
Proof.
intros set_eq ssa_f.
revert set_eq; revert inVars'.
induction ssa_f; constructor; auto.
- now apply set_eq.
induction ssa_f; try constructor; auto.
- intros. hnf in H0. hnf in set_eq. rewrite set_eq; auto.
- hnf in *; split; intros.
+ rewrite <- H0. rewrite <- set_eq; auto.
+ rewrite set_eq. rewrite H0. auto.
- intros. hnf in *. split; intros.
+ rewrite <- H; rewrite <- set_eq; auto.
+ rewrite set_eq; rewrite H; auto.
- apply NatSetProps.Dec.F.not_mem_iff. intros ?. set_tac. now apply H, set_eq.
- apply IHssa_f2.
split; set_tac; intros[?|Ha]; auto; apply set_eq in Ha; auto.
Qed.
(**
(* TODO: shows that outVars is not needed *)
Lemma ssa_open_out V (f:expr V) inVars outVars outVars' :
ssa f inVars outVars ->
......@@ -167,6 +175,7 @@ Lemma ssa_open_out V (f:expr V) inVars outVars outVars' :
Proof.
intros ssa_f. induction ssa_f; constructor; auto.
Qed.
**)
Fixpoint validSSA (f:expr Q) (inVars:NatSet.t) :=
match f with
......@@ -186,21 +195,21 @@ Lemma validSSA_sound f inVars:
exists outVars, ssa f inVars outVars.
Proof.
induction f in inVars |- *; cbn; intros H.
- exists NatSet.empty. constructor. set_tac.
- exists NatSet.empty. constructor.
- exists inVars. constructor; [ set_tac | auto using NatSetProps.equal_refl].
- exists inVars. constructor; auto using NatSetProps.equal_refl.
- destruct (IHf _ H) as [O ?]. exists O.
now constructor.
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
exists (O1 O2).
constructor; eauto using ssa_open_out.
constructor; auto.
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
edestruct IHf3 as [O3 ?]; eauto.
exists (O1 O2 O3).
constructor; eauto using ssa_open_out.
constructor; auto.
- destruct (IHf _ H) as [O ?]. exists O.
now constructor.
- andb_to_prop H.
......@@ -208,7 +217,7 @@ Proof.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
exists (O1 O2).
constructor; eauto using ssa_open_out.
constructor; auto.
(*
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
......
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