Commit 8585245b authored by Heiko Becker's avatar Heiko Becker

Fix ssa predicate usage in validator proof

parent d83bd3db
This diff is collapsed.
......@@ -150,7 +150,7 @@ Definition toRMap (d:expr R -> option mType) (e: expr R) :=
Arguments toRMap _ _/.
(**
Define the set of "used" variables of an exprression to be the set of variables
Define the set of "used" variables of an expression to be the set of variables
occuring in it
**)
(*
......@@ -162,7 +162,7 @@ Fixpoint usedVars (V:Type) (e:expr V) :NatSet.t :=
| Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
| Fma e1 e2 e3 => NatSet.union (usedVars e1) (NatSet.union (usedVars e2) (usedVars e3))
| Downcast _ e1 => usedVars e1
| Let _ _ e1 e2 => usedVars e1 usedVars e2
| Let _ x e1 e2 => NatSet.union (NatSet.singleton x) (NatSet.union (usedVars e1) (usedVars e2))
| Cond e1 e2 e3 => usedVars e1 usedVars e2 usedVars e3
end.
*)
......
......@@ -245,11 +245,15 @@ Proof.
apply Rlt_Qlt in H3. lra. }
- destruct types_defined
as [? [? [[? [? ?]]?]]].
inversion ssa_f.
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; eapply IHf1; eauto; set_tac).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; eapply IHf2; eauto; set_tac).
inversion ssa_f; subst.
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1.
{ Flover_compute; try congruence. eapply IHf1; try eauto.
- now extended_ssa.
- set_tac. }
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2.
{ Flover_compute; try congruence. eapply IHf2; try eauto.
- now extended_ssa.
- set_tac. }
repeat split;
[ intros; subst; Flover_compute; congruence |
auto | auto |].
......@@ -321,11 +325,11 @@ Proof.
- destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
- assert (~ (snd iv_f2) == 0).
{ hnf; intros. destruct L; try lra.
assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H7; lra).
assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H12; lra).
lra. }
assert (~ (fst iv_f2) == 0).
{ hnf; intros; destruct L; try lra.
assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H8; lra).
assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H13; lra).
lra. }
repeat (rewrite <- Q2R_inv in *; try auto).
repeat rewrite <- Q2R_mult in *.
......@@ -336,12 +340,18 @@ Proof.
- destruct types_defined
as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
inversion ssa_f.
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; eapply IHf1; eauto; set_tac).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; eapply IHf2; eauto; set_tac).
assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
by (Flover_compute; try congruence; eapply IHf3; eauto; set_tac).
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1.
{ Flover_compute; try congruence. eapply IHf1; try eauto.
- now extended_ssa.
- set_tac. }
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2.
{ Flover_compute; try congruence. eapply IHf2; try eauto.
- now extended_ssa.
- set_tac. }
assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3.
{ Flover_compute; try congruence. eapply IHf3; try eauto.
- now extended_ssa.
- set_tac. }
repeat split; try auto.
apply validRanges_single in valid_f1;
apply validRanges_single in valid_f2;
......@@ -393,14 +403,18 @@ Proof.
Flover_compute; try congruence.
inversion ssa_f; subst.
canonize_hyps.
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; eapply IHf1; eauto; set_tac).
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1.
{ Flover_compute; try congruence. eapply IHf1; try eauto.
- eapply ssa_outVars_extensible; try eauto. set_tac.
- set_tac. }
pose proof (validRanges_single _ _ _ _ valid_f1) as valid_single_f1.
destruct valid_single_f1 as [iv_f1 [err_f1 [v [find_v [eval_f1 valid_bounds_f1]]]]].
rewrite find_v in *; inversion Heqo0; subst.
assert (validRanges f2 A (updEnv n v E) (toRTMap (toRExpMap Gamma))) as valid_f2.
{ eapply IHf2; eauto.
- eapply ssa_equal_set; eauto.
- eapply ssa_outVars_extensible with (outVars1:=outVars2); try eauto;
[ | set_tac].
eapply ssa_equal_set; eauto.
intros x. split; set_tac; intros; tauto.
- intros v0 mem_v0.
unfold updEnv.
......@@ -426,7 +440,7 @@ Proof.
set_tac.
assert (NatSet.In n fVars) as in_free
by (apply preVars_free; eapply preIntvVars_sound; eauto).
exfalso. apply H5. set_tac. }
exfalso. apply H3. set_tac. }
repeat split; auto.
+ intros vR ?.
assert (vR = v) by (eapply meps_0_deterministic; eauto); now subst.
......@@ -438,121 +452,3 @@ Proof.
repeat split; eauto; try lra.
econstructor; eauto; reflexivity.
Qed.
\ No newline at end of file
(*
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
forall Gamma E fVars dVars outVars P,
ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A ->
P_intv_sound E P ->
NatSet.Subset (preIntvVars P) fVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f A P dVars = true ->
validTypesCmd f Gamma ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros * ssa_f dVars_sound fVars_valid preIntvVars_free usedVars_subset
valid_bounds_f valid_types_f;
cbn in *.
- Flover_compute.
inversion ssa_f; subst.
canonize_hyps.
pose proof (validIntervalbounds_sound e Gamma (E:=E) (fVars:=fVars) L) as validIV_e.
destruct valid_types_f
as [[mG [find_mG [_ [_ [validt_e validt_f]]]]] _].
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e.
{ apply validIV_e; try auto.
set_tac. repeat split; auto.
hnf; intros; subst.
set_tac. }
assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
{ hnf. intros a; split; intros in_set; set_tac.
- destruct in_set as [ ? | [? ?]]; try auto; set_tac.
destruct H0; auto.
- destruct in_set as [? | ?]; try auto; set_tac.
destruct H as [? | [? ?]]; auto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single_e.
destruct valid_single_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]].
rewrite find_v in *; inversion Heqo; subst.
specialize (IHf Gamma (updEnv n v E) fVars (NatSet.add n dVars)) as IHf_spec.
assert (validRangesCmd f A (updEnv n v E) (toRTMap (toRExpMap Gamma))).
{ eapply IHf_spec; eauto.
- eapply ssa_equal_set. symmetry in H. apply H. apply H7.
- intros v0 mem_v0.
unfold updEnv.
case_eq (v0 =? n); intros v0_eq.
+ rename R1 into eq_lo;
rename R0 into eq_hi.
rewrite Nat.eqb_eq in v0_eq; subst.
exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra.
+ apply dVars_sound.
set_tac.
destruct mem_v0 as [? | [? ?]]; try auto.
rewrite Nat.eqb_neq in v0_eq.
congruence.
- hnf. intros x ? ?.
unfold updEnv.
case_eq (x =? n); intros case_x; auto.
rewrite Nat.eqb_eq in case_x. subst.
set_tac.
assert (NatSet.In n fVars) as in_free
by (apply preIntvVars_free; eapply preIntvVars_sound; eauto).
(* by (destruct (fVars_valid n iv); auto; set_tac). *)
exfalso. apply H6. set_tac.
- intros x x_contained.
set_tac.
repeat split; try auto.
+ hnf; intros; subst. apply H1; set_tac.
+ hnf; intros. apply H1; set_tac. }
(*
destruct x_contained as [x_free | x_def].
+ destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
exists m_x.
unfold updDefVars. case_eq (x =? n); intros eq_case; try auto.
rewrite Nat.eqb_eq in eq_case.
subst.
exfalso; apply H6; set_tac.
+ set_tac.
destruct x_def as [x_n | x_def]; subst.
* exists REAL; unfold updDefVars; rewrite Nat.eqb_refl; auto.
* destruct x_def. destruct (types_valid x) as [m_x Gamma_x].
{ rewrite NatSet.union_spec; auto. }
{ exists m_x.
unfold updDefVars; case_eq (x =? n); intros eq_case; try auto.
rewrite Nat.eqb_eq in eq_case; subst.
congruence. }
{ clear L R1 R0 R IHf.
hnf. intros a a_freeVar.
rewrite NatSet.diff_spec in a_freeVar.
destruct a_freeVar as [a_freeVar a_no_dVar].
apply usedVars_subset.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
repeat split; try auto.
+ hnf; intros; subst.
apply a_no_dVar.
rewrite NatSet.add_spec; auto.
+ hnf; intros a_dVar.
apply a_no_dVar.
rewrite NatSet.add_spec; auto. } *)
{ repeat split; try auto.
- intros vR ?.
assert (vR = v) by (eapply meps_0_deterministic; eauto); subst.
auto.
- apply validRangesCmd_single in H0.
destruct H0 as [? [? [? [? [? ?]]]]].
repeat eexists; eauto.
econstructor; try eauto.
+ lra.
+ lra. }
- unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validIntervalbounds_sound e (E:=E) Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
destruct valid_types_f as [? ?].
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e by (apply valid_iv_e; auto).
split; try auto.
apply validRanges_single in valid_e.
destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
Qed.
*)
......@@ -384,6 +384,7 @@ Proof.
*)
Qed.
(*
Lemma validRanges_ssa_extension (e: expr Q) A E Gamma
vR' n fVars:
NatSet.Subset (freeVars e) fVars ->
......@@ -463,15 +464,18 @@ Proof.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *)
rewrite freeVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
- rename n0 into x. simpl in Hsub.
assert (NatSet.Subset (freeVars e1) fVars) as Hsub1 by set_tac.
destruct Hranges as [[Hranges1 Hranges2] Hranges].
specialize (IHe1 _ _ Hsub1 Hnotin Hranges1).
destruct Hranges as [iv [err [vR Hranges]]].
destruct Hranges as (iv & err & vR & find_e & eval_real & bounded_e).
inversion eval_real; subst.
specialize (Hranges2 v1 H7).
specialize (IHe2 (updEnv x v1 E) fVars).
repeat split; auto.
+ intros.
destruct (n =? n0)%nat eqn:Heqn.
* admit.
* rewrite Nat.eqb_eq in Heqn; subst.
* admit.
+ exists iv, err, vR; intuition.
eapply eval_expr_ssa_extension; eauto.
......@@ -498,3 +502,4 @@ Proof.
rewrite !freeVars_toREval_toRExp_compat; auto.
*)
Abort.
*)
\ No newline at end of file
This diff is collapsed.
......@@ -100,31 +100,35 @@ Qed. *)
Inductive ssa (V:Type): (expr V) -> NatSet.t -> NatSet.t -> Prop :=
| ssaVar x inVars outVars:
(x inVars) ->
(NatSet.Equal inVars outVars) ->
(NatSet.Subset inVars outVars) ->
ssa (Var _ x) inVars outVars
| ssaConst m v inVars outVars:
(NatSet.Equal inVars outVars) ->
(NatSet.Subset 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 outVars1 outVars2:
| ssaBinop b e1 e2 inVars outVars1 outVars2 outVars3:
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:
NatSet.Subset (NatSet.union outVars1 outVars2) outVars3 ->
ssa (Binop b e1 e2) inVars outVars3
| ssaFma e1 e2 e3 inVars outVars1 outVars2 outVars3 outVars4:
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))
NatSet.Subset (NatSet.union outVars1 (NatSet.union outVars2 outVars3))
outVars4 ->
ssa (Fma e1 e2 e3) inVars outVars4
| ssaDowncast m e inVars outVars:
ssa e inVars outVars ->
ssa (Downcast m e) inVars outVars
| ssaLet m x e s inVars outVars1 outVars2:
| ssaLet m x e s inVars outVars1 outVars2 outVars3:
NatSet.mem x inVars = false ->
ssa e inVars outVars1 ->
ssa s (NatSet.add x inVars) outVars2 ->
ssa (Let m x e s) inVars (NatSet.union outVars1 outVars2)
NatSet.Subset (NatSet.union outVars1 outVars2) outVars3 ->
ssa (Let m x e s) inVars outVars3
(*
| ssaCond e1 e2 e3 inVars outVars:
ssa e1 inVars outVars ->
......@@ -156,26 +160,40 @@ Proof.
revert set_eq; revert inVars'.
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.
- hnf in *; intros.
apply H0. rewrite <- set_eq; auto.
- hnf in *. intros.
apply H. rewrite <- set_eq; auto.
- hnf in *. intros.
econstructor; eauto.
- hnf in *; intros. econstructor; eauto.
- hnf in *; intros. econstructor; eauto.
+ 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 ->
ssa f inVars outVars'.
Lemma ssa_outVars_extensible V (e:expr V):
forall inVars outVars1 outVars2,
ssa e inVars outVars1 ->
NatSet.Subset outVars1 outVars2 ->
ssa e inVars outVars2.
Proof.
intros ssa_f. induction ssa_f; constructor; auto.
induction e; intros * ssa_e subset_vars;
inversion ssa_e; subst; try constructor; try set_tac.
- eapply IHe; eauto.
- econstructor; try eauto. set_tac.
- econstructor; try eauto. set_tac.
destruct H; try auto. set_tac.
- eapply IHe; eauto.
- econstructor; try eauto.
+ rewrite <- NatSetProps.Dec.F.not_mem_iff; auto.
+ set_tac.
Qed.
**)
Ltac extended_ssa :=
eapply ssa_outVars_extensible; try eauto; set_tac.
Fixpoint validSSA (f:expr Q) (inVars:NatSet.t) :=
match f with
......@@ -195,21 +213,22 @@ Lemma validSSA_sound f inVars:
exists outVars, ssa f inVars outVars.
Proof.
induction f in inVars |- *; cbn; intros H.
- exists inVars. constructor; [ set_tac | auto using NatSetProps.equal_refl].
- exists inVars. constructor; auto using NatSetProps.equal_refl.
- exists inVars. constructor; [ set_tac | auto using NatSetProps.subset_refl].
- exists inVars. constructor; auto using NatSetProps.subset_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; auto.
econstructor; try eauto. set_tac.
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
edestruct IHf3 as [O3 ?]; eauto.
exists (O1 O2 O3).
constructor; auto.
econstructor; try eauto. set_tac.
destruct H2; try auto. set_tac.
- destruct (IHf _ H) as [O ?]. exists O.
now constructor.
- andb_to_prop H.
......@@ -217,7 +236,7 @@ Proof.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
exists (O1 O2).
constructor; auto.
econstructor; try eauto. set_tac.
(*
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
......@@ -388,6 +407,7 @@ Proof.
edestruct ssa_inv_let; eauto.
Qed.
(*
Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
(forall n, E1 n = E2 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