From ea44bd696dcfb446f5f980f16d7df41b21357698 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 6 Jul 2020 19:27:51 +0100 Subject: Fix HTLgenspec. --- src/translation/HTLgen.v | 18 +- src/translation/HTLgenspec.v | 925 +++++++++++++++++++++---------------------- 2 files changed, 467 insertions(+), 476 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 995977c..09af28a 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -414,21 +414,19 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := end) (enumerate 0 ns). -Definition add_single_cycle_load (n n' : node) (stack : reg) (addr : expr) (dst : reg) : mon unit := +Definition create_single_cycle_load (stack : reg) (addr : expr) (dst : reg) : stmnt := let l0 := Vnonblock (Vvarb0 dst) (Vvari stack addr) in let l1 := Vnonblock (Vvarb1 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) in let l2 := Vnonblock (Vvarb2 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in - let l3 := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in - let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3 - in add_instr n n' instr. + let l3 := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) + in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. -Definition add_single_cycle_store (n n' : node) (stack : reg) (addr : expr) (src : reg) : mon unit := +Definition create_single_cycle_store (stack : reg) (addr : expr) (src : reg) : stmnt := let l0 := Vnonblock (Vvari stack addr) (Vvarb0 src) in let l1 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in let l2 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in - let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) in - let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3 - in add_instr n n' instr. + let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) + in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with @@ -442,10 +440,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Iload mem addr args dst n' => do addr' <- translate_eff_addressing addr args; do _ <- declare_reg None dst 32; - add_single_cycle_load n n' stack addr' dst + add_instr n n' $ create_single_cycle_load stack addr' dst | Istore mem addr args src n' => do addr' <- translate_eff_addressing addr args; - add_single_cycle_store n n' stack addr' src + add_instr n n' $ create_single_cycle_store stack addr' src | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 4662cf4..bbcde14 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -134,476 +134,469 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip | tr_instr_Iload : - forall mem addr args s s' i c dst n, - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) + forall mem addr args s s' i e dst n, + translate_eff_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) + (create_single_cycle_load stk e dst) (state_goto st n) | tr_instr_Istore : - forall mem addr args s s' i c src n, - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n) + forall mem addr args s s' i e src n, + translate_eff_addressing addr args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) + (create_single_cycle_store stk e src) (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). Hint Constructors tr_instr : htlspec. -(* Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) *) -(* (fin rtrn st stk : reg) : Prop := *) -(* tr_code_intro : *) -(* forall s t, *) -(* c!pc = Some i -> *) -(* stmnts!pc = Some s -> *) -(* trans!pc = Some t -> *) -(* tr_instr fin rtrn st stk i s t -> *) -(* tr_code c pc i stmnts trans fin rtrn st stk. *) -(* Hint Constructors tr_code : htlspec. *) - -(* Inductive tr_module (f : RTL.function) : module -> Prop := *) -(* tr_module_intro : *) -(* forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, *) -(* m = (mkmodule f.(RTL.fn_params) *) -(* data *) -(* control *) -(* f.(RTL.fn_entrypoint) *) -(* st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> *) -(* (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> *) -(* tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> *) -(* stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> *) -(* Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> *) -(* 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> *) -(* st = ((RTL.max_reg_function f) + 1)%positive -> *) -(* fin = ((RTL.max_reg_function f) + 2)%positive -> *) -(* rtrn = ((RTL.max_reg_function f) + 3)%positive -> *) -(* stk = ((RTL.max_reg_function f) + 4)%positive -> *) -(* start = ((RTL.max_reg_function f) + 5)%positive -> *) -(* rst = ((RTL.max_reg_function f) + 6)%positive -> *) -(* clk = ((RTL.max_reg_function f) + 7)%positive -> *) -(* tr_module f m. *) -(* Hint Constructors tr_module : htlspec. *) - -(* Lemma create_reg_datapath_trans : *) -(* forall sz s s' x i iop, *) -(* create_reg iop sz s = OK x s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_datapath_trans : htlspec. *) - -(* Lemma create_reg_controllogic_trans : *) -(* forall sz s s' x i iop, *) -(* create_reg iop sz s = OK x s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_controllogic_trans : htlspec. *) - -(* Lemma declare_reg_datapath_trans : *) -(* forall sz s s' x i iop r, *) -(* declare_reg iop r sz s = OK x s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_datapath_trans : htlspec. *) - -(* Lemma declare_reg_controllogic_trans : *) -(* forall sz s s' x i iop r, *) -(* declare_reg iop r sz s = OK x s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_reg_controllogic_trans : htlspec. *) - -(* Lemma declare_reg_freshreg_trans : *) -(* forall sz s s' x i iop r, *) -(* declare_reg iop r sz s = OK x s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. inversion 1; auto. Qed. *) -(* Hint Resolve declare_reg_freshreg_trans : htlspec. *) - -(* Lemma create_arr_datapath_trans : *) -(* forall sz ln s s' x i iop, *) -(* create_arr iop sz ln s = OK x s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_arr_datapath_trans : htlspec. *) - -(* Lemma create_arr_controllogic_trans : *) -(* forall sz ln s s' x i iop, *) -(* create_arr iop sz ln s = OK x s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. intros. monadInv H. trivial. Qed. *) -(* Hint Resolve create_arr_controllogic_trans : htlspec. *) - -(* Lemma get_refl_x : *) -(* forall s s' x i, *) -(* get s = OK x s' i -> *) -(* s = x. *) -(* Proof. inversion 1. trivial. Qed. *) -(* Hint Resolve get_refl_x : htlspec. *) - -(* Lemma get_refl_s : *) -(* forall s s' x i, *) -(* get s = OK x s' i -> *) -(* s = s'. *) -(* Proof. inversion 1. trivial. Qed. *) -(* Hint Resolve get_refl_s : htlspec. *) - -(* Ltac inv_incr := *) -(* repeat match goal with *) -(* | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => *) -(* let H1 := fresh "H" in *) -(* assert (H1 := H); eapply create_reg_datapath_trans in H; *) -(* eapply create_reg_controllogic_trans in H1 *) -(* | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => *) -(* let H1 := fresh "H" in *) -(* assert (H1 := H); eapply create_arr_datapath_trans in H; *) -(* eapply create_arr_controllogic_trans in H1 *) -(* | [ H: get ?s = OK _ _ _ |- _ ] => *) -(* let H1 := fresh "H" in *) -(* assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; *) -(* subst *) -(* | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H *) -(* | [ H: st_incr _ _ |- _ ] => destruct st_incr *) -(* end. *) - -(* Lemma collect_controllogic_trans : *) -(* forall A f l cs cs' ci, *) -(* (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> *) -(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). *) -(* Proof. *) -(* induction l; intros; monadInv H0. *) -(* - trivial. *) -(* - apply H in EQ. rewrite EQ. eauto. *) -(* Qed. *) - -(* Lemma collect_datapath_trans : *) -(* forall A f l cs cs' ci, *) -(* (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> *) -(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). *) -(* Proof. *) -(* induction l; intros; monadInv H0. *) -(* - trivial. *) -(* - apply H in EQ. rewrite EQ. eauto. *) -(* Qed. *) - -(* Lemma collect_freshreg_trans : *) -(* forall A f l cs cs' ci, *) -(* (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> *) -(* @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). *) -(* Proof. *) -(* induction l; intros; monadInv H0. *) -(* - trivial. *) -(* - apply H in EQ. rewrite EQ. eauto. *) -(* Qed. *) - -(* Lemma collect_declare_controllogic_trans : *) -(* forall io n l s s' i, *) -(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) -(* s.(st_controllogic) = s'.(st_controllogic). *) -(* Proof. *) -(* intros. eapply collect_controllogic_trans; try eassumption. *) -(* intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. *) -(* Qed. *) - -(* Lemma collect_declare_datapath_trans : *) -(* forall io n l s s' i, *) -(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) -(* s.(st_datapath) = s'.(st_datapath). *) -(* Proof. *) -(* intros. eapply collect_datapath_trans; try eassumption. *) -(* intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. *) -(* Qed. *) - -(* Lemma collect_declare_freshreg_trans : *) -(* forall io n l s s' i, *) -(* HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. eapply collect_freshreg_trans; try eassumption. *) -(* inversion 1. auto. *) -(* Qed. *) - -(* Ltac unfold_match H := *) -(* match type of H with *) -(* | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate *) -(* end. *) - -(* Lemma translate_eff_addressing_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_eff_addressing op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) -(* Qed. *) -(* Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. *) - -(* Lemma translate_comparison_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_comparison op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) -(* Qed. *) -(* Hint Resolve translate_comparison_freshreg_trans : htlspec. *) - -(* Lemma translate_comparison_imm_freshreg_trans : *) -(* forall op args s r s' i n, *) -(* translate_comparison_imm op args n s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *) -(* Qed. *) -(* Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. *) - -(* Lemma translate_condition_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_condition op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) -(* Qed. *) -(* Hint Resolve translate_condition_freshreg_trans : htlspec. *) - -(* Lemma translate_instr_freshreg_trans : *) -(* forall op args s r s' i, *) -(* translate_instr op args s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *) -(* monadInv H1. eauto with htlspec. *) -(* Qed. *) -(* Hint Resolve translate_instr_freshreg_trans : htlspec. *) - -(* Lemma translate_arr_access_freshreg_trans : *) -(* forall mem addr args st s r s' i, *) -(* translate_arr_access mem addr args st s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. *) -(* Qed. *) -(* Hint Resolve translate_arr_access_freshreg_trans : htlspec. *) - -(* Lemma add_instr_freshreg_trans : *) -(* forall n n' st s r s' i, *) -(* add_instr n n' st s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_instr_freshreg_trans : htlspec. *) - -(* Lemma add_branch_instr_freshreg_trans : *) -(* forall n n0 n1 e s r s' i, *) -(* add_branch_instr e n n0 n1 s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_branch_instr_freshreg_trans : htlspec. *) - -(* Lemma add_node_skip_freshreg_trans : *) -(* forall n1 n2 s r s' i, *) -(* add_node_skip n1 n2 s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_node_skip_freshreg_trans : htlspec. *) - -(* Lemma add_instr_skip_freshreg_trans : *) -(* forall n1 n2 s r s' i, *) -(* add_instr_skip n1 n2 s = OK r s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. *) -(* Hint Resolve add_instr_skip_freshreg_trans : htlspec. *) - -(* Lemma transf_instr_freshreg_trans : *) -(* forall fin ret st instr s v s' i, *) -(* transf_instr fin ret st instr s = OK v s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. destruct instr eqn:?. subst. unfold transf_instr in H. *) -(* destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. *) -(* - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. *) -(* apply declare_reg_freshreg_trans in EQ1. congruence. *) -(* - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. *) -(* apply declare_reg_freshreg_trans in EQ1. congruence. *) -(* - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. *) -(* - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *) -(* congruence. *) -(* - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. *) -(* Qed. *) -(* Hint Resolve transf_instr_freshreg_trans : htlspec. *) - -(* Lemma collect_trans_instr_freshreg_trans : *) -(* forall fin ret st l s s' i, *) -(* HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> *) -(* s.(st_freshreg) = s'.(st_freshreg). *) -(* Proof. *) -(* intros. eapply collect_freshreg_trans; try eassumption. *) -(* eauto with htlspec. *) -(* Qed. *) - -(* Ltac rewrite_states := *) -(* match goal with *) -(* | [ H: ?x ?s = ?x ?s' |- _ ] => *) -(* let c1 := fresh "c" in *) -(* let c2 := fresh "c" in *) -(* remember (?x ?s) as c1; remember (?x ?s') as c2; try subst *) -(* end. *) - -(* Ltac inv_add_instr' H := *) -(* match type of H with *) -(* | ?f _ _ _ = OK _ _ _ => unfold f in H *) -(* | ?f _ _ _ _ = OK _ _ _ => unfold f in H *) -(* | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H *) -(* end; repeat unfold_match H; inversion H. *) - -(* Ltac inv_add_instr := *) -(* lazymatch goal with *) -(* | H: context[add_instr_skip _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_instr_skip _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* | H: context[add_instr _ _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_instr _ _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* | H: context[add_branch_instr _ _ _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_branch_instr _ _ _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* | H: context[add_node_skip _ _ _] |- _ => *) -(* inv_add_instr' H *) -(* | H: context[add_node_skip _ _] |- _ => *) -(* monadInv H; inv_incr; inv_add_instr *) -(* end. *) - -(* Ltac destruct_optional := *) -(* match goal with H: option ?r |- _ => destruct H end. *) - -(* Lemma iter_expand_instr_spec : *) -(* forall l fin rtrn stack s s' i x c, *) -(* HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> *) -(* list_norepet (List.map fst l) -> *) -(* (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> *) -(* (forall pc instr, In (pc, instr) l -> *) -(* c!pc = Some instr -> *) -(* tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). *) -(* Proof. *) -(* induction l; simpl; intros; try contradiction. *) -(* destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. *) -(* destruct (peq pc pc1). *) -(* - subst. *) -(* destruct instr1 eqn:?; try discriminate; *) -(* try destruct_optional; inv_add_instr; econstructor; try assumption. *) -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. *) -(* eapply in_map with (f := fst) in H9. contradiction. *) - -(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. *) -(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) - -(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. *) -(* econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct H2. *) -(* * inversion H2. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H2. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct H2. *) -(* * inversion H2. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H2. contradiction. *) - -(* + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *) -(* + inversion H2. *) -(* * inversion H14. constructor. congruence. *) -(* * apply in_map with (f := fst) in H14. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + inversion H2. *) -(* * inversion H9. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H9. contradiction. *) - -(* + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *) -(* + inversion H2. *) -(* * inversion H9. *) -(* replace (st_st s2) with (st_st s0) by congruence. *) -(* eauto with htlspec. *) -(* * apply in_map with (f := fst) in H9. contradiction. *) - -(* - eapply IHl. apply EQ0. assumption. *) -(* destruct H2. inversion H2. subst. contradiction. *) -(* intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. *) -(* destruct H2. inv H2. contradiction. assumption. assumption. *) -(* Qed. *) -(* Hint Resolve iter_expand_instr_spec : htlspec. *) - -(* Lemma create_arr_inv : forall w x y z a b c d, *) -(* create_arr w x y z = OK (a, b) c d -> *) -(* y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). *) -(* Proof. *) -(* inversion 1; split; auto. *) -(* Qed. *) - -(* Lemma create_reg_inv : forall a b s r s' i, *) -(* create_reg a b s = OK r s' i -> *) -(* r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). *) -(* Proof. *) -(* inversion 1; auto. *) -(* Qed. *) - -(* Theorem transl_module_correct : *) -(* forall f m, *) -(* transl_module f = Errors.OK m -> tr_module f m. *) -(* Proof. *) -(* intros until m. *) -(* unfold transl_module. *) -(* unfold run_mon. *) -(* destruct (transf_module f (max_state f)) eqn:?; try discriminate. *) -(* intros. inv H. *) -(* inversion s; subst. *) - -(* unfold transf_module in *. *) -(* unfold stack_correct in *. *) -(* destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; *) -(* destruct (RTL.fn_stacksize f + stmnts!pc = Some s -> + trans!pc = Some t -> + tr_instr fin rtrn st stk i s t -> + tr_code c pc i stmnts trans fin rtrn st stk. +Hint Constructors tr_code : htlspec. + +Inductive tr_module (f : RTL.function) : module -> Prop := + tr_module_intro : + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, + m = (mkmodule f.(RTL.fn_params) + data + control + f.(RTL.fn_entrypoint) + st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + stk_len = Z.to_nat f.(RTL.fn_stacksize) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + st = ((RTL.max_reg_function f) + 1)%positive -> + fin = ((RTL.max_reg_function f) + 2)%positive -> + rtrn = ((RTL.max_reg_function f) + 3)%positive -> + stk = ((RTL.max_reg_function f) + 4)%positive -> + start = ((RTL.max_reg_function f) + 5)%positive -> + rst = ((RTL.max_reg_function f) + 6)%positive -> + clk = ((RTL.max_reg_function f) + 7)%positive -> + tr_module f m. +Hint Constructors tr_module : htlspec. + +Lemma create_reg_datapath_trans : + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma create_reg_controllogic_trans : + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma declare_reg_datapath_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma declare_reg_controllogic_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma declare_reg_freshreg_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. inversion 1; auto. Qed. +Hint Resolve declare_reg_freshreg_trans : htlspec. + +Lemma create_arr_datapath_trans : + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_arr_datapath_trans : htlspec. + +Lemma create_arr_controllogic_trans : + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_arr_controllogic_trans : htlspec. + +Lemma get_refl_x : + forall s s' x i, + get s = OK x s' i -> + s = x. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_x : htlspec. + +Lemma get_refl_s : + forall s s' x i, + get s = OK x s' i -> + s = s'. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_s : htlspec. + +Ltac inv_incr := + repeat match goal with + | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply create_reg_datapath_trans in H; + eapply create_reg_controllogic_trans in H1 + | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply create_arr_datapath_trans in H; + eapply create_arr_controllogic_trans in H1 + | [ H: get ?s = OK _ _ _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; + subst + | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H + | [ H: st_incr _ _ |- _ ] => destruct st_incr + end. + +Lemma collect_controllogic_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_datapath_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_freshreg_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_declare_controllogic_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. + intros. eapply collect_controllogic_trans; try eassumption. + intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_datapath_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. + intros. eapply collect_datapath_trans; try eassumption. + intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_freshreg_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + inversion 1. auto. +Qed. + +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + +Lemma translate_eff_addressing_freshreg_trans : + forall op args s r s' i, + translate_eff_addressing op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. + +Lemma translate_comparison_freshreg_trans : + forall op args s r s' i, + translate_comparison op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_freshreg_trans : htlspec. + +Lemma translate_comparison_imm_freshreg_trans : + forall op args s r s' i n, + translate_comparison_imm op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. + +Lemma translate_condition_freshreg_trans : + forall op args s r s' i, + translate_condition op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_condition_freshreg_trans : htlspec. + +Lemma translate_instr_freshreg_trans : + forall op args s r s' i, + translate_instr op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. + monadInv H1. eauto with htlspec. +Qed. +Hint Resolve translate_instr_freshreg_trans : htlspec. + +Lemma add_instr_freshreg_trans : + forall n n' st s r s' i, + add_instr n n' st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_freshreg_trans : htlspec. + +Lemma add_branch_instr_freshreg_trans : + forall n n0 n1 e s r s' i, + add_branch_instr e n n0 n1 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_branch_instr_freshreg_trans : htlspec. + +Lemma add_node_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_node_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_node_skip_freshreg_trans : htlspec. + +Lemma add_instr_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_instr_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_skip_freshreg_trans : htlspec. + +Lemma transf_instr_freshreg_trans : + forall fin ret st instr s v s' i, + transf_instr fin ret st instr s = OK v s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. destruct instr eqn:?. subst. unfold transf_instr in H. + destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. + - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - apply add_instr_freshreg_trans in EQ2. apply translate_eff_addressing_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - apply add_instr_freshreg_trans in EQ0. apply translate_eff_addressing_freshreg_trans in EQ. + congruence. + - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. + congruence. + - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. +Qed. +Hint Resolve transf_instr_freshreg_trans : htlspec. + +Lemma collect_trans_instr_freshreg_trans : + forall fin ret st l s s' i, + HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + eauto with htlspec. +Qed. + +Ltac rewrite_states := + match goal with + | [ H: ?x ?s = ?x ?s' |- _ ] => + let c1 := fresh "c" in + let c2 := fresh "c" in + remember (?x ?s) as c1; remember (?x ?s') as c2; try subst + end. + +Ltac inv_add_instr' H := + match type of H with + | ?f _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + end; repeat unfold_match H; inversion H. + +Ltac inv_add_instr := + lazymatch goal with + | H: context[add_instr_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_instr _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_branch_instr _ _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_branch_instr _ _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_node_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_node_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + end. + +Ltac destruct_optional := + match goal with H: option ?r |- _ => destruct H end. + +Lemma iter_expand_instr_spec : + forall l fin rtrn stack s s' i x c, + HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> + list_norepet (List.map fst l) -> + (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> + (forall pc instr, In (pc, instr) l -> + c!pc = Some instr -> + tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). +Proof. + induction l; simpl; intros; try contradiction. + destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. + destruct (peq pc pc1). + - subst. + destruct instr1 eqn:?; try discriminate; + try destruct_optional; inv_add_instr; econstructor; try assumption. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H9. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. + * inversion H14. constructor. congruence. + * apply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + - eapply IHl. apply EQ0. assumption. + destruct H2. inversion H2. subst. contradiction. + intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. + destruct H2. inv H2. contradiction. assumption. assumption. +Qed. +Hint Resolve iter_expand_instr_spec : htlspec. + +Lemma create_arr_inv : forall w x y z a b c d, + create_arr w x y z = OK (a, b) c d -> + y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). +Proof. + inversion 1; split; auto. +Qed. + +Lemma create_reg_inv : forall a b s r s' i, + create_reg a b s = OK r s' i -> + r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). +Proof. + inversion 1; auto. +Qed. + +Theorem transl_module_correct : + forall f m, + transl_module f = Errors.OK m -> tr_module f m. +Proof. + intros until m. + unfold transl_module. + unfold run_mon. + destruct (transf_module f (max_state f)) eqn:?; try discriminate. + intros. inv H. + inversion s; subst. + + unfold transf_module in *. + unfold stack_correct in *. + destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; + destruct (RTL.fn_stacksize f