diff --git a/compiler/src/compiler/DeadAssignment.v b/compiler/src/compiler/DeadAssignment.v new file mode 100644 index 000000000..f1cc861e5 --- /dev/null +++ b/compiler/src/compiler/DeadAssignment.v @@ -0,0 +1,1891 @@ +Require Import compiler.util.Common. +Require Import compiler.FlatImp. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.Syntax. +Require Import coqutil.Tactics.fwd. +Require Import String. +Require Import compiler.DeadAssignmentDef. +Require Import compiler.DeadAssignmentHelper. +Require Import bedrock2.MetricLogging. +Require Import coqutil.Datatypes.PropSet. + +Local Notation var := String.string (only parsing). + +Section WithArguments. + Context {width : Z}. + Context {BW : Bitwidth.Bitwidth width }. + Context {word : word width } {word_ok : word.ok word}. + Context {env : map.map string (list var * list var * stmt var) } {env_ok : map.ok env}. + Context {mem : map.map word (Init.Byte.byte : Type) } {mem_ok: map.ok mem}. + Context {locals : map.map string word } {locals_ok: map.ok locals}. + Context {ext_spec : Semantics.ExtSpec} {ext_spec_ok: Semantics.ext_spec.ok ext_spec}. + + Local Hint Constructors exec: core. + Local Create HintDb set_hints. + Local Hint Resolve + subset_diff + in_singleton + subset_union_rr + subset_union_rl + subset_ref : set_hints. + Local Hint Rewrite ListSet.of_list_list_union : set_hints. + Local Hint Rewrite of_list_list_diff: set_hints. + Local Create HintDb agree_on_hints. + Hint Resolve + agree_on_getmany + agree_on_subset : agree_on_hints. + + (* Ideally `autorewrite* with set_hints` + should be able to replace + + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + + But currently it doesn't. *) + + (* + Currently this tactic + match goal with + | |- subset ?x (union ?x ?y) => + eauto with set_hints + end. + doesn't solve it, although this tactic clears the goal: + + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + *) + + + + Definition compile_post used_after (postH : Semantics.trace -> mem -> locals -> MetricLog -> Prop) : (Semantics.trace -> mem -> locals -> MetricLog -> Prop) := + (fun t' m' lL' mcL' => + exists lH' mcH', + map.agree_on (PropSet.of_list used_after) lH' lL' + /\ postH t' m' lH' mcH' ). + + + Lemma deadassignment_correct_aux: + forall eH eL, + deadassignment_functions eH = Success eL -> + forall sH t m mcH lH postH, + exec eH sH t m lH mcH postH -> + forall used_after lL mcL, + map.agree_on (of_list (live (deadAssignment used_after sH) used_after)) lH lL + -> exec eL (deadAssignment used_after sH) t m lL mcL (compile_post used_after postH). + Proof. + induction 2. + - simpl. + intros. + eapply @exec.interact; fwd. + + match goal with + | H: map.split ?m _ _ |- map.split m _ _ => eapply H + end. + + match goal with + | H1: map.getmany_of_list ?l ?argvars = Some ?argvals, + H2: map.agree_on _ ?l ?lL + |- map.getmany_of_list ?lL ?argvars = Some ?y => + cut (map.getmany_of_list l argvars = map.getmany_of_list lL argvars); + intros; + match goal with + | H: map.getmany_of_list l argvars + = map.getmany_of_list lL argvars + |- map.getmany_of_list lL argvars = Some _ => + rewrite <- H; eassumption + | |- map.getmany_of_list l argvars + = map.getmany_of_list lL argvars => + eapply agree_on_getmany; eapply agree_on_subset; + [ eapply H2 | ] + end + end. + + repeat match goal with + | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union + | |- context[ListSet.list_diff] => rewrite of_list_list_diff + end. + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + + match goal with + | |- ext_spec _ _ _ _ _ => eassumption + end. + + intros. + match goal with + | H: outcome ?mReceive ?resvals, + H1: forall mReceive resvals, + outcome mReceive resvals -> _ |- _ => + apply H1 in H; + repeat match goal with + | H: exists l, _ |- _ => destr H + | H: _ /\ _ |- _ => destr H + end + end. + match goal with + | H: map.putmany_of_list_zip ?resvars ?resvals _ = _ |- + exists l, + map.putmany_of_list_zip resvars resvals _ = Some _ /\ _ + => + let Heq := fresh in + pose proof H as Heq; eapply putmany_Some in H; destr H + end. + match goal with + | H: map.putmany_of_list_zip _ _ _ = Some ?x0 |- _ => eexists x0; split; [ eapply H | ] + end. + match goal with + | |- forall m', map.split m' mKeep mReceive -> _ + => intros + end. + match goal with + | H: map.split ?m ?mKeep ?mReceive, + H': forall m', + map.split m' mKeep mReceive -> _ + |- _ => eapply H' in H + end. + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m' ?x _ |- exists lH' mcH', + map.agree_on _ lH' _ /\ + (post _ _ lH' _) => + exists x; eexists; split; [ | eapply H ] + end. + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + match goal with + | H: map.agree_on (union _ _) _ _ |- _ => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on (diff (of_list ?l1) (of_list ?l2)) ?l ?lL + |- _ => + match goal with + | H': map.putmany_of_list_zip l2 ?v l = Some ?x |- _ => + match goal with + | H'': map.putmany_of_list_zip l2 v lL = Some ?x0 + |- map.agree_on (of_list l1) x x0 => + eapply agree_on_subset; + [ eauto using agree_on_putmany + | eapply subset_trans; + [ eapply subset_union_rl; eapply subset_ref + | eapply sameset_union_diff_oflist ] + ] + end + end + end. + - simpl. + intros. + eapply @exec.call; fwd. + + match goal with + | H: deadassignment_functions ?eH = Success ?eL, + H1: map.get eH ?fname = Some ?x |- + map.get eL fname = Some _ => + unfold deadassignment_functions in H; + unfold deadassignment_function in H; + eapply map.try_map_values_fw in H; [ | eapply H1 ]; + repeat (destr H; simpl in H) + end. + match goal with + | H: Success _ = Success ?x, + H1: map.get ?eL ?fname = Some x + |- map.get eL fname = Some _ + => inversion H; fwd; eapply H1 + end. + + match goal with + | H: map.getmany_of_list ?l ?args = Some ?argvs + |- map.getmany_of_list lL args = Some _ => + replace (map.getmany_of_list lL args) with (map.getmany_of_list l args); [ eapply H | ] + end. + match goal with + | H: map.agree_on ?s ?l ?lL + |- map.getmany_of_list l ?args + = map.getmany_of_list lL ?args + => eapply agree_on_getmany; + eapply agree_on_subset; [ eapply H | ] + end. + repeat match goal with + | |- context[of_list (ListSet.list_union _ _ _)] => rewrite ListSet.of_list_list_union + | |- context[ListSet.list_diff] => rewrite of_list_list_diff + end. + match goal with + | |- subset ?x (union ?x ?y) => + eapply subset_union_rl; eapply subset_ref + end. + + match goal with + | |- map.putmany_of_list_zip _ _ _ = Some _ => eassumption + end. + + match goal with + | |- exec _ _ _ _ _ _ _ => eauto using agree_on_refl + end. + + match goal with + | |- forall t' m' mc' st1, + compile_post ?rets ?outcome t' m' st1 mc' -> _ + => unfold compile_post; intros; fwd + end. + + match goal with + | H: outcome _ _ _ _, + H1: forall t' m' mc' st1, + outcome _ _ _ _ -> + exists retvs l', + map.getmany_of_list st1 ?rets = Some retvs /\ _ + |- _ => eapply H1 in H; fwd + end. + + match goal with + | H: map.putmany_of_list_zip ?binds ?x1 ?l = Some ?x2, + H1: map.agree_on _ l ?lL + |- context[map.putmany_of_list_zip ?binds _ ?lL] => + let Heq := fresh in + pose proof H as Heq; eapply putmany_Some in H; destr H; fwd + end. + + match goal with + | H: map.agree_on (of_list ?rets) ?lH' ?st1, + H1: map.getmany_of_list ?lH' ?rets = Some ?retvs, + H2: map.putmany_of_list_zip ?binds ?retvs _ = Some ?x |- + exists retvs0 l'0, + map.getmany_of_list st1 rets = Some retvs0 /\ _ + => exists retvs; exists x; repeat split; [ | eapply H2 | ] + end. + * match goal with + | H: map.agree_on (of_list ?rets) ?lH' ?st1, + H1: map.getmany_of_list ?lH' ?rets = Some ?retvs + |- map.getmany_of_list ?st1 ?rets = Some ?retvs + => apply agree_on_getmany in H; rewrite <- H; eapply H1 + end. + * match goal with + | H: post ?t' ?m' ?l' _ + |- exists lH'0 mcH'0, + map.agree_on (of_list ?used_after) lH'0 ?x /\ + post ?t' ?m' lH'0 mcH'0 + => exists l'; eexists; split; [ | eapply H ] + end. + repeat match goal with + | H: context[of_list (ListSet.list_union _ _ _)] |- _ => rewrite ListSet.of_list_list_union in H + | H: context[ListSet.list_diff] |- _ => rewrite of_list_list_diff in H + end. + match goal with + | H: map.agree_on (union _ _) ?l ?lL + |- _ => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (of_list ?binds)) ?l ?lL, + H1: map.putmany_of_list_zip binds ?retvs l = Some ?l', + H2: map.putmany_of_list_zip binds retvs lL = Some ?x + |- map.agree_on (of_list used_after) l' x + => eapply agree_on_subset; + [ eauto using agree_on_putmany | + eapply subset_trans; + [ eapply subset_union_rl; eapply subset_ref | + eapply sameset_union_diff_oflist ] + ] + end. + - simpl. + intros. + match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ => + apply agree_on_find in H; destr H + end. + eapply @exec.load; fwd. + + match goal with + | H: map.agree_on (of_list [?a]) ?l ?lL, + H1: map.get ?l ?a = Some ?addr |- + map.get ?lL ?a = Some _ => rewrite <- H; [ eassumption | ] + end. + match goal with + | |- ?s \in of_list [?s] => cut (of_list [s] s); [ simpl; intro; auto | unfold of_list; simpl; auto ] + end. + + match goal with + | H: Memory.load _ _ _ = Some _ |- Memory.load _ _ _ = Some _ => eapply H + end. + + match goal with + | |- compile_post _ _ _ _ _ _ => unfold compile_post + end. + match goal with + | H: post ?t m (map.put ?l ?x ?v) _, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list used_after) lH' + (map.put lL x v) /\ + post t m lH' mcH' + => exists (map.put l x v); eexists; split; [ | ] ; + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) _ |- post t m (map.put l x v) _ => eapply H + | |- _ => idtac + end + end. + + match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; + apply agree_on_diff_of_list_singleton; + assumption + end. + + - simpl. intros. + repeat match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ + => apply agree_on_find in H; destr H + end. + eapply @exec.store; fwd. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | |- Memory.store _ _ (word.add _ _) _ = Some _ => eassumption + end. + + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: map.agree_on ?s ?l ?lL, + H1: post ?t ?m' ?l ?mcH' + |- exists lH' mcH', + map.agree_on ?s lH' ?lL /\ + post ?t ?m' lH' mcH' + => exists l; eexists; split; [ eapply H | eapply H1 ] + end. + - simpl. intros. + match goal with + | H: map.agree_on (of_list (if _ then _ else _)) _ _ |- _ => + apply agree_on_find in H; destr H + end. + eapply @exec.inlinetable. + + match goal with + | |- ?x <> ?i => assumption + end. + + match goal with + | H: map.get ?l ?a = Some _, + H1: map.agree_on (of_list [?a]) ?l ?lL|- map.get ?lL ?a = Some _ => + rewrite <- H1; [ eapply H | ]; cut (of_list [a] a); [ auto | constructor; reflexivity ] + end. + + match goal with + | |- Memory.load _ (OfListWord.map.of_list_word _) _ = Some _ => eassumption + end. + + (* Note for further automation: + this goal's proof is exactly lifted from + the exec.load case's corresponding goal. *) + + match goal with + | |- context[compile_post] => unfold compile_post + end. + + match goal with + | H: post ?t m (map.put ?l ?x ?v) _, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list used_after) lH' + (map.put lL x v) /\ + post t m lH' mcH' + => exists (map.put l x v); eexists; split; [ | ] ; + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) _ |- post t m (map.put l x v) _ => eapply H + | |- _ => idtac + end + end. + match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list used_after) (map.put ?l ?x ?v) (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; + eapply agree_on_subset; + [ eapply agree_on_diff_of_list_singleton; eassumption + | eapply sameset_ref ] + end. + - simpl. + intros. + eapply @exec.stackalloc. + + match goal with + | |- ?n mod Memory.bytes_per_word ?width = 0 => assumption + end. + + (* For complicated goals like this, + unsure how sound automation will be. *) + match goal with + | |- forall a mStack mCombined, + Memory.anybytes a ?n mStack -> + map.split mCombined ?mSmall mStack -> + exec _ _ _ mCombined _ _ _ + => intros + end. + match goal with + | H: context[exec _ (deadAssignment _ _) _ _ _ _ _], + H1: Memory.anybytes _ _ _, + H2: map.agree_on (of_list (List.removeb eqb ?x ?l')) ?l ?lL |- exec _ (deadAssignment _ _) _ _ (map.put ?lL ?x ?a) _ _ => + eapply H with (lL := map.put lL x a) in H1 + end. + all: try match goal with + | H: map.split _ ?mSmall ?mStack |- + map.split _ ?mSmall ?mStack => eapply H + end. + all: try match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list _) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; eapply agree_on_diff_of_list_singleton; eassumption + end. + + match goal with + | H: exec ?eL ?s ?t ?m ?l _ ?post |- exec ?eL ?s ?t ?m ?l _ ?post' => eapply exec.weaken; [ eapply H | simpl ] + end. + match goal with + | |- context[compile_post] => + unfold compile_post; simpl; intros; fwd + end. + match goal with + | H: Memory.anybytes ?a ?n ?mStack', + H1: map.split ?m' ?mSmall' ?mStack', + H2: post ?t' ?mSmall' ?lH' ?mcH', + H3: map.agree_on (of_list ?used_after) ?lH' ?l' + |- exists mSmall'1 mStack'1, + Memory.anybytes ?a ?n mStack'1 /\ + map.split ?m' mSmall'1 mStack'1 /\ + (exists lH'0 mcH'0, + map.agree_on (of_list ?used_after) lH'0 ?l' /\ + post ?t' mSmall'1 lH'0 mcH'0) => + exists mSmall'; exists mStack'; propositional idtac + end. + - simpl. intros. + match goal with + | H: context[existsb (eqb ?x) ?used_after] |- + context[existsb (eqb ?x) ?used_after] => + destr (existsb (eqb x) used_after) + end; + match goal with + | H: map.agree_on (of_list (live _ _)) ?l ?lL |- _ => + simpl in H + end. + + eapply @exec.lit. + unfold compile_post. + match goal with + | H: existsb (eqb ?x) ?used_after = true, + H1: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL, + H2: post ?t ?m (map.put ?l ?x (word.of_Z ?v)) ?mcH + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x (word.of_Z ?v)) /\ + post ?t ?m lH' mcH' => simpl in H1; exists (map.put l x (word.of_Z v)); eexists; propositional idtac + end. + * match goal with + | H: map.agree_on (of_list (List.removeb eqb ?x ?used_after)) ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => rewrite ListSet.of_list_removeb in H; eapply agree_on_diff_of_list_singleton; eassumption + end. + * match goal with + | H: post ?t ?m ?l ?mc |- + post ?t ?m ?l _ => eapply H + end. + + eapply @exec.skip. + unfold compile_post. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: map.agree_on (of_list ?used_after) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' ?lL + /\ post ?t ?m lH' mcH' => + exists (map.put l x v); + exists mcH; propositional idtac; + apply agree_on_put_not_in; eauto + end. + - simpl. intros. + match goal with + | H: context[existsb (eqb ?x) ?used_after] |- + context[existsb (eqb ?x) ?used_after] => + destr (existsb (eqb x) used_after) + end; + match goal with + | H: map.agree_on (of_list (live _ _)) ?l ?lL |- _ => + simpl in H + end. + all: try repeat match goal with + | H: context[match ?z with _ => _ end] |- _ => destr z + end; simpl. + all: try match goal with + | H: find (eqb ?y) ?l = Some ?y' |- _ => + apply find_some in H; destr H; + match goal with + | H: (?a = ?b)%string |- _ => + apply eqb_eq in H; rewrite H in * + end; + match goal with + | H: In ?x (ListSet.list_union _ _ _) |- _ => + apply in_of_list in H4 + end + end. + + all: try repeat rewrite ListSet.of_list_list_union, ListSet.of_list_removeb in *. + + eapply @exec.op. + * match goal with + | H: map.get ?l ?s = Some ?y', + H1: ?s \in ?s', + H2: map.agree_on ?s' ?l ?lL + |- map.get ?lL ?s = _ => rewrite H2 in H; [ eapply H | eapply H1 ] + end. + * match goal with + | H: exec.lookup_op_locals ?l (Var ?v) = Some ?z', + H1: map.agree_on (union (of_list [?v]) _) ?l ?lL |- exec.lookup_op_locals ?lL (Var ?v) = Some _ => unfold exec.lookup_op_locals in *; simpl; rewrite H1 in H; [ eapply H | ] + end. + + match goal with + | |- ?v \in union (of_list [?v]) _ => + apply in_union_l; constructor; reflexivity + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: map.agree_on + (union _ + (diff (of_list ?used_after) (singleton_set ?x))) + ?l ?lL + + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x ?v) /\ post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split + end. + -- match goal with + | H: map.agree_on + (union _ (diff (of_list ?used_after) (singleton_set ?x))) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; eassumption + end. + -- match goal with + | H: post ?t ?m ?l ?mc |- post ?t ?m ?l ?mc + => eapply H + end. + + (* Note: duplicated from previous '+' case, + with change from Var v -> Const c *) + eapply @exec.op. + * match goal with + | H: map.get ?l ?s = Some ?y', + H1: ?s \in ?s', + H2: map.agree_on ?s' ?l ?lL + |- map.get ?lL ?s = _ => rewrite H2 in H; [ eapply H | eapply H1 ] + end. + * match goal with + | |- exec.lookup_op_locals ?lL (Const ?v) = Some _ => unfold exec.lookup_op_locals in *; simpl; reflexivity + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: exec.lookup_op_locals _ (Const ?c) = Some ?z' |- _ => + simpl in H; inversion H; fwd + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: map.agree_on + (union _ + (diff (of_list ?used_after) (singleton_set ?x))) ?l ?lL + + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x ?v) /\ post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split; + [ | eapply H ] + end. + match goal with + | H: map.agree_on + (union _ (diff (of_list ?used_after) (singleton_set ?x))) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; eassumption + end. + + eapply @exec.op. + * match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + match goal with + | H: map.get ?l ?y = Some ?y', + H1: map.get ?l ?y = map.get ?lL ?y + |- map.get ?lL ?y = Some _ => rewrite <- H1; eapply H + end. + * match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + + match goal with + | H: exec.lookup_op_locals ?l (Var ?v) = Some ?z' |- exec.lookup_op_locals ?lL (Var ?v) = Some _ => unfold exec.lookup_op_locals in *; simpl + end. + + match goal with + | H: map.agree_on + (of_list + (ListSet.list_union eqb [?v] + _)) ?l ?lL, + H1: map.get ?l ?v = Some ?z' |- map.get ?lL ?v = Some _ => rewrite H in H1; [ apply H1 | rewrite ListSet.of_list_list_union; apply in_union_l ] + end. + match goal with + | |- ?v \in of_list [?v] => constructor; reflexivity + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + match goal with + | H: map.agree_on + (of_list + (ListSet.list_union eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_list_union in H; + apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (of_list (List.removeb eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_removeb in H + end. + match goal with + | H: context[exec.lookup_op_locals] |- _ => simpl in H + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) + (singleton_set ?x)) + ?l ?lL, + H1: post ?t ?m (map.put ?l ?x (?f ?op ?y' ?z')) ?mcH + |- exists lH' mcH', + map.agree_on (of_list ?used_after) + lH' + (map.put ?lL ?x (?f ?op ?y' ?z')) /\ + post ?t ?m lH' mcH' + => exists (map.put l x (f op y' z')); exists mcH; split; + [ | eapply H1 ] + end. + match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; eassumption + end. + + match goal with + | H: map.agree_on (of_list (?y :: ?c)) ?l ?lL + |- _ => eapply agree_on_cons in H; destr H + end. + match goal with + | H: map.agree_on + (of_list + (ListSet.list_union eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_list_union in H; + apply agree_on_union in H; destr H + end. + match goal with + | H: map.agree_on + (of_list (List.removeb eqb _ _)) ?l ?lL + |- _ => rewrite ListSet.of_list_removeb in H + end. + match goal with + | H: context[exec.lookup_op_locals] |- _ => + simpl in H; fwd + end. + eapply @exec.op. + * match goal with + | H: map.get ?l ?y = Some ?y', + H1: map.get ?l ?y = map.get ?lL ?y + |- map.get ?lL ?y = Some _ => + rewrite H1 in H; eapply H + end. + * match goal with + | |- context[exec.lookup_op_locals] => + simpl; auto + end. + * match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m + (map.put ?l ?x (?f ?op ?y' ?z')) + ?mcH, + H1: map.agree_on (diff (of_list ?used_after) + (singleton_set ?x)) + ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' + (map.put ?lL ?x (?f ?op ?y' ?z')) /\ + post ?t ?m lH' mcH' + => exists (map.put l x (f op y' z')); exists mcH; split + end. + -- match goal with + | H: map.agree_on + (diff (of_list ?used_after) (singleton_set ?x)) + ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) + (map.put ?lL ?x ?v) + => eapply agree_on_diff_of_list_singleton; + eassumption + end. + -- match goal with + | H: post ?t ?m ?l ?mcH |- post ?t ?m ?l ?mcH + => eapply H + end. + + eapply @exec.skip. + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: existsb (eqb ?x) ?used_after = false, + H2: map.agree_on (of_list ?used_after) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' ?lL /\ + post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split; [ | eapply H ] + end. + match goal with + | H: existsb (eqb ?x) ?used_after = false, + H1: map.agree_on (of_list ?used_after) ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) ?lL => + eapply agree_on_put_not_in; [ eapply H1 | eapply H ] + end. + - simpl. intros. + match goal with + | H: context[existsb (eqb ?x) ?used_after] |- + context[existsb (eqb ?x) ?used_after] => + destr (existsb (eqb x) used_after) + end; + match goal with + | H: map.agree_on (of_list (live _ _)) ?l ?lL |- _ => + simpl in H + end. + + all: try repeat match goal with + | H: context[match ?z with _ => _ end] |- _ => destr z + end; simpl. + + all: try match goal with + | H: find (eqb ?y) ?l = Some ?y' |- _ => + apply find_some in H; destr H; + match goal with + | H: (?a = ?b)%string |- _ => + apply eqb_eq in H; rewrite H in * + end; + match goal with + | H: In ?s _ |- _ => + apply in_of_list in H + end + end. + + eapply @exec.set. + * match goal with + | H: map.get ?l ?s = Some ?y' + , H1: map.agree_on (of_list ?l') ?l ?lL + , H2: ?s \in of_list ?l' |- _ => + rewrite H1 in H; [ eapply H | eapply H2 ] + end. + * match goal with + | |- context[compile_post] => unfold compile_post; simpl + end. + repeat match goal with + | H: context[of_list (List.removeb eqb _ _)] |- _ => + rewrite ListSet.of_list_removeb in H + end. + + match goal with + | H: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL, + H1: post ?t ?m (map.put ?l ?x ?y') ?mcH, + H2: ?s \in (diff (of_list ?used_after) (singleton_set ?x)) + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' (map.put ?lL ?x ?y) /\ post ?t ?m lH' mcH' => + exists (map.put l x y); exists mcH; split; [ | eapply H1 ] + end. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL |- + map.agree_on (of_list ?used_after) (map.put ?l ?x ?y') (map.put ?lL ?x ?y') => + eapply agree_on_diff_of_list_singleton; + eapply H + end. + + match goal with + | H: map.agree_on (of_list (_ :: _)) _ _ |- _ => + eapply agree_on_cons in H; destr H + end. + eapply @exec.set. + * match goal with + | H: map.get ?l ?y = Some ?y', + H1: map.get ?l ?y = map.get ?lL ?y + |- map.get ?lL ?y = Some _ => + rewrite H1 in H; eapply H + end. + * match goal with | |- context[compile_post] => unfold compile_post end. + + repeat match goal with + | H: context[of_list (List.removeb eqb _ _)] |- _ => + rewrite ListSet.of_list_removeb in H + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?y') ?mcH, + H1: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' (map.put ?lL ?x ?y') /\ post ?t ?m lH' mcH' => exists (map.put l x y'); exists mcH; split; [ | eapply H ] + end. + match goal with + | H: map.agree_on (diff (of_list ?used_after) (singleton_set ?x)) ?l ?lL |- map.agree_on (of_list ?used_after) (map.put ?l ?x ?y') (map.put ?lL ?x ?y') => + eapply agree_on_diff_of_list_singleton; eapply H + end. + + eapply @exec.skip. + match goal with + | |- context[compile_post] => unfold compile_post + end. + match goal with + | H: post ?t ?m (map.put ?l ?x ?v) ?mcH, + H1: existsb (eqb ?x) ?used_after = false, + H2: map.agree_on (of_list ?used_after) ?l ?lL + |- exists lH' mcH', + map.agree_on (of_list ?used_after) lH' ?lL /\ + post ?t ?m lH' mcH' + => exists (map.put l x v); exists mcH; split; [ | eapply H ] + end. + match goal with + | H: existsb (eqb ?x) ?used_after = false, + H1: map.agree_on (of_list ?used_after) ?l ?lL + |- map.agree_on (of_list ?used_after) + (map.put ?l ?x ?v) ?lL => + eapply agree_on_put_not_in; [ eapply H1 | eapply H ] + end. + - simpl. intros. + repeat match goal with + | H: map.agree_on (of_list (ListSet.list_union _ _ _)) ?l ?lL |- _ => rewrite ListSet.of_list_list_union in H; eapply agree_on_union in H; destr H + end. + eapply @exec.if_true. + + eauto 2 using accessed_vars_bcond_eval. + + eauto 2 using IHexec. + - simpl. intros. + repeat match goal with + | H: map.agree_on (of_list (ListSet.list_union _ _ _)) ?l ?lL |- _ => rewrite ListSet.of_list_list_union in H; eapply agree_on_union in H; destr H + end. + eapply @exec.if_false. + + eauto 2 using accessed_vars_bcond_eval. + + eauto 2 using IHexec. + - intros. + simpl in *. + rename IHexec into IH1. + rename H4 into IH2. + rename H6 into IH12. + eapply @exec.loop. + + + (* The goal here isn't true; see the helper file for attempts. *) + admit. + + intros. + unfold compile_post in H8. + repeat destr H8. + apply H1 in H9. + admit. (* easier; apply eval_bcond equality *) + + intros. + unfold compile_post in *. + inversion H9. + repeat destr H8. + eapply H2 in H10. + 2: admit. (* followes from accessed_vars_bcond *) + exists x. eexists. + split; admit. (* follows from assumptions *) + + intros. + unfold compile_post in H8. + repeat destr H8. + eapply H4 in H10. + 2: admit. (* follows from accessed_vars_bcond *) + * eapply H10. + * admit. (* goal here also might be untrue *) + + intros. + unfold compile_post in * . + repeat destr H8. + eapply H6 in H9. + * eapply H9. + * admit. (* unsure *) + - + + + eexists. split. + * admit. + * + + 13: { + intros. + simpl. + eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). + - eapply IHexec. simpl in H3. eapply H3. + - intros. unfold compile_post in H4. fwd. + eapply H2. + + eapply H4p1. + + eapply H4p0. + } + Proof. + induction 2; unfold compile_post in *; simpl. + { simpl. + intros. + eapply @exec.interact; eauto. + eauto. + intros. apply H3 in H5. + destruct H5. destruct H5. + eexists. split. + all: eauto using agree_on_refl. + } + { simpl. intros. + eapply @exec.call. + * unfold deadassignment_functions in H. + unfold deadassignment_function in H. + simpl in H. + eapply map.try_map_values_fw in H. + 2: { eapply H0. } + destruct H. + destruct H. + inversion H. + rewrite <- H8 in H6. + apply H6. + * eassumption. + * eassumption. + * eapply IHexec. apply agree_on_refl. + * intros. destruct H6. destruct H6. + destruct H6. eapply H4 in H7. + destruct H7. destruct H7. + destruct H7. destruct H8. + eexists. eexists. + split. + -- eapply agree_on_getmany in H6. + rewrite <- H6. + eassumption. + -- split. + ++ eapply H8. + ++ eexists. eexists. + split. + 2: eapply H9. + eapply agree_on_refl. + + } + { simpl. intros. + eapply @exec.load; eauto. + destr (find (eqb a) (List.removeb eqb x used_after)). + all: eauto using agree_on_refl. + } + { simpl. intros. + destr (find (eqb v) used_after). + - destr (find (eqb a) used_after); eauto using agree_on_refl. + - destr (find (eqb a) (v :: used_after)); eauto using agree_on_refl. + } + { simpl. intros. + eauto using agree_on_refl. + } + { simpl. intros. + all: eauto using agree_on_refl. + apply @exec.stackalloc; auto. + simpl. intros. + eapply @exec.weaken. + -- eauto using agree_on_refl. + -- simpl. intros. + propositional idtac. + } + { simpl. intros. + destr (existsb (eqb x) used_after). + all: eauto 6 using agree_on_refl, agree_on_not_in. + } + { simpl. intros. + destr (existsb (eqb x) used_after). + all: eauto 6 using agree_on_refl, agree_on_not_in. + } + { simpl; eauto. + intros. destr (existsb (eqb x) used_after). + all: eauto 6 using agree_on_refl, agree_on_not_in. + } + { simpl. intros. + eapply @exec.if_true; eauto. + eapply IHexec. + eapply agree_on_subset. + -- eapply H2. + -- unfold subset. intros. + rewrite ListSet.of_list_list_union. + apply in_union_l. + rewrite ListSet.of_list_list_union. + apply in_union_l. + assumption. + } + { simpl. intros. + eapply @exec.if_false; eauto. + eapply IHexec. + all: eauto. + eapply agree_on_subset. + -- eapply H2. + -- unfold subset. intros. + rewrite ListSet.of_list_list_union. + apply in_union_l. + rewrite ListSet.of_list_list_union. + apply in_union_r. + assumption. + } + { simpl. intros. + eapply @exec.loop; eauto. + - eapply @exec.weaken. + + eapply IHexec. + admit. + + admit. + - intros. eapply H2 in H8. + 2: eassumption. + repeat eexists. + eapply H8. + - intros. eapply H4 in H8. + 2: eassumption. + + eapply H8. + + admit. + - admit. + } + { simpl. + intros. + eapply @exec.seq with (mid := compile_post (live (deadAssignment used_after s2) used_after) mid). + - (* specialize (IHexec (live s2 used_after)). + specialize IHexec with (1 := H3). + apply IHexec in H3. + eapply IHexec. *) + + eapply IHexec. + + eapply H3. + (* eapply agree_on_subset. + + eapply H3. *) + (* + + admit. (* eapply live_monotone. *) + (* replace (live sH used_after) with (live sH used_after') + where subset used_after used_after' + *) + + (* show that + of_list (live (deadAss used_after s2) used_after) + is subset of (live s2 used_after), and that + forall s1 u u', + subset u u' -> + subset (of_list (live s1 u)) (of_list live s1 u') *) +*) + - simpl. intros. + unfold compile_post in H4. + fwd. + eapply H2. + + (* context has that there exists some lH' and mcH', + but goal has that a specific lH and mcH that satisfy mid + eexists. eexists. + all: eauto. + all: ad mit. + exec.seq *) + all: admit. + } + { simpl. + intros. + eapply @exec.skip; eauto. + eexists. eexists. + split. + 2: eassumption. + apply agree_on_refl. + } + Admitted. + +End WithArguments. +(* + Lemma live_monotone : + forall s used_after used_after', + subset (of_list used_after) (of_list used_after') -> + subset (of_list (live s used_after)) (of_list (live s used_after')). + Proof. + induction s; intros. + + - (* SLoad *) + simpl. + destr (find (eqb a) (List.removeb eqb x used_after)). + + eapply find_some in E. + destr E. + eapply eqb_eq in H1. + subst. + eapply in_of_list in H0. + repeat rewrite ListSet.of_list_removeb in *. + + assert (subset (diff (of_list used_after) (singleton_set x)) (diff (of_list used_after') (singleton_set x))) by (eauto using subset_diff). + + assert (s \in diff (of_list used_after') (singleton_set x)) by eauto. + rewrite <- ListSet.of_list_removeb in H2. + + destr (find (eqb s) (List.removeb eqb x used_after')). + * rewrite ListSet.of_list_removeb. auto. + * eapply find_none in E. + 2: eapply H2. + rewrite eqb_refl in E. discriminate. + + simpl. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + * destr (find (eqb a) (List.removeb eqb x used_after')). + -- eapply find_some in E0. + destr E0. + eapply eqb_eq in H1. + subst. + eauto with set_hints. + + -- rewrite of_list_cons. + unfold add. eapply subset_union_rl. + eapply subset_ref. + * destr (find (eqb a) (List.removeb eqb x used_after')). + -- do 2 (rewrite ListSet.of_list_removeb). + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + do 2 (rewrite ListSet.of_list_removeb). + eauto using subset_diff. + - (* SStore *) + simpl. + (* destruct_one_match *) + repeat match goal with + | |- context[if ?c then _ else _] => + lazymatch c with + | context[if ?c' then _ else _] => fail + | _ => destr c + end + end. + destruct_one_match. + destr (find (eqb v) used_after). + + eapply find_some in E. + destr E. + eapply eqb_eq in H1. + subst. + assert (of_list used_after s) by (propositional idtac). + assert (of_list used_after' s). + { eapply H. auto. } + destr (find (eqb s) used_after'). + * destr (find (eqb a) used_after). + -- eapply find_some in E0. destr E0. + eapply eqb_eq in H4. + symmetry in H4. + subst. + assert (of_list used_after' a). + { eapply H. auto. } + destr (find (eqb a) used_after'). + ++ auto. + ++ eapply find_none in E0. + 2: { eapply H4. } + rewrite eqb_refl in E0. discriminate. + -- destr (find (eqb a) used_after'). + ++ rewrite of_list_cons. + unfold add. + eapply find_some in E1. + destr E1. + eapply eqb_eq in H4. + subst. + apply subset_union_l. + ** eauto using in_singleton. + ** eauto. + ++ repeat rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** apply subset_union_rl. + eapply subset_ref. + ** apply subset_union_rr. + auto. + * destr (find (eqb a) used_after). + -- eapply find_some in E0. destr E0. + eapply eqb_eq in H4. + symmetry in H4. + subst. + assert (of_list used_after' a). + { eapply H. auto. } + destr (find (eqb a) (s :: used_after')). + ++ rewrite of_list_cons. + unfold add. + eauto using subset_union_rr. + ++ rewrite of_list_cons. + unfold add. + eauto using subset_union_rr. + -- rewrite of_list_cons. + unfold add. + apply subset_union_l. + ++ destr (find (eqb a) (s :: used_after')). + ** eapply find_some in E1. + destr E1. + eapply eqb_eq in H4. + symmetry in H4. + subst. + eauto using in_singleton. + ** rewrite of_list_cons. + unfold add. + apply subset_union_rl. + eauto using subset_refl. + ++ destr (find (eqb a) (s :: used_after')). + ** rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto. + ** rewrite of_list_cons. + unfold add. + apply subset_union_rr. + rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto. + + destr (find (eqb a) (v :: used_after)). + * eapply find_some in E0. + destr E0. + eapply eqb_eq in H1. + symmetry in H1. + subst. + eapply in_inv in H0. + propositional idtac. + -- destr (find (eqb a) used_after'). + ++ simpl. rewrite E0. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ** eapply in_singleton. + apply find_some in E0. + destr E0. + eapply eqb_eq in H1. + subst. + auto. + ** auto. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** destr (find (eqb a) (a :: used_after')). + --- rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + ** destr (find (eqb a) (a :: used_after')). + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + assumption. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + rewrite of_list_cons. + unfold add. + apply subset_union_rr. + assumption. + -- destr (find (eqb v) used_after'). + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** apply find_some in E0. + destr E0. + apply eqb_eq in H2. + symmetry in H2. subst. + destr (find (eqb a) used_after'). + --- eapply find_some in E0. + destr E0. eapply eqb_eq in H3. + subst. + auto using in_singleton. + --- eapply subset_trans. + 2: { rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eapply subset_ref. } + eauto using in_singleton. + ** destr (find (eqb a) used_after'). + --- auto. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + auto. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** destr (find (eqb a) (v :: used_after')). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + apply subset_ref. + ** destr (find (eqb a) (v :: used_after')). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + assumption. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + assumption. + * simpl in E0. + destr (a =? v)%string; [ discriminate | ]. + destr (find (eqb v) used_after'). + -- apply find_some in E2. + destr E2. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb a) used_after'). + ++ apply find_some in E2. + destr E2. + apply eqb_eq in H2. + symmetry in H2. + subst. + rewrite of_list_cons. + unfold add. + apply subset_union_l; [ eauto using in_singleton | ]. + rewrite of_list_cons. + unfold add. + apply subset_union_l; [ eauto using in_singleton | eauto ]. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_l. + ** rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + ** rewrite of_list_cons. + unfold add. + apply subset_union_l. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto using in_singleton. + --- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + eauto. + -- rewrite of_list_cons. + unfold add. + apply subset_union_l. + ++ destr (find (eqb a) (v :: used_after')). + ** simpl in E3. + destr ((a =? v)%string). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- apply find_some in E3. + destr E3. + apply eqb_eq in H1. + symmetry in H1. + subst. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eauto using in_singleton. + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ++ destr (find (eqb a) (v :: used_after')). + ** simpl in E3. + destr ((a =? v)%string). + + --- + (* context here has something like + v <> v in premises, which should + make this trivial, but unsure how *) + rewrite of_list_cons. + unfold add. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + +++ eapply subset_union_rl. + eapply subset_ref. + +++ eauto using subset_union_rr. + --- rewrite of_list_cons. + unfold add. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + +++ eapply subset_union_rl. + eapply subset_ref. + +++ eauto using subset_union_rr. + ** rewrite of_list_cons. + unfold add. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + --- eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + auto. + - simpl. + destr (find (eqb i) (List.removeb eqb x used_after)). + + apply find_some in E. + destr E. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb i) (List.removeb eqb x used_after')). + * repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + * rewrite of_list_cons. + unfold add. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff, subset_union_rr. + + rewrite of_list_cons. + unfold add. + apply subset_union_l. + * destr (find (eqb i) (List.removeb eqb x used_after')). + -- apply find_some in E0. + destr E0. + eapply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + * destr (find (eqb i) (List.removeb eqb x used_after')). + -- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SStackalloc *) + simpl. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SLit *) + simpl. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SOp *) + simpl. destr z. + + simpl. + destr (find (eqb v) (List.removeb eqb x used_after)). + * simpl. + apply find_some in E. + destr E. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after)). + -- simpl. + apply find_some in E. + destr E. + apply eqb_eq in H2. + symmetry in H2. + subst. + destr (find (eqb v) (List.removeb eqb x used_after')). + ++ apply find_some in E. + destr E. + eapply eqb_eq in H3. + symmetry in H3. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + ** apply find_some in E. + destr E. + eapply eqb_eq in H4. + symmetry in H4. + subst. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ++ destr (find (eqb y) (v :: List.removeb eqb x used_after')). + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + auto using subset_diff. + -- rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ++ destr (find (eqb v) (List.removeb eqb x used_after')). + ** destr (find (eqb y) (List.removeb eqb x used_after')). + --- apply find_some in E1. + destr E1. + apply eqb_eq in H2. + symmetry in H2. + subst. + auto using in_singleton. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ** destr (find (eqb y) (v :: List.removeb eqb x used_after')). + --- apply find_some in E1. + destr E1. + apply eqb_eq in H2. + symmetry in H2. + subst. + eauto using in_singleton. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ++ destr (find (eqb v) (List.removeb eqb x used_after')). + ** destr (find (eqb y) (List.removeb eqb x used_after')). + --- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ** destr (find (eqb y) (v :: List.removeb eqb x used_after')). + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + auto using subset_diff. + * destr (find (eqb y) (v :: List.removeb eqb x used_after)). + ++ rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- eapply find_some in E1. + destr E1. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + +++ eauto using in_singleton. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eauto using in_singleton. + --- destr (find (eqb y) (v :: List.removeb eqb x used_after')). + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- eapply find_some in E1. + destr E1. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + +++ repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- destr (find (eqb y) (v :: List.removeb eqb x used_after')). + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ++ rewrite of_list_cons. + unfold add. + eapply subset_union_l. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- destr (find (eqb y) (List.removeb eqb x used_after')). + +++ apply find_some in E2. + destr E2. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + --- destr (find (eqb y) (v :: List.removeb eqb x used_after')). + +++ apply find_some in E2. + destr E2. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + +++ rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + eapply subset_ref. + ** destr (find (eqb v) (List.removeb eqb x used_after')). + --- apply find_some in E1. + destr E1. + apply eqb_eq in H1. + symmetry in H1. + subst. + rewrite of_list_cons. + unfold add. + eapply subset_union_l. + +++ destr (find (eqb y) (List.removeb eqb x used_after')). + *** eauto using in_singleton. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + eauto using in_singleton. + +++ destr (find (eqb y) (List.removeb eqb x used_after')). + *** repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + --- rewrite of_list_cons. + unfold add. + apply subset_union_l. + +++ destr (find (eqb y) (v :: List.removeb eqb x used_after')). + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + apply subset_ref. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rl. + apply subset_ref. + +++ destr (find (eqb y) (v :: List.removeb eqb x used_after')). + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + *** rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + rewrite of_list_cons. + unfold add. + eapply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + + simpl. + destr (find (eqb y) (List.removeb eqb x used_after)). + * apply find_some in E. + destr E. + apply eqb_eq in H1. + symmetry in H1. + subst. + destr (find (eqb y) (List.removeb eqb x used_after')). + -- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + * rewrite of_list_cons. + unfold add. + apply subset_union_l. + -- destr (find (eqb y) (List.removeb eqb x used_after')). + ++ apply find_some in E0. + destr E0. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + -- destr (find (eqb y) (List.removeb eqb x used_after')). + ++ repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + ++ rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SSet *) + simpl. + destr (find (eqb y) (List.removeb eqb x used_after)). + + destr (find (eqb y) (List.removeb eqb x used_after')). + * repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + * rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + + rewrite of_list_cons. + unfold add. + apply subset_union_l. + * destr (find (eqb y) (List.removeb eqb x used_after')). + -- apply find_some in E0. + destr E0. + apply eqb_eq in H1. + symmetry in H1. + subst. + eauto using in_singleton. + -- rewrite of_list_cons. + unfold add. + apply subset_union_rl. + apply subset_ref. + * destr (find (eqb y) (List.removeb eqb x used_after')). + -- repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + -- rewrite of_list_cons. + unfold add. + apply subset_union_rr. + repeat rewrite ListSet.of_list_removeb. + eauto using subset_diff. + - (* SIf *) + simpl. + repeat rewrite ListSet.of_list_list_union. + repeat apply subset_union_l. + + apply subset_union_rl. + apply subset_union_rl. + eauto. + + apply subset_union_rl. + apply subset_union_rr. + eauto. + + apply subset_union_rr. + eapply subset_ref. + - (* SLoop *) + simpl. eapply IHs1. + repeat rewrite ListSet.of_list_list_union. + repeat apply subset_union_l. + + apply subset_union_rl. + eapply subset_ref. + + apply subset_union_rr. + apply subset_union_rl. + eauto. + + apply subset_union_rr. + apply subset_union_rr. + apply subset_ref. + - (* SSeq *) + simpl. + eauto. + - (* SSkip *) + simpl. + auto. + - (* SCall *) + simpl. + repeat rewrite ListSet.of_list_list_union. + apply subset_union_l. + + apply subset_union_rl. + apply subset_ref. + + apply subset_union_rr. + all: admit. + Admitted. + + + Lemma deadAssignment_subset : + forall s1 s2 used_after, + subset (of_list (live s1 used_after)) (of_list (live s2 used_after)) -> + subset (of_list (live (deadAssignment used_after s1) used_after)) (of_list (live (deadAssignment used_after s2) used_after)). + Proof. + Abort. + + Lemma deadAssignment_subset' : + forall s u u', + subset (of_list u') (of_list u) -> + subset + (of_list (live (deadAssignment u s) u')) + (of_list (live s u)). + Proof. + induction s. + Abort. + + Lemma deadassignment_live: + forall sH used_after, + subset + (of_list (live (deadAssignment used_after sH) used_after)) + (of_list (live sH used_after)). + Proof. + induction sH. + all: intros; try solve [simpl; eapply subset_refl]. + - (* SStackalloc *) + simpl. repeat (rewrite ListSet.of_list_removeb). eauto using subset_diff. + - (* SLit *) + simpl. destr (existsb (eqb x) used_after); simpl. + + eapply subset_ref. + + rewrite ListSet.of_list_removeb. + eapply sameset_sym. + eapply sameset_sym. + eauto using sameset_diff_not_in. + - (* SOp *) + simpl. destr (existsb (eqb x) used_after); simpl; [ eapply subset_ref | ]. + destr z; simpl. + + destr (find (eqb v) (List.removeb eqb x used_after)). + all: admit. + Admitted. + + + +*) diff --git a/compiler/src/compiler/DeadAssignmentDef.v b/compiler/src/compiler/DeadAssignmentDef.v new file mode 100644 index 000000000..fe2af8ee0 --- /dev/null +++ b/compiler/src/compiler/DeadAssignmentDef.v @@ -0,0 +1,80 @@ +Require Import compiler.util.Common. +Require Import compiler.FlatImp. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.Syntax. +Require Import coqutil.Tactics.fwd. +Require Import String. +Open Scope Z_scope. +Require Import coqutil.Map.MapEauto. +Require Import coqutil.Datatypes.ListSet. +Local Notation var := String.string (only parsing). + +Section WithArgs. + + Context {env: map.map String.string (list var * list var * stmt var)}. + + Local Notation bcond := (@FlatImp.bcond var). + + Definition accessed_vars_bcond(c: bcond): list var := + match c with + | CondBinary _ x y => list_union String.eqb [x] [y] + | CondNez x => [x] + end. + + Fixpoint live(s: stmt var)(used_after: list var): list var := + match s with + | SSet x y + | SLoad _ x y _ + | SInlinetable _ x _ y => + list_union String.eqb [y] (list_diff String.eqb used_after [x]) + | SStore _ a x _ => list_union String.eqb [a; x] used_after + | SStackalloc x _ body => list_diff String.eqb (live body used_after) [x] + | SLit x _ => list_diff String.eqb used_after [x] + | SOp x _ y z => let var_z := match z with + | Var vz => [vz] + | Const _ => [] + end in + list_union String.eqb ([y] ++ var_z) (list_diff String.eqb used_after [x]) + | SIf c s1 s2 => list_union String.eqb + (list_union String.eqb (live s1 used_after) (live s2 used_after)) + (accessed_vars_bcond c) + | SSeq s1 s2 => live s1 (live s2 used_after) + | SLoop s1 c s2 => + live s1 (list_union String.eqb (accessed_vars_bcond c) (list_union String.eqb used_after (live s2 []))) + | SSkip => used_after + | SCall binds _ args + | SInteract binds _ args => list_union String.eqb args (list_diff String.eqb used_after binds) + end. + + Fixpoint deadAssignment(used_after: list var)(s: stmt var) : stmt var := + let deadAssignment' := deadAssignment used_after in + match s with + | SIf c s1 s2 => SIf c (deadAssignment' s1) (deadAssignment' s2) + | SLoop _ _ _ => s + | SStackalloc v1 sz1 s => SStackalloc v1 sz1 (deadAssignment' s) + | SSeq s1 s2 => + let s2' := deadAssignment' s2 in + let s1_used_after := live s2' used_after in + SSeq (deadAssignment s1_used_after s1) (s2') + | SLit x _ => + if existsb (String.eqb x) used_after + then s else SSkip + | SOp x _ _ _ => + if existsb (String.eqb x) used_after + then s else SSkip + | SSet x _ => + if existsb (String.eqb x) used_after + then s else SSkip + | _ => s + end. + + Definition deadassignment_function: (list string * list string * stmt string) -> result (list string * list string * stmt string) := + fun '(argnames, retnames, body) => + let body' := deadAssignment retnames body in + Success (argnames, retnames, body'). + + Definition deadassignment_functions : env -> result env := + map.try_map_values deadassignment_function. + + +End WithArgs. diff --git a/compiler/src/compiler/DeadAssignmentHelper.v b/compiler/src/compiler/DeadAssignmentHelper.v new file mode 100644 index 000000000..aef055401 --- /dev/null +++ b/compiler/src/compiler/DeadAssignmentHelper.v @@ -0,0 +1,737 @@ +Require Import compiler.util.Common. +Require Import compiler.FlatImp. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.Syntax. +Require Import coqutil.Tactics.fwd. +Require Import String. +Require Import compiler.DeadAssignmentDef. +Require Import bedrock2.MetricLogging. +Require Import coqutil.Datatypes.PropSet. + +Local Notation var := String.string (only parsing). + +Section WithArguments. + Context {width : Z}. + Context {BW : Bitwidth.Bitwidth width }. + Context {word : word width } {word_ok : word.ok word}. + Context {locals : map.map string word } {locals_ok: map.ok locals}. + + Lemma putmany_Some' : + forall (lk: list string) lv (m: locals), + (exists m', map.putmany_of_list_zip lk lv m = Some m') + <-> Datatypes.length lk = Datatypes.length lv. + Proof. + induction lk. + - simpl. intros. destr lv. + + simpl. + unfold iff; split. + * intros. reflexivity. + * intros. eauto. + + simpl. + unfold iff; split. + * intros. destr H. discriminate. + * intros. discriminate. + - intros. destr lv. + + simpl. + unfold iff; split. + * intros. destr H. discriminate. + * intros. discriminate. + + simpl. + unfold iff; split. + * intros. apply eq_S. + eapply IHlk. + eapply H. + * intros. apply eq_add_S in H. + eapply IHlk in H. + eapply H. + Qed. + + Lemma putmany_Some: + forall (lk: list string) lv (m0: locals) m1, + map.putmany_of_list_zip lk lv m0 = Some m1 + -> (forall (m: locals), + (exists m', map.putmany_of_list_zip lk lv m = Some m')). + Proof. + intros. + eapply putmany_Some'. + eapply putmany_Some'. + eexists. + eapply H. + Qed. + + Lemma agree_on_union: + forall (s0 s1: set string) (m0 m1: locals), + map.agree_on (union s0 s1) m0 m1 + <-> map.agree_on s0 m0 m1 /\ map.agree_on s1 m0 m1. + Proof. + intros. + unfold iff; split. + - unfold map.agree_on in *. + split; intros; cut (s0 k \/ s1 k); auto. + - unfold map.agree_on in *. + intros. + destr H. + cut (s0 k \/ s1 k). + + intros. destr H2; auto. + + auto. + Qed. + + Lemma agree_on_refl : + forall keySet (m : locals), + map.agree_on keySet m m. + Proof. + intros. + unfold map.agree_on. + intros. + reflexivity. + Qed. + + + Lemma sameset_in: + forall (s1 s2: set string), + sameset s1 s2 -> + forall k, k \in s1 <-> k \in s2. + Proof. + intros. + unfold iff. + propositional idtac. + - unfold sameset in H. + destruct H. + unfold subset in H. + eauto. + - unfold sameset in H. + destruct H. + unfold subset in H0. + eauto. + Qed. + + Lemma union_iff: + forall {E: Type} (s1 s2: set E) (x : E), + union s1 s2 x <-> s1 x \/ s2 x. + Proof. + intros. + unfold iff. + propositional idtac. + Qed. + + + Lemma existsb_of_list : + forall k keySet, + existsb (eqb k) keySet = true <-> k \in of_list keySet. + Proof. + intros. + simpl. + unfold iff. + propositional idtac. + - induction keySet. + + simpl in Hyp. discriminate. + + eapply sameset_in. + * eapply of_list_cons. + * unfold add. eapply union_iff. + simpl in Hyp. + apply Bool.orb_prop in Hyp. + destruct Hyp. + -- left. unfold singleton_set. eapply eqb_eq. rewrite eqb_sym. assumption. + -- right. eapply IHkeySet. eassumption. + - induction keySet. + + unfold of_list in Hyp. simpl in Hyp. + auto. + + simpl. assert (sameset (of_list (a :: keySet)) (add (of_list keySet) a) ) by apply of_list_cons. + assert (k \in (add (of_list keySet) a)). + { eapply sameset_in; eauto. } + unfold add in H0. + eapply union_iff in H0. destruct H0. + * unfold singleton_set in H0. rewrite H0. + rewrite eqb_refl. + rewrite Bool.orb_true_l. + reflexivity. + * assert (existsb (eqb k) keySet = true). + -- eapply IHkeySet. eapply H0. + -- rewrite H1. rewrite Bool.orb_true_r. reflexivity. + Qed. + + + + Lemma agree_on_not_in: + forall keySet (m: locals) x, + existsb (String.eqb x) keySet = false -> + forall y, + map.agree_on (PropSet.of_list keySet) (map.put m x y) m. + Proof. + intros. + unfold map.agree_on. + intros. + rewrite map.get_put_dec. + destr (x =? k)%string. + - apply existsb_of_list in H0. + rewrite H in H0. discriminate. + - reflexivity. + Qed. + + + Lemma agree_on_subset: + forall s1 s2 (m1 m2: locals), + map.agree_on s2 m1 m2 -> + subset s1 s2 -> + map.agree_on s1 m1 m2. + Proof. + intros. + unfold map.agree_on in *. + intros. + unfold subset in *. + eauto. + Qed. + + Lemma sameset_implies_subset: + forall (s1 s2: set string), + sameset s1 s2 -> + subset s1 s2. + Proof. + unfold sameset, subset. + intros. destr H; auto. + Qed. + + Lemma agree_on_sameset: + forall s1 s2 (m1 m2: locals), + map.agree_on s2 m1 m2 -> + sameset s1 s2 -> + map.agree_on s1 m1 m2. + Proof. + intros. + eauto using agree_on_subset, sameset_implies_subset. + Qed. + + Lemma agree_on_cons: + forall (h: string) t (m1 m2: locals), + map.agree_on (of_list (h :: t)) m1 m2 + -> map.get m1 h = map.get m2 h /\ + map.agree_on (of_list t) m1 m2. + Proof. + intros. + eapply agree_on_sameset in H. + 2: { eapply sameset_sym. eapply of_list_cons. } + unfold add in H. + split. + - assert (map.agree_on (singleton_set h) m1 m2). + { + eapply agree_on_subset. + - eapply H. + - eapply subset_union_rl. + eapply sameset_implies_subset. + eapply sameset_ref. + } + unfold map.agree_on in H0. + eapply H0. + unfold singleton_set. + eapply eq_refl. + - eapply agree_on_subset. + + eapply H. + + eapply subset_union_rr. + eapply sameset_implies_subset. + eapply sameset_ref. + Qed. + + Lemma agree_on_getmany : + forall rets (x st1 : locals), + map.agree_on (of_list rets) x st1 -> + map.getmany_of_list x rets = map.getmany_of_list st1 rets. + Proof. + intros. + unfold map.getmany_of_list. + induction rets; simpl; [ reflexivity | ]. + eapply agree_on_cons in H. + destr H. + rewrite H. + destr (map.get st1 a); [ | reflexivity ]. + eapply IHrets in H0. + rewrite H0. + reflexivity. + Qed. + + + Lemma subset_diff : + forall (s1 s2 s3: set string), + subset s1 s2 -> + subset (diff s1 s3) (diff s2 s3). + Proof. + intros. + unfold subset, diff. + intros. + assert (x \in s1 /\ ~ (x \in s3)). + { assert ((fun x : string => x \in s1 /\ ~ x \in s3) x) by exact H0. + simpl in H1. + assumption. + } + assert ((x \in s2) /\ (~x \in s3) -> x \in (fun x0 : string => x0 \in s2 /\ ~ x0 \in s3)). + { auto. } + eapply H2. + destr H1. split; eauto. + Qed. + + Lemma sameset_diff : + forall (s1 s2 s3: set string), + sameset s1 s2 -> + sameset (diff s1 s3) (diff s2 s3). + Proof. + intros. + unfold sameset in *. + destr H. + split; eauto using subset_diff. + Qed. + + Lemma sameset_diff_not_in: + forall (s: list string) x, + existsb (eqb x) s = false -> + sameset (diff (of_list s) (singleton_set x)) + (of_list s). + Proof. + intros. + unfold sameset; split. + * unfold subset; simpl. + intros. + unfold diff in H. + assert (x0 \in of_list s /\ ~ x0 \in singleton_set x) by auto. + destr H0; assumption. + * unfold subset; simpl. + intros. + unfold diff. + cut (x0 \in of_list s /\ ~ x0 \in singleton_set x); [ auto | ]. + split; [ assumption | ]. + eapply existsb_of_list in H0. + assert (x = x0 -> False). + { intros; subst. rewrite H0 in H. discriminate. } + auto. + Qed. + + + Lemma diff_subset: + forall s1 s2: set string, + subset (diff s1 s2) s1. + Proof. + intros. + unfold subset. + intros. + unfold diff in H. + assert (s1 x /\ ~ (s2 x)) by auto. + cut (s1 x). + { auto. } + destr H0; auto. + Qed. + + Lemma existsb_removeb_None: + forall (s: string) l, + existsb (eqb s) l = false -> + List.removeb eqb s l = l. + Proof. + intros. induction l. + - simpl; reflexivity. + - simpl in H. + apply Bool.orb_false_elim in H. + destr H. + eapply IHl in H0. + simpl. + rewrite H. simpl. + rewrite H0. + reflexivity. + Qed. + Lemma in_singleton : + forall (x: string) (s: list string), + In x s -> + subset (singleton_set x) (of_list s). + Proof. + intros. + unfold subset, singleton_set. + intros. + assert (eq x x0) by auto. + subst. + propositional idtac. + Qed. + + Lemma of_list_list_diff: + forall l1 l2 : list string, + of_list (ListSet.list_diff eqb l1 l2) = + diff (of_list l1) (of_list l2). + Proof. + intros. + (* PR for this lemma being proved in coqutil exists; + unsure how to prove it without the assumptions + in the file that ListSet.of_list_list_union + is proven in *) + Admitted. + + + Lemma agree_on_put: + forall a r s (mH mL: locals) mH' mL', + map.agree_on s mH mL -> + map.put mH a r = mH' -> + map.put mL a r = mL' -> + map.agree_on (union s (singleton_set a)) mH' mL'. + Proof. + intros. + apply agree_on_union. + split. + - unfold map.agree_on in *. + intros. + eapply H in H2. + subst. + destr (eqb a k). + + repeat rewrite map.get_put_same; reflexivity. + + repeat rewrite map.get_put_diff; eauto. + - unfold map.agree_on. + intros. + cut (a = k). + + intros. subst. + repeat rewrite map.get_put_same; reflexivity. + + assert (singleton_set a k) by auto. + unfold singleton_set in *; assumption. + Qed. + + Lemma union_sameset: + forall (s1 s2 s1' s2': set string), + sameset s1 s1' -> + sameset s2 s2' -> + sameset (union s1 s2) (union s1' s2'). + Proof. + intros. + unfold sameset, union. + split. + - unfold sameset, subset in *. + propositional idtac. + assert (x \in s1 \/ x \in s2) by auto. + cut (x \in s1' \/ x \in s2'); [ auto | ]. + destr H. + + left; eauto. + + right; eauto. + - unfold sameset, subset in *. + propositional idtac. + assert (x \in s1' \/ x \in s2') by auto. + cut (x \in s1 \/ x \in s2); [ auto | ]. + destr H. + + left; eauto. + + right; eauto. + Qed. + + Lemma agree_on_putmany: + forall (lk0: list string) lv s (mH mL: locals) mH' mL', + map.agree_on s mH mL -> + map.putmany_of_list_zip lk0 lv mH = Some mH' -> + map.putmany_of_list_zip lk0 lv mL = Some mL' -> + map.agree_on (union s (of_list lk0)) mH' mL'. + Proof. + induction lk0. + - intros. simpl in *. + destr lv; [ | discriminate ]. + apply agree_on_union. + split. + + inversion H0. + inversion H1. + subst; eauto. + + unfold map.agree_on. + intros. + cut (of_list [] k). + * unfold of_list. + intros. + exfalso. + eauto using in_nil. + * auto. + - intros. destr lv; [ discriminate | ]. + simpl in *. + cut (map.agree_on (union s (singleton_set a)) + (map.put mH a r) (map.put mL a r)). + + intros. + eapply IHlk0 in H2. + 2-3: eassumption. + eapply agree_on_sameset. + * eassumption. + * eapply sameset_trans. + 2: { eapply union_assoc. } + apply union_sameset; + [ eapply sameset_ref | eapply of_list_cons ]. + + eapply agree_on_put. + 2-3: reflexivity. + eassumption. + Qed. + + + Lemma sameset_union_diff_oflist: + forall (l1 l2: list string), + sameset (union (of_list l1) (of_list l2)) (union (diff (of_list l1) (of_list l2) ) (of_list l2)). + Proof. + intros. + unfold sameset, of_list, subset, union, diff. + + assert (forall x, In x l2 \/ ~ (In x l2)). + { intro. eapply ListDec.In_decidable. unfold ListDec.decidable_eq. + intros. destr (eqb x0 y). + - unfold Decidable.decidable. left. reflexivity. + - unfold Decidable.decidable. right. eassumption. + } + + split. + - intros. + cut ((fun x : string => + x \in (fun e : string => In e l1) \/ + x \in (fun e : string => In e l2)) x); [ simpl; intro | auto ]. + cut ((In x l1) \/ (In x l2)); [ simpl; intro | auto ]. + cut ((fun x0 : string => + x0 \in + (fun x1 : string => + x1 \in (fun e : string => In e l1) /\ + ~ x1 \in (fun e : string => In e l2)) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + assert (In x l2 \/ ~ In x l2) by eapply H. + destr H3. + + right. auto. + + propositional idtac. left. + cut ((fun x1 : string => + x1 \in (fun e : string => In e l1) /\ + ~ x1 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + split; auto. + - intros. + cut ((fun x : string => + x \in + (fun x0 : string => + x0 \in (fun e : string => In e l1) /\ + ~ x0 \in (fun e : string => In e l2)) \/ + x \in (fun e : string => In e l2)) x); [ | auto ]. + simpl. intro. + destr H1. + + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) /\ + ~ x0 \in (fun e : string => In e l2)) x); [ simpl; intro | auto ]. + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + destr H2. left. assumption. + + cut ((fun x0 : string => + x0 \in (fun e : string => In e l1) \/ + x0 \in (fun e : string => In e l2)) x); [ simpl; intro; auto | ]. + simpl. + right. assumption. + Qed. + + Lemma sameset_diff_singleton: + forall (l: list string) x, + sameset (diff (of_list l) (of_list [x])) (diff (of_list l) (singleton_set x)). + Proof. + intros. + unfold diff. + unfold sameset. + split; unfold subset; intros. + - cut ((fun x0 : string => + x0 \in of_list l /\ ~ x0 \in of_list [x]) x0); [ | auto ]. + simpl. + intros. + cut ((fun x1 : string => + x1 \in of_list l /\ ~ x1 \in singleton_set x) x0); [ auto | ]. + simpl. + destr H0. + split. + + assumption. + + unfold singleton_set, of_list in *. + destr (eqb x x0). + * assert (~ (In x0 [x0])) by auto. + assert (In x0 [x0]) by eapply in_eq. + eapply H2 in H3. + exfalso; auto. + * eauto. + - cut ((fun x0 : string => + x0 \in of_list l /\ ~ x0 \in of_list [x]) x0); [ auto | ]. + simpl. + cut ((fun x1 : string => + x1 \in of_list l /\ ~ x1 \in singleton_set x) x0); [ | auto ]. + simpl. + intro. + destr H0. + split. + + assumption. + + unfold singleton_set, of_list in *. + cut ((fun e : string => In e [x]) x0 -> False); [ auto | ]. + simpl. + intros. + destr H2; [ | assumption ]. + subst. + assert (eq x0 x0) by auto. + assert (eq x0 x0 -> False) by auto. + auto. + Qed. + + Lemma agree_on_find: + forall s l (m1 m2: locals), + map.agree_on (of_list (if (find (eqb s) l) + then l + else s :: l)) m1 m2 + -> map.agree_on (of_list [s]) m1 m2 /\ + map.agree_on (of_list l) m1 m2. + Proof. + intros. + destr (find (eqb s) l). + - split. + + unfold map.agree_on. + intros. + assert (k = s). + { cut (of_list [s] k); auto. + intros. destr H1; auto. + inversion H1. + } + rewrite H1 in *; clear H1. + apply find_some in E. + destr E. + apply eqb_eq in H2. + rewrite H2 in *. + eauto. + + assumption. + - eapply agree_on_sameset in H. + 2: eapply sameset_sym; eapply of_list_cons. + unfold add in H. + apply agree_on_union in H. + propositional idtac. + unfold map.agree_on in H_l. + assert (map.get m1 s = map.get m2 s). { + apply H_l. + unfold singleton_set. + cut (eq s s); auto. + } + unfold map.agree_on. + intros. + assert (k = s). + { cut (of_list [s] k); auto. + intros. destr H1; auto. + inversion H1. + } + rewrite H1. + assumption. + Qed. + + Lemma agree_on_put_not_in : + forall x l (m1 m2: locals), + map.agree_on (of_list l) m1 m2 + -> existsb (eqb x) l = false + -> forall v, + map.agree_on (of_list l) (map.put m1 x v) m2. + Proof. + intros. + unfold map.agree_on. + intros. + rewrite <- H. + 2: eassumption. + erewrite agree_on_not_in. + 3: eassumption. + 2: eassumption. + reflexivity. + Qed. + + Lemma subset_of_list_union_diff_singleton: + forall (l: list string) x, + subset (of_list l) + (union (diff (of_list l) (singleton_set x)) + (singleton_set x)). + Proof. + intros. + match goal with + | |- subset (of_list _) + (union (diff (of_list ?s) (singleton_set ?x)) + (singleton_set ?x)) => + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union _ _) => + eapply union_sameset; + match goal with + | |- sameset (diff _ _) _ => + eapply sameset_sym; eapply sameset_diff_singleton + | |- sameset (singleton_set _) _ => + eapply sameset_sym; eapply of_list_singleton + end + end; + eapply subset_trans; + match goal with + | |- subset (of_list _) _ => idtac + | |- subset _ (union (diff _ _) _) => eapply sameset_union_diff_oflist + end; + eapply subset_union_rl; + eapply subset_ref + end. + Qed. + + Lemma agree_on_diff_of_list_singleton: + forall (l: list string) x (m1 m2: locals), + map.agree_on (diff (of_list l) (singleton_set x)) m1 m2 -> + forall v, + map.agree_on (of_list l) (map.put m1 x v) (map.put m2 x v). + Proof. + intros. + eapply agree_on_subset. + - eapply agree_on_put. + 2-3: reflexivity. + eapply H. + - eapply subset_of_list_union_diff_singleton. + Qed. + + Lemma accessed_vars_bcond_eval : + forall (l lL: locals) cond val, + map.agree_on (of_list (accessed_vars_bcond cond)) l lL -> + eval_bcond l cond = Some val -> + eval_bcond lL cond = Some val. + Proof. + intros. + induction cond. + - simpl in *. + repeat (match goal with + | H: match ?c with _ => _ end = Some _ |- _ => + destr c + end; try match goal with + | H: None = Some _ |- _ + => inversion H + end). + repeat match goal with + | H: context[if ?c then _ else _] |- _ => destr c; fwd + end. + + match goal with + | H: map.get ?l ?s = Some ?r, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; fwd + end. + match goal with + | H: map.agree_on (of_list [?s]) ?l ?lL, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; [ | constructor; reflexivity ]; + repeat rewrite H1 + end. + reflexivity. + + repeat match goal with + | H: map.agree_on (of_list _) ?l ?lL |- _ => + apply agree_on_cons in H; destr H + end. + repeat match goal with + | H: map.get ?l ?s = map.get ?lL ?s, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; fwd + end. + reflexivity. + - simpl in *. + repeat (match goal with + | H: match ?c with _ => _ end = Some _ |- _ => + destr c + end; try match goal with + | H: None = Some _ |- _ + => inversion H + end); fwd. + repeat match goal with + | H: map.agree_on (of_list _) ?l ?lL |- _ => + apply agree_on_cons in H; destr H + end; fwd. + repeat match goal with + | H: map.get ?l ?s = map.get ?lL ?s, + H1: map.get ?l ?s = Some ?r0 |- _ => + rewrite H in H1; fwd + end. + reflexivity. + Qed. + + + +End WithArguments. diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v index 6dd84f8b4..2f22991b4 100644 --- a/compiler/src/compiler/Pipeline.v +++ b/compiler/src/compiler/Pipeline.v @@ -51,8 +51,9 @@ Require Import coqutil.Tactics.autoforward. Require Import compiler.FitsStack. Require Import compiler.LowerPipeline. Require Import bedrock2.WeakestPreconditionProperties. -Require Import compiler.UseImmediateDef. -Require Import compiler.UseImmediate. +Require Export compiler.UseImmediateDef. +Require Export compiler.UseImmediate. +Require Export compiler.DeadAssignmentDef. Import Utility. Section WithWordAndMem. @@ -299,6 +300,42 @@ Section WithWordAndMem. - eauto. Qed. + Lemma deadassignment_functions_NoDup: forall funs funs', + (forall f argnames retnames body, + map.get funs f = Some (argnames, retnames, body) -> NoDup argnames /\ NoDup retnames) -> + (deadassignment_functions funs = Success funs') -> + forall f argnames retnames body, + map.get funs' f = Some (argnames, retnames, body) -> NoDup argnames /\ NoDup retnames. + Proof. + unfold deadassignment_functions. intros. + eapply map.try_map_values_bw in H0. + 2: { eassumption. } + unfold deadassignment_function in *. + fwd. + eapply H. + eassumption. + Qed. + + Lemma deadassignment_correct: phase_correct FlatWithStrVars FlatWithStrVars deadassignment_functions. + Proof. + unfold FlatWithStrVars. + split; cbn. + { unfold map.forall_values, ParamsNoDup. intros. + destruct v as ((argnames & retnames) & body). + eapply deadassignment_functions_NoDup; try eassumption. + intros. specialize H0 with (1 := H2). + simpl in H0. assumption. + } + + unfold locals_based_call_spec. intros. fwd. + pose proof H0 as GI. + unfold deadassignment_functions in GI. + eapply map.try_map_values_fw in GI. 2: eassumption. + unfold deadassignment_function in GI. fwd. + eexists _, _, _, _. split. 1: eassumption. split. 1: eassumption. + intros. + Admitted. + Lemma regalloc_functions_NoDup: forall funs funs', regalloc_functions funs = Success funs' -> forall f argnames retnames body, @@ -440,7 +477,8 @@ Section WithWordAndMem. (compose_phases (useimmediate_functions is5BitImmediate is12BitImmediate) (compose_phases regalloc_functions (compose_phases spill_functions - (riscvPhase compile_ext_call))))). + (riscvPhase compile_ext_call))))). + Lemma composed_compiler_correct: phase_correct SrcLang RiscvLang composed_compile. Proof. @@ -459,6 +497,24 @@ Section WithWordAndMem. | Failure e => Failure e end. + (* only for testing the dead assignment phase, remove in the future *) + Definition composed_compile': + string_keyed_map (list string * list string * cmd) -> + result (list Instruction * string_keyed_map Z * Z) := + (compose_phases flatten_functions + (compose_phases (useimmediate_functions is5BitImmediate is12BitImmediate) + (compose_phases deadassignment_functions + (compose_phases regalloc_functions + (compose_phases spill_functions + (riscvPhase compile_ext_call)))))). + + (* only for testing the dead assignment phase, remove in the future *) + Definition compile'(funs: list (string * (list string * list string * cmd))): + result (list Instruction * list (string * Z) * Z) := + match composed_compile' (map.of_list funs) with + | Success (insts, pos, space) => Success (insts, map.tuples pos, space) + | Failure e => Failure e + end. Definition valid_src_fun: (string * (list string * list string * cmd)) -> bool := fun '(name, (args, rets, body)) => andb (List.list_eqb String.eqb (List.dedup String.eqb args) args) diff --git a/compiler/src/compilerExamples/deadAssExample.v b/compiler/src/compilerExamples/deadAssExample.v new file mode 100644 index 000000000..5336ad733 --- /dev/null +++ b/compiler/src/compilerExamples/deadAssExample.v @@ -0,0 +1,160 @@ +Require Import compiler.ExprImp. +Require Import compiler.Pipeline. +Require Import compiler.DeadAssignmentDef. +Require Import riscv.Spec.Decode. +Require Import riscv.Utility.Words32Naive. +Require Import riscv.Utility.DefaultMemImpl32. +Require riscv.Utility.InstructionNotations. +Require Import riscv.Utility.Encode. +Require Import coqutil.Map.SortedList. +Require coqutil.Map.SortedListString. +Require Import compiler.MemoryLayout. +Require riscv.Utility.bverify. +Open Scope Z_scope. +Open Scope string_scope. +Open Scope ilist_scope. + +Local Instance funpos_env: map.map string Z := SortedListString.map _. + + + (* dead assignments because of immediate optimization *) + + (* loading a constant into a variable usually assigns the constant first to a + temp variable, but with the useimmediate optimization the temp variable shouldn't + be used *) + Definition test_constant : (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.set "ret_val" (expr.literal 4193)))). + + (* making sure that the optimization recurses into a stack alloc. *) + Definition test_stackalloc : (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.stackalloc "x" 4 + (cmd.seq (cmd.set "x" (expr.literal 1303)) + (cmd.stackalloc "y" 4 + (cmd.seq (cmd.set "y" (expr.literal 1217)) + (cmd.set "ret_val" (expr.var "x")))))))). + + + (* checking that if-else's are recursed into *) + Definition test_ifelse : (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.stackalloc "x" 4 + (cmd.stackalloc "y" 4 + (cmd.seq (cmd.set "x" (expr.literal 7307)) + (cmd.seq (cmd.set "y" (expr.literal 1711)) + (cmd.cond + (expr.literal 9) + (cmd.set "ret_val" (expr.literal 6409)) + (cmd.set "ret_val" (expr.var "x"))))))))). + + +(* test to check breaking a call*) + Definition test_call_fn : (string * (list string * list string * cmd)) + := ("first_arg", (["x"; "y"], ["ret_val"], + (cmd.set "ret_val" (expr.var "x")))). + + Definition test_call: (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.stackalloc "x" 4 + (cmd.stackalloc "y" 4 + (cmd.stackalloc "z" 4 + (cmd.seq (cmd.set "x" (expr.literal 7307)) + (cmd.seq (cmd.set "y" (expr.literal 1711)) + (cmd.seq (cmd.set "z" (expr.literal 9231)) + (cmd.call ["ret_val"] "first_arg" [expr.var "x"; expr.var "y"]))))))))). + + (* test to check simple loops *) + Definition test_loop_fn : (string * (list string * list string * cmd)) + := ("return_1019", (["x"; "y"], ["ret_val"], + (cmd.seq (cmd.set "ret_val" (expr.literal 0)) + (cmd.while + (expr.op + bopname.sub + (expr.var "ret_val") + (expr.literal 1019) + ) + (cmd.seq + (cmd.set "x" (expr.op + bopname.add + (expr.var "x") + (expr.literal 706))) + (cmd.seq + (cmd.set "ret_val" + (expr.op + bopname.add + (expr.var "ret_val") + (expr.literal 1))) + (cmd.set "y" (expr.op + bopname.xor + (expr.var "x") + (expr.literal 4902))))))))). + + Definition test_loop: (string * (list string * list string * cmd)) + := ("main", ([]: list string, ["ret_val"], + (cmd.call ["ret_val"] "return_1019" [expr.literal 131; expr.literal (-97)]))). + + Definition compile_ext_call(posenv: funpos_env)(mypos stackoffset: Z)(s: FlatImp.stmt Z) : list Instruction := []. + +Local Instance RV32I_bitwidth: FlatToRiscvCommon.bitwidth_iset 32 RV32I. +Proof. reflexivity. Qed. + +Definition multi_compile funs_lists := + List.all_success + (List.map + (fun x => '(insts, _, _) <- (compile compile_ext_call x) ;; Success insts) funs_lists). + +(* Expressing nested list literals as [[x]] is wonky + because of [[]] being used for list of Instructions *) +Definition imm_asm: list (list Instruction). + let r := eval cbv in (multi_compile + ([test_constant] :: + [test_stackalloc] :: + [test_ifelse] :: + [test_loop_fn; test_loop] :: + [test_call_fn; test_call] :: [])) in set (res := r). + match goal with + | res := Success (?x) |- _ => exact x + end. +Defined. + + + +Definition multi_compile' funs_lists := + List.all_success + (List.map + (fun x => '(insts, _, _) <- (compile' compile_ext_call x) ;; Success insts) funs_lists). + +Definition imm_asm' : list (list Instruction). + let r := eval cbv in (multi_compile' + ([test_constant] :: + [test_stackalloc] :: + [test_ifelse] :: + [test_loop_fn; test_loop] :: + [test_call_fn; test_call] :: [])) in set (res := r). + match goal with + | res := Success (?x) |- _ => exact x + end. +Defined. + +Module PrintAssembly. + Import riscv.Utility.InstructionNotations. + Goal True. let r := eval unfold imm_asm in imm_asm in idtac (* r *). Abort. +End PrintAssembly. + + +Module PrintAssembly'. + Import riscv.Utility.InstructionNotations. + Goal True. let r := eval unfold imm_asm' in imm_asm' in idtac (* r *). Abort. + +End PrintAssembly'. + +Module CheckAssembly. + Goal Forall (bverify.validInstructions RV32I) imm_asm'. + repeat (constructor; [solve + [apply bverify.bvalidInstructions_valid; + vm_compute; reflexivity] + | ]). + constructor. + Qed. +End CheckAssembly.