diff --git a/coq/Commands.v b/coq/Commands.v index f544f4a76cf419fb74f4732fdebcc5476e6fcc73..a6ef152043c254ba1864ca7957617d31f405192b 100644 --- a/coq/Commands.v +++ b/coq/Commands.v @@ -6,28 +6,16 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet. (** Next define what a program is. - Currently no loops, only conditionals and assignments - Final return statement + Currently no loops, or conditionals. + Only assignments and return statement **) Inductive cmd (V:Type) :Type := Let: nat -> exp V -> cmd V -> cmd V | Ret: exp V -> cmd V. -(*| Nop: cmd V. *) - -(* -UNUSED! - Small Step semantics for Daisy language -Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop := - let_s x e s E v eps: - eval_exp eps E e v -> - sstep (Let x e s) E eps s (updEnv x v E) - |ret_s e E v eps: - eval_exp eps E e v -> - sstep (Ret e) E eps (Nop R) (updEnv 0 v E). - *) (** - Analogously define Big Step semantics for the Daisy language + Define big step semantics for the Daisy language, terminating on a "returned" + result value **) Inductive bstep : cmd R -> env -> R -> R -> Prop := let_b x e s E v eps res: @@ -38,12 +26,19 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop := eval_exp eps E e v -> bstep (Ret e) E eps v. +(** + The free variables of a command are all used variables of expressions + without the let bound variables +**) Fixpoint freeVars V (f:cmd V) :NatSet.t := match f with - | Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g)) - | Ret e => Expressions.freeVars e + | Let x e g => NatSet.remove x (NatSet.union (usedVars e) (freeVars g)) + | Ret e => usedVars e end. +(** + The defined variables of a command are all let bound variables +**) Fixpoint definedVars V (f:cmd V) :NatSet.t := match f with | Let x _ g => NatSet.add x (definedVars g) diff --git a/coq/Expressions.v b/coq/Expressions.v index b00238d250c4d93ca0ce07c9e807c8a89292b6f3..ff66e04b31488a28768a557aaa0ca043bd2b14ba 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -129,8 +129,8 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop := Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t := match e with | Var _ x => NatSet.singleton x - | Unop u e1 => freeVars e1 - | Binop b e1 e2 => NatSet.union (freeVars e1) (freeVars e2) + | Unop u e1 => usedVars e1 + | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2) | _ => NatSet.empty end. diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v index f3342589900b1f8fb4e9c80544ee5ed0fc13d790..6bd099dd744c8433fe2f221dc0b1d7d443b28984 100644 --- a/coq/ssaPrgs.v +++ b/coq/ssaPrgs.v @@ -1,70 +1,45 @@ +(** + We define a pseudo SSA predicate. + The formalization is similar to the renamedApart property in the LVC framework by Schneider, Smolka and Hack + http://dblp.org/rec/conf/itp/SchneiderSH15 + Our predicate is not as fully fledged as theirs, but we especially borrow the idea of annotating + the program with the predicate with the set of free and defined variables +**) Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals. Require Import Coq.micromega.Psatz. Require Import Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs. Require Export Daisy.Commands. -Fixpoint validVars (V:Type) (f:exp V) Vs :bool := - match f with - | Const n => true - | Var _ v => NatSet.mem v Vs - | Unop o f1 => validVars f1 Vs - | Binop o f1 f2 => validVars f1 Vs && validVars f2 Vs - end. - -Lemma validVars_subset_freeVars T (e:exp T) V: - validVars e V = true-> - NatSet.Subset (Expressions.freeVars e) V. -Proof. - revert V; induction e; simpl; intros V valid_V; try auto. - - rewrite NatSet.mem_spec in valid_V. - hnf. intros; rewrite NatSet.singleton_spec in *; subst; auto. - - hnf; intros a in_empty; inversion in_empty. - - andb_to_prop valid_V. - hnf; intros a in_union. - rewrite NatSet.union_spec in in_union. - destruct in_union as [in_e1 | in_e2]. - + specialize (IHe1 V L a in_e1); auto. - + specialize (IHe2 V R a in_e2); auto. -Qed. - -Lemma validVars_add V (f:exp V) Vs n: - validVars f Vs = true -> - validVars f (NatSet.add n Vs) = true. +Lemma validVars_add V (e:exp V) Vs n: + NatSet.Subset (usedVars e) Vs -> + NatSet.Subset (usedVars e) (NatSet.add n Vs). Proof. - induction f; try auto. - - intros valid_var. unfold validVars in *; simpl in *. - rewrite NatSet.mem_spec in *. + induction e; try auto. + - intros valid_subset. + hnf. intros a in_singleton. + specialize (valid_subset a in_singleton). 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. - -Lemma validVars_valid_subset (V:Type) (e:exp V) inVars: - validVars e inVars = true -> - NatSet.Subset (Expressions.freeVars e) inVars. -Proof. - induction e; intros vars_valid; unfold validVars in *; simpl in *; try auto. - - rewrite NatSet.mem_spec in vars_valid. - hnf. intros; rewrite NatSet.singleton_spec in *; subst; auto. - - hnf; intros a in_empty; inversion in_empty. - - hnf; intros a in_union; rewrite NatSet.union_spec in in_union. - rewrite andb_true_iff in vars_valid. - destruct vars_valid. - destruct in_union as [in_e1 | in_e2]. - + apply IHe1; auto. - + apply IHe2; auto. + intros a in_empty. + inversion in_empty. + - simpl; intros in_vars. + intros a in_union. + rewrite NatSet.union_spec in in_union. + destruct in_union. + + apply IHe1; try auto. + hnf; intros. + apply in_vars. + rewrite NatSet.union_spec; auto. + + apply IHe2; try auto. + hnf; intros. + apply in_vars. + rewrite NatSet.union_spec; auto. Qed. Lemma validVars_non_stuck (e:exp Q) inVars E: - validVars e inVars = true -> - (forall v, NatSet.In v (Expressions.freeVars e) -> + NatSet.Subset (usedVars e) inVars -> + (forall v, NatSet.In v (usedVars e) -> exists r, E v = Some r)%R -> exists vR, eval_exp 0 E (toRExp e) vR. Proof. @@ -84,50 +59,38 @@ Proof. + exists (evalUnop Neg ve); constructor; auto. + exists (perturb (evalUnop Inv ve) 0); constructor; auto. rewrite Rabs_R0; lra. - - andb_to_prop vars_valid; simpl in *. + - repeat rewrite NatSet.subset_spec in *; simpl in *. assert (exists vR1, eval_exp 0 E (toRExp e1) vR1) as eval_e1_def. + eapply IHe1; eauto. - intros. - destruct (fVars_live v) as [vR E_def]; try eauto. - apply NatSet.union_spec; auto. - + assert (exists vR2, eval_exp 0 E (toRExp e2) vR2) as eval_e2_def. - * eapply IHe2; eauto. - intros. + * hnf; intros. + apply vars_valid. + rewrite NatSet.union_spec; auto. + * intros. destruct (fVars_live v) as [vR E_def]; try eauto. apply NatSet.union_spec; auto. + + assert (exists vR2, eval_exp 0 E (toRExp e2) vR2) as eval_e2_def. + * eapply IHe2; eauto. + { hnf; intros. + apply vars_valid. + rewrite NatSet.union_spec; auto. } + { intros. + destruct (fVars_live v) as [vR E_def]; try eauto. + apply NatSet.union_spec; auto. } * destruct eval_e1_def as [vR1 eval_e1_def]; destruct eval_e2_def as [vR2 eval_e2_def]. exists (perturb (evalBinop b vR1 vR2) 0); constructor; auto. rewrite Rabs_R0; lra. Qed. -Lemma validVars_equal_set V (e:exp V) vars vars': - NatSet.Equal vars vars' -> - validVars e vars = true -> - validVars e vars' = true. -Proof. - revert vars vars'. - induction e; intros vars vars' eq_set valid_vars; simpl in *; auto. - - rewrite NatSet.mem_spec in *. - rewrite <- eq_set; auto. - - eapply IHe; eauto. - - apply Is_true_eq_true. - apply andb_prop_intro. - andb_to_prop valid_vars. - split; apply Is_true_eq_left. - + eapply IHe1; eauto. - + eapply IHe2; eauto. -Qed. - Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop := ssaLet x e s inVars Vterm: - validVars e inVars = true-> + NatSet.Subset (usedVars e) inVars-> NatSet.mem x inVars = false -> ssaPrg s (NatSet.add x inVars) Vterm -> ssaPrg (Let x e s) inVars Vterm |ssaRet e inVars Vterm: - validVars e inVars = true -> - NatSet.equal inVars (NatSet.remove 0%nat Vterm) = true-> + NatSet.Subset (usedVars e) inVars -> + NatSet.Equal inVars Vterm -> ssaPrg (Ret e) inVars Vterm. Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars: @@ -135,8 +98,7 @@ Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars: NatSet.Subset (Commands.freeVars f) inVars. Proof. intros ssa_f; induction ssa_f. - - simpl in *. apply validVars_subset_freeVars in H. - hnf; intros a in_fVars. + - simpl in *. hnf; intros a in_fVars. rewrite NatSet.remove_spec, NatSet.union_spec in in_fVars. destruct in_fVars as [in_union not_eq]. destruct in_union; try auto. @@ -145,7 +107,6 @@ Proof. destruct IHssa_f; subst; try auto. exfalso; apply not_eq; auto. - hnf; intros. - apply validVars_subset_freeVars in H. simpl in H1. apply H; auto. Qed. @@ -159,8 +120,7 @@ Proof. revert set_eq; revert inVars'. induction ssa_f. - constructor. - + eapply validVars_equal_set; eauto. - symmetry; auto. + + rewrite set_eq; auto. + case_eq (NatSet.mem x inVars'); intros case_mem; try auto. rewrite NatSet.mem_spec in case_mem. rewrite set_eq in case_mem. @@ -169,20 +129,15 @@ Proof. + apply IHssa_f; auto. apply NatSetProps.Dec.F.add_m; auto. - constructor. - + eapply validVars_equal_set; eauto. - symmetry; auto. - + rewrite NatSet.equal_spec in *. - hnf. intros a; split. - * intros in_primed. - rewrite <- H0. rewrite <- set_eq. auto. - * intros in_rem. rewrite set_eq. rewrite H0; auto. + + rewrite set_eq; auto. + + rewrite set_eq; auto. Qed. Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) := match f with |Let x e g => - andb (andb (negb (NatSet.mem x inVars)) (validVars e inVars)) (validSSA g (NatSet.add x inVars)) - |Ret e => validVars e inVars && (negb (NatSet.mem 0%nat inVars)) + andb (andb (negb (NatSet.mem x inVars)) (NatSet.subset (usedVars e) inVars)) (validSSA g (NatSet.add x inVars)) + |Ret e => NatSet.subset (usedVars e) inVars end. Lemma validSSA_sound f inVars: @@ -197,32 +152,14 @@ Proof. destruct IHf as [outVars IHf]. exists outVars. constructor; eauto. - rewrite negb_true_iff in L0. auto. + + rewrite <- NatSet.subset_spec; auto. + + rewrite negb_true_iff in L0. auto. - intros inVars validSSA_ret. simpl in *. - exists (NatSet.add 0%nat inVars). - andb_to_prop validSSA_ret. + exists inVars. 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. + + rewrite <- NatSet.subset_spec; auto. + + hnf; intros; split; auto. Qed. Lemma ssa_shadowing_free x y v v' e f inVars outVars E: @@ -301,7 +238,7 @@ Proof. Qed. Lemma dummy_bind_ok e v x v' inVars E: - validVars e inVars = true -> + NatSet.Subset (usedVars e) inVars -> NatSet.mem x inVars = false -> eval_exp 0 E (toRExp e) v -> eval_exp 0 (updEnv x v' E) (toRExp e) v. @@ -315,7 +252,13 @@ Proof. 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. + hnf in valid_vars. + assert (NatSet.mem x (NatSet.singleton x) = true) + as in_singleton by (rewrite NatSet.mem_spec, NatSet.singleton_spec; auto). + rewrite NatSet.mem_spec in *. + specialize (valid_vars x in_singleton). + rewrite <- NatSet.mem_spec in valid_vars. + rewrite valid_vars in *; congruence. + econstructor. rewrite H; auto. - inversion eval_e; subst; constructor; auto. @@ -323,14 +266,15 @@ Proof. + 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. + hnf; intros a in_e1. + apply valid_vars; + rewrite NatSet.union_spec; auto. + eapply IHe2; eauto. - apply Is_true_eq_true; auto. + hnf; intros a in_e2. + apply valid_vars; + rewrite NatSet.union_spec; auto. Qed. Fixpoint exp_subst (e:exp Q) x e_new := @@ -397,7 +341,7 @@ Fixpoint map_subst (f:cmd Q) x e := Lemma stepwise_substitution x e v f E vR inVars outVars: ssaPrg f inVars outVars -> NatSet.In x inVars -> - validVars e inVars = true -> + NatSet.Subset (usedVars e) inVars -> eval_exp 0%R E (toRExp e) v -> bstep (toRCmd f) (updEnv x v E) 0%R vR <-> bstep (toRCmd (map_subst f x e)) E 0%R vR. diff --git a/hol4/Infra/ExpressionAbbrevsScript.sml b/hol4/ExpressionAbbrevsScript.sml similarity index 100% rename from hol4/Infra/ExpressionAbbrevsScript.sml rename to hol4/ExpressionAbbrevsScript.sml