Commit 56829d57 authored by Joachim Bard's avatar Joachim Bard

using only preVars for validSSA in certificate checker

parent b9ac30e9
...@@ -82,72 +82,11 @@ Proof. ...@@ -82,72 +82,11 @@ Proof.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto. exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed. Qed.
Lemma validSSA_eq_set s s' f :
NatSet.Equal s' s -> validSSA f s = true -> validSSA f s' = true.
Proof.
induction f in s, s' |- *; intros sub ?.
- andb_to_prop H.
apply andb_true_iff; split.
apply andb_true_iff; split.
+ apply negb_true_iff.
apply negb_true_iff in L0.
apply NatSetProps.FM.not_mem_iff.
apply NatSetProps.FM.not_mem_iff in L0.
apply NatSetProps.subset_equal in sub.
intros ?. auto.
+ apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in R0.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
set_tac.
+ fold validSSA in *.
eapply IHf; eauto.
assert (NatSet.Subset s' s) by now apply NatSetProps.subset_equal in sub.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
split; set_tac; intuition.
- apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in H.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
set_tac.
Qed.
Lemma validSSA_downward_closed s f vars :
NatSet.Subset (freeVars f) vars ->
validSSA f (vars s) = true ->
validSSA f vars = true.
Proof.
induction f in vars |- *.
- intros sub H. andb_to_prop H.
apply andb_true_intro; split.
apply andb_true_intro; split.
+ apply negb_true_iff.
apply NatSetProps.FM.not_mem_iff.
apply negb_true_iff in L0.
apply NatSetProps.FM.not_mem_iff in L0.
intros ?. apply L0. set_tac.
+ apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in R0.
set_tac. set_tac.
split; auto.
apply negb_true_iff in L0.
apply NatSetProps.FM.not_mem_iff in L0.
intros ?. subst. apply L0. set_tac.
+ fold validSSA in *. apply IHf.
* set_tac.
destruct (dec_eq_nat a n); [now left | right; set_tac].
* eapply validSSA_eq_set; eauto.
split; set_tac; intuition.
- intros ? _.
now apply NatSetProps.FM.subset_1.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: FloverMap.t intv) Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: FloverMap.t intv)
(Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars := (Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
match getValidMapCmd defVars f (FloverMap.empty mType) with match getValidMapCmd defVars f (FloverMap.empty mType) with
| Succes Gamma => | Succes Gamma =>
if (validSSA f (freeVars f preVars P)) if (validSSA f (preVars P))
then then
if (RangeValidatorCmd f absenv P Qmap NatSet.empty) && if (RangeValidatorCmd f absenv P Qmap NatSet.empty) &&
FPRangeValidatorCmd f absenv Gamma NatSet.empty FPRangeValidatorCmd f absenv Gamma NatSet.empty
...@@ -188,13 +127,14 @@ Proof. ...@@ -188,13 +127,14 @@ Proof.
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
repeat rewrite <- andb_lazy_alt in certificate_valid. repeat rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid. andb_to_prop certificate_valid.
pose proof (validSSA_checks_freeVars _ _ L) as sub.
assert (validSSA f (freeVars f) = true) as ssa_valid assert (validSSA f (freeVars f) = true) as ssa_valid
by (eapply validSSA_downward_closed; eauto; set_tac). by (eapply validSSA_downward_closed; eauto; set_tac).
apply validSSA_sound in ssa_valid as [outVars_small ssa_f_small]. apply validSSA_sound in ssa_valid as [outVars_small ssa_f_small].
apply validSSA_sound in L. apply validSSA_sound in L.
destruct L as [outVars ssa_f]. destruct L as [outVars ssa_f].
assert (ssa f ((freeVars f preVars P) NatSet.empty) outVars) as ssa_valid. assert (ssa f (preVars P NatSet.empty) outVars) as ssa_valid.
{ eapply ssa_equal_set; try eauto. { eapply ssa_equal_set; eauto.
apply NatSetProps.empty_union_2. apply NatSetProps.empty_union_2.
apply NatSet.empty_spec. } apply NatSet.empty_spec. }
rename R into validFPRanges. rename R into validFPRanges.
...@@ -204,8 +144,7 @@ Proof. ...@@ -204,8 +144,7 @@ Proof.
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f)) assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac. as freeVars_contained by set_tac.
assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f. assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply (RangeValidatorCmd_sound _ (fVars:=freeVars f preVars P)); eauto; set_tac. { eapply (RangeValidatorCmd_sound _ (fVars:=preVars P)); eauto; intuition.
(* unfold RangeValidatorCmd. *)
unfold affine_dVars_range_valid; intros. unfold affine_dVars_range_valid; intros.
set_tac. } set_tac. }
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single. pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
......
...@@ -178,6 +178,81 @@ Proof. ...@@ -178,6 +178,81 @@ Proof.
+ hnf; intros; split; auto. + hnf; intros; split; auto.
Qed. Qed.
Lemma validSSA_checks_freeVars f S :
validSSA f S = true ->
NatSet.Subset (freeVars f) S.
Proof.
induction f in S |- *; intros * validSSA_true; cbn in *.
- andb_to_prop validSSA_true.
pose proof (IHf _ R).
intros x; set_tac.
apply NatSetProps.FM.subset_2 in R0.
intros [[?|?] ?]; try now set_tac.
pose proof (H _ H0).
clear R0. set_tac. intuition.
- now apply NatSetProps.FM.subset_2.
Qed.
Lemma validSSA_eq_set s s' f :
NatSet.Equal s' s -> validSSA f s = true -> validSSA f s' = true.
Proof.
induction f in s, s' |- *; intros sub ?.
- andb_to_prop H.
apply andb_true_iff; split.
apply andb_true_iff; split.
+ apply negb_true_iff.
apply negb_true_iff in L0.
apply NatSetProps.FM.not_mem_iff.
apply NatSetProps.FM.not_mem_iff in L0.
apply NatSetProps.subset_equal in sub.
intros ?. auto.
+ apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in R0.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
set_tac.
+ fold validSSA in *.
eapply IHf; eauto.
assert (NatSet.Subset s' s) by now apply NatSetProps.subset_equal in sub.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
split; set_tac; intuition.
- apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in H.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
set_tac.
Qed.
Lemma validSSA_downward_closed S S' f :
NatSet.Subset (freeVars f) S' ->
NatSet.Subset S' S ->
validSSA f S = true ->
validSSA f S' = true.
Proof.
induction f in S, S' |- *.
- intros sub1 sub2 H. andb_to_prop H.
apply andb_true_intro; split.
apply andb_true_intro; split.
+ apply negb_true_iff.
apply NatSetProps.FM.not_mem_iff.
apply negb_true_iff in L0.
apply NatSetProps.FM.not_mem_iff in L0.
intros ?. apply L0. now apply sub2.
+ apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in R0.
set_tac. set_tac.
split; auto.
apply negb_true_iff in L0.
apply NatSetProps.FM.not_mem_iff in L0.
intros ?. subst. apply L0. set_tac.
+ fold validSSA in *. eapply IHf; eauto.
* set_tac.
destruct (dec_eq_nat a n); [now left | right; set_tac].
* set_tac. intuition.
- intros. now apply NatSetProps.FM.subset_1.
Qed.
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars: Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars:
ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars -> ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars ->
NatSet.In y inVars -> NatSet.In y inVars ->
......
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