Skip to content

GitLab

Commit 7f633e09 authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Add ssa soundness checker

parent 2e65b5a9
Hide whitespace changes
Inline Side-by-side
Showing with 410 additions and 27 deletions
coq/CertificateChecker.v
View file @ 7f633e09
......@@ -53,13 +53,13 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :
(validErrorboundCmd f absenv).
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (VarEnv1 VarEnv2 ParamEnv:env) outVars envR envF,
forall (VarEnv1 VarEnv2 ParamEnv:env) outVars vR vF,
approxEnv VarEnv1 absenv VarEnv2 ->
ssaPrg Q f NatSet.empty outVars ->
bstep (toRCmd f) VarEnv1 ParamEnv P 0 (Nop R) envR ->
bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R machineEpsilon) (Nop R) envF ->
bstep (toRCmd f) VarEnv1 ParamEnv P 0 (Nop R) vR ->
bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R machineEpsilon) (Nop R) vF ->
CertificateCheckerCmd f absenv P = true ->
(Rabs (envR 0%nat - envF 0%nat) <= Q2R (snd (absenv (Var Q 0))))%R.
(Rabs (vR - vF) <= Q2R (snd (absenv (Var Q 0))))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......
coq/Commands.v
View file @ 7f633e09
(**
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
**)
Require Import Coq.Reals.Reals.
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
(**
Next define what a program is.
......@@ -14,7 +14,7 @@ Let: nat -> exp V -> cmd V -> cmd V
| Nop: cmd V.
(**
Small Step semantics for Daisy language, parametric by evaluation function.
Small Step semantics for Daisy language
**)
Inductive sstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
let_s x e s VarEnv ParamEnv P v eps:
......@@ -25,14 +25,50 @@ Inductive sstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
sstep (Ret R e) VarEnv ParamEnv P eps (Nop R) (updEnv 0 v VarEnv).
(**
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function
Analogously define Big Step semantics for the Daisy language
**)
Inductive bstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
let_b x e s s' VarEnv ParamEnv P v eps VarEnv2:
Inductive bstep : cmd R -> env -> env -> precond -> R -> cmd R -> R -> Prop :=
let_b x e s s' VarEnv ParamEnv P v eps res:
eval_exp eps VarEnv ParamEnv P e v ->
bstep s (updEnv x v VarEnv) ParamEnv P eps s' VarEnv2 ->
bstep (Let R x e s) VarEnv ParamEnv P eps s' VarEnv2
bstep s (updEnv x v VarEnv) ParamEnv P eps s' res ->
bstep (Let R x e s) VarEnv ParamEnv P eps s' res
|ret_b e VarEnv ParamEnv P v eps:
eval_exp eps VarEnv ParamEnv P e v ->
bstep (Ret R e) VarEnv ParamEnv P eps (Nop R) (updEnv 0 v VarEnv).
\ No newline at end of file
bstep (Ret R e) VarEnv ParamEnv P eps (Nop R) v.
Fixpoint substitute_exp (v:nat) (e:exp Q) (e_old:exp Q) :=
match e_old with
|Var _ v_old => if (v =? v_old) then e else Var Q v_old
|Unop op e' => Unop op (substitute_exp v e e')
|Binop op e1 e2 => Binop op (substitute_exp v e e1) (substitute_exp v e e2)
|e => e
end.
Fixpoint substitute (v:nat) (e:exp Q) (f:cmd Q) :=
match f with
|Let _ x e_x g =>
let new_e := substitute_exp v e e_x in
Let Q x new_e (substitute v e g)
|Ret _ e_ret => Ret Q (substitute_exp v e e_ret)
|Nop _ => Nop Q
end.
Fixpoint expand_lets (f:cmd Q) (fuel:nat) :option (cmd Q):=
match fuel with
|0%nat => Some f
|S fuel' =>
match f with
|Let _ x e g =>
(expand_lets (substitute x e g) fuel')
|Ret _ e => Some (Ret Q e)
|Nop _ => None
end
end.
Fixpoint count_lets (f:cmd Q) :nat :=
match f with
|Let _ x e g => S (count_lets g)
| _ => 0%nat
end.
Definition expand (f:cmd Q) := expand_lets f (count_lets f).
\ No newline at end of file
coq/ErrorValidation.v
View file @ 7f633e09
......@@ -1886,17 +1886,17 @@ Proof.
Qed.
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall VarEnv1 VarEnv2 ParamEnv inVars outVars envR envF elo ehi err P,
forall VarEnv1 VarEnv2 ParamEnv inVars outVars vR vF elo ehi err P,
approxEnv VarEnv1 absenv VarEnv2 ->
ssaPrg Q f inVars outVars ->
bstep (toRCmd f) VarEnv1 ParamEnv P 0%R (Nop R) envR ->
bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R RationalSimps.machineEpsilon) (Nop R) envF ->
bstep (toRCmd f) VarEnv1 ParamEnv P 0%R (Nop R) vR ->
bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R RationalSimps.machineEpsilon) (Nop R) vF ->
validErrorboundCmd f absenv = true ->
validIntervalboundsCmd f absenv P inVars = true ->
(forall v : NatSet.elt, NatSet.mem v inVars = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv1 v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
absenv (Var Q 0%nat) = ((elo,ehi),err) ->
(Rabs ((envR 0%nat) - (envF 0%nat)) <= (Q2R err))%R.
(Rabs (vR - vF) <= (Q2R err))%R.
Proof.
induction f;
intros VarEnv1 VarEnv2 ParamEnv inVars outVars envR envF elo ehi err P;
......
coq/IntervalValidation.v
View file @ 7f633e09
......@@ -458,14 +458,14 @@ Proof.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
forall VarEnv ParamEnv envR inVars outVars elo ehi err P,
forall VarEnv ParamEnv vR inVars outVars elo ehi err P,
ssaPrg Q f inVars outVars ->
bstep (toRCmd f) VarEnv ParamEnv P 0%R (Nop R) envR ->
bstep (toRCmd f) VarEnv ParamEnv P 0%R (Nop R) vR ->
(forall v, NatSet.mem v inVars = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
validIntervalboundsCmd f absenv P inVars = true ->
absenv (Var Q 0%nat) = ((elo,ehi),err) ->
(Q2R elo <= envR (0%nat) <= Q2R ehi)%R.
(Q2R elo <= vR <= Q2R ehi)%R.
Proof.
induction f;
intros VarEnv ParamEnv envR inVars outVars elo ehi err P
......@@ -501,9 +501,7 @@ Proof.
andb_to_prop valid_bounds_f.
inversion eval_f; subst.
unfold updEnv.
assert (0 =? 0 = true) as refl0 by (apply Nat.eqb_refl).
rewrite refl0.
assert (Q2R (fst (fst (absenv e))) <= v <= Q2R (snd (fst (absenv e))))%R
assert (Q2R (fst (fst (absenv e))) <= envR <= Q2R (snd (fst (absenv e))))%R
by (eapply validIntervalbounds_sound; eauto).
rename L0 into eq_lo;
rename R0 into eq_hi.
......
coq/ssaPrgs.v
View file @ 7f633e09
Require Import Coq.MSets.MSets Coq.Arith.PeanoNat.
Require Import Coq.MSets.MSets Coq.Arith.PeanoNat Coq.QArith.QArith Coq.Reals.Reals.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Export Daisy.Commands.
(**
......@@ -40,7 +41,25 @@ Fixpoint validVars (V:Type) (f:exp V) Vs :bool :=
| Binop o f1 f2 => validVars V f1 Vs && validVars V f2 Vs
end.
(* TODO: This still allows overwriting of return value *)
Lemma validVars_add V f Vs n:
validVars V f Vs = true ->
validVars V f (NatSet.add n Vs) = true.
Proof.
induction f; try auto.
- intros valid_var. unfold validVars in *; simpl in *.
rewrite NatSet.mem_spec in *.
rewrite NatSet.add_spec; right; auto.
- intros vars_binop.
simpl in *.
apply Is_true_eq_left in vars_binop.
apply Is_true_eq_true.
apply andb_prop_intro.
apply andb_prop_elim in vars_binop.
destruct vars_binop; split; apply Is_true_eq_left.
+ apply IHf1. apply Is_true_eq_true; auto.
+ apply IHf2. apply Is_true_eq_true; auto.
Qed.
Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
ssaLet x e s inVars Vterm:
validVars V e inVars = true->
......@@ -48,5 +67,335 @@ Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
ssaPrg V s (NatSet.add x inVars) Vterm ->
ssaPrg V (Let V x e s) inVars Vterm
|ssaRet e inVars Vterm:
NatSet.equal inVars Vterm = true->
ssaPrg V (Ret V e) inVars Vterm.
\ No newline at end of file
validVars V e inVars = true ->
NatSet.equal inVars (NatSet.remove 0%nat Vterm) = true->
ssaPrg V (Ret V e) inVars Vterm.
Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
match f with
|Let _ x e g =>
andb (andb (negb (NatSet.mem x inVars)) (validVars Q e inVars)) (validSSA g (NatSet.add x inVars))
|Ret _ e => validVars Q e inVars && (negb (NatSet.mem 0%nat inVars))
|Nop _ => false
end.
Lemma validSSA_sound f inVars:
validSSA f inVars = true ->
exists outVars, ssaPrg Q f inVars outVars.
Proof.
revert inVars; induction f.
- intros inVars validSSA_let.
simpl in *.
andb_to_prop validSSA_let.
specialize (IHf (NatSet.add n inVars) R).
destruct IHf as [outVars IHf].
exists outVars.
constructor; eauto.
rewrite negb_true_iff in L0. auto.
- intros inVars validSSA_ret.
simpl in *.
exists (NatSet.add 0%nat inVars).
andb_to_prop validSSA_ret.
constructor; auto.
rewrite negb_true_iff in R.
hnf in R.
rewrite NatSet.equal_spec.
hnf.
intros a.
rewrite NatSet.remove_spec, NatSet.add_spec.
split.
+ intros in_inVars.
case_eq (a =? 0%nat).
* intros a_zero.
rewrite Nat.eqb_eq in a_zero.
rewrite a_zero in in_inVars.
rewrite <- NatSet.mem_spec in in_inVars.
rewrite in_inVars in R.
inversion R.
* intros a_neq_zero. apply beq_nat_false in a_neq_zero.
split; auto.
+ intros in_add_rem.
destruct in_add_rem as [ [a_zero | a_inVars] a_neq_zero]; try auto.
exfalso; eauto.
- intros inVars validSSA_nop. simpl in *.
inversion validSSA_nop.
Qed.
Lemma ssa_shadowing_free x y v v' e f inVars outVars VarEnv ParamEnv P:
ssaPrg Q (Let Q x e f) inVars outVars ->
NatSet.In y inVars ->
eval_exp 0 VarEnv ParamEnv P (toRExp e) v ->
forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
Proof.
intros ssa_let y_free eval_e.
inversion ssa_let; subst.
intros E n; unfold updEnv.
case_eq (n =? x).
- intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
case_eq (n =? y); try auto.
intros n_eq_y.
rewrite Nat.eqb_eq in n_eq_y.
subst.
rewrite n_eq_y in H5.
rewrite <- NatSet.mem_spec in y_free.
rewrite y_free in H5. inversion H5.
- intros n_neq_x.
case_eq (n =? y); auto.
Qed.
Lemma shadowing_free_rewriting_exp e v VarEnv1 VarEnv2 ParamEnv P:
(forall n, VarEnv1 n = VarEnv2 n) ->
eval_exp 0 VarEnv1 ParamEnv P e v <->
eval_exp 0 VarEnv2 ParamEnv P e v.
Proof.
revert v VarEnv1 VarEnv2 ParamEnv P.
induction e; intros v' VarEnv1 VarEnv2 ParamEnv P agree_on_vars.
- split; intros eval_Var.
+ inversion eval_Var; subst.
rewrite agree_on_vars. constructor.
+ inversion eval_Var; subst.
rewrite <- agree_on_vars; constructor.
- split; intros eval_Param; inversion eval_Param; subst.
+ econstructor.
apply H0. apply H1. apply H2. auto.
+ econstructor.
apply H0. apply H1. apply H2. auto.
- split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
- split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
+ erewrite IHe; eauto.
+ erewrite IHe; eauto.
+ erewrite <- IHe; eauto.
+ erewrite <- IHe; eauto.
- split; intros eval_Binop; inversion eval_Binop; subst; econstructor; try auto;
try (erewrite IHe1; eauto);
try (erewrite IHe2; eauto).
Qed.
Lemma shadowing_free_rewriting_cmd f VarEnv1 VarEnv2 ParamEnv P vR:
(forall n, VarEnv1 n = VarEnv2 n) ->
bstep f VarEnv1 ParamEnv P 0 (Nop R) vR <->
bstep f VarEnv2 ParamEnv P 0 (Nop R) vR.
Proof.
revert VarEnv1 VarEnv2 ParamEnv P vR.
induction f; intros VarEnv1 VarEnv2 ParamEnv P vR agree_on_vars.
- split; intros bstep_Let; inversion bstep_Let; subst.
+ erewrite shadowing_free_rewriting_exp in H8; auto.
econstructor; eauto.
rewrite <- IHf.
apply H9.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
+ erewrite <- shadowing_free_rewriting_exp in H8; auto.
econstructor; eauto.
rewrite IHf.
apply H9.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
- split; intros bstep_Ret; inversion bstep_Ret; subst.
+ erewrite shadowing_free_rewriting_exp in H0; auto.
constructor; auto.
+ erewrite <- shadowing_free_rewriting_exp in H0; auto.
constructor; auto.
- split; intros bstep_Nop; inversion bstep_Nop.
Qed.
Lemma dummy_bind_ok e v x v' inVars VarEnv ParamEnv P:
validVars Q e inVars = true ->
NatSet.mem x inVars = false ->
eval_exp 0 VarEnv ParamEnv P (toRExp e) v ->
eval_exp 0 (updEnv x v' VarEnv) ParamEnv P (toRExp e) v.
Proof.
revert v x v' inVars VarEnv ParamEnv P.
induction e; intros v1 x v2 inVars VarEnv ParamEnv P valid_vars x_not_free eval_e.
- inversion eval_e; subst.
assert ((updEnv x v2 VarEnv) n = VarEnv n).
+ unfold updEnv.
case_eq (n =? x); try auto.
intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
subst; simpl in *.
rewrite x_not_free in valid_vars; inversion valid_vars.
+ rewrite <- H; constructor.
- inversion eval_e; subst; econstructor.
apply H0. apply H1. apply H2. auto.
- inversion eval_e; subst; constructor; auto.
- inversion eval_e; subst; constructor; auto.
+ eapply IHe; eauto.
+ eapply IHe; eauto.
- simpl in valid_vars.
apply Is_true_eq_left in valid_vars.
apply andb_prop_elim in valid_vars.
destruct valid_vars.
inversion eval_e; subst; constructor; auto.
+ eapply IHe1; eauto.
apply Is_true_eq_true; auto.
+ eapply IHe2; eauto.
apply Is_true_eq_true; auto.
Qed.
Fixpoint exp_subst (e:exp Q) x e_new :=
match e with
|Var _ v => if v =? x then e_new else Var Q v
|Unop op e1 => Unop op (exp_subst e1 x e_new)
|Binop op e1 e2 => Binop op (exp_subst e1 x e_new) (exp_subst e2 x e_new)
| e => e
end.
Lemma exp_subst_correct e e_sub VarEnv ParamEnv P x v v_res:
eval_exp (0%R) VarEnv ParamEnv P (toRExp e_sub) v ->
eval_exp (0%R) (updEnv x v VarEnv) ParamEnv P (toRExp e) v_res <->
eval_exp (0%R) VarEnv ParamEnv P (toRExp (exp_subst e x e_sub)) v_res.
Proof.
intros eval_e.
revert v_res.
induction e.
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ unfold updEnv in eval_upd. simpl in *.
inversion eval_upd; subst.
case_eq (n =? x); intros; try auto.
constructor.
+ simpl in eval_subst.
case_eq (n =? x); intros n_eq_case;
rewrite n_eq_case in eval_subst.
* simpl.
assert (v_res = (updEnv x v VarEnv) n).
{ unfold updEnv.
rewrite n_eq_case.
eapply meps_0_deterministic; eauto. }
{ rewrite H. constructor. }
* simpl. inversion eval_subst; subst.
assert (VarEnv n = updEnv x v VarEnv n).
{ unfold updEnv; rewrite n_eq_case; reflexivity. }
{ rewrite H; constructor. }
- intros v_res; split; simpl; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; subst. eapply Param_acc.
assumption.
apply H1.
apply H2.
assumption.
+ inversion eval_subst; subst.
eapply Param_acc.
assumption.
apply H1.
apply H2.
assumption.
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; auto.
+ inversion eval_subst; constructor; auto.
- split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; try auto.
* rewrite <- IHe. assumption.
* rewrite <- IHe. assumption.
+ inversion eval_subst; constructor; try auto.
* rewrite IHe; assumption.
* rewrite IHe; assumption.
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; try auto.
* rewrite <- IHe1. assumption.
* rewrite <- IHe2. assumption.
+ inversion eval_subst; constructor; try auto.
* rewrite IHe1; assumption.
* rewrite IHe2; assumption.
Qed.
Fixpoint map_subst (f:cmd Q) x e :=
match f with
|Let _ y e_y g => Let Q y (exp_subst e_y x e) (map_subst g x e)
|Ret _ e_r => Ret Q (exp_subst e_r x e)
|Nop _ => Nop Q
end.
Lemma stepwise_substitution x e v f VarEnv ParamEnv P vR inVars outVars:
ssaPrg Q f inVars outVars ->
NatSet.In x inVars ->
validVars Q e inVars = true ->
eval_exp 0%R VarEnv ParamEnv P (toRExp e) v ->
bstep (toRCmd f) (updEnv x v VarEnv) ParamEnv P 0%R (Nop R) vR <->
bstep (toRCmd (map_subst f x e)) VarEnv ParamEnv P 0%R (Nop R) vR.
Proof.
revert VarEnv ParamEnv e x P vR inVars outVars.
induction f; intros VarEnv ParamEnv e0 x P vR inVars outVars ssa_f x_free valid_vars_e eval_e.
- split; [ intros bstep_let | intros bstep_subst].
+ inversion bstep_let; subst.
simpl in *.
inversion ssa_f; subst.
assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var).
* eapply ssa_shadowing_free.
apply ssa_f.
apply x_free.
apply H8.
* rewrite (shadowing_free_rewriting_cmd _ _ _ _ _ _ (H VarEnv)) in H9.
econstructor; auto.
rewrite <- exp_subst_correct; eauto.
rewrite <- IHf; eauto.
rewrite NatSet.add_spec.
right; auto.
apply validVars_add; auto.
eapply dummy_bind_ok; eauto.
+ inversion bstep_subst; subst.
simpl in *.
inversion ssa_f; subst.
econstructor.
rewrite exp_subst_correct; eauto.
rewrite <- IHf in H9; eauto.
rewrite <- shadowing_free_rewriting_cmd in H9; eauto.
eapply ssa_shadowing_free; eauto.
rewrite <- exp_subst_correct in H8; eauto.
rewrite NatSet.add_spec.
right; auto.
apply validVars_add; auto.
eapply dummy_bind_ok; eauto.
- split; [intros bstep_let | intros bstep_subst].
+ inversion bstep_let; subst.
simpl in *.
rewrite exp_subst_correct in H0; eauto.
constructor. assumption.
+ inversion bstep_subst; subst.
simpl in *.
rewrite <- exp_subst_correct in H0; eauto.
constructor; assumption.
- split; intros step; inversion step.
Qed.
Fixpoint let_subst (f:cmd Q) :=
match f with
| Let _ x e1 g =>
match (let_subst g) with
|Some e' => Some (exp_subst e' x e1)
|None => None
end
| Ret _ e1 => Some e1
| Nop _ => None
end.
Theorem let_free_form f VarEnv ParamEnv P vR inVars outVars e:
ssaPrg Q f inVars outVars ->
bstep (toRCmd f) VarEnv ParamEnv P 0 (Nop R) vR ->
let_subst f = Some e ->
bstep (toRCmd (Ret Q e)) VarEnv ParamEnv P 0 (Nop R) vR.
Proof.
revert VarEnv ParamEnv P vR inVars outVars e;
induction f;
intros VarEnv ParamEnv P vR inVars outVars e_subst ssa_f bstep_f subst_step.
- simpl.
inversion bstep_f; subst.
inversion ssa_f; subst.
simpl in subst_step.
case_eq (let_subst f).
+ intros f_subst subst_f_eq.
specialize (IHf (updEnv n v VarEnv) ParamEnv P vR (NatSet.add n inVars) outVars f_subst H6 H9 subst_f_eq).
rewrite subst_f_eq in subst_step.
inversion IHf; subst.
constructor.
inversion subst_step.
subst.
rewrite <- exp_subst_correct; eauto.
+ intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step.
- inversion bstep_f; subst.
constructor.
simpl in *.
inversion subst_step; subst.
assumption.
- simpl in *; inversion subst_step.
Qed.
\ No newline at end of file
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