diff options
Diffstat (limited to 'src/translation/HTLgenspec.v')
-rw-r--r-- | src/translation/HTLgenspec.v | 105 |
1 files changed, 81 insertions, 24 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 89b79ac..57d2d87 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -184,7 +184,7 @@ 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, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls, (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) -> @@ -192,34 +192,48 @@ Inductive tr_module (f : RTL.function) : module -> Prop := data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls) -> tr_module f m. Hint Constructors tr_module : htlspec. Lemma create_reg_datapath_trans : - forall sz s s' x i, - create_reg sz s = OK x s' i -> + 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, - create_reg sz s = OK x s' i -> + 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 create_arr_datapath_trans : - forall sz ln s s' x i, - create_arr sz ln s = OK x s' i -> + 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, - create_arr sz ln s = OK x s' i -> + 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. @@ -240,11 +254,11 @@ Hint Resolve get_refl_s : htlspec. Ltac inv_incr := repeat match goal with - | [ H: create_reg _ ?s = OK _ ?s' _ |- _ ] => + | [ 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' _ |- _ ] => + | [ 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 @@ -256,6 +270,44 @@ Ltac inv_incr := | [ 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_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. + Ltac rewrite_states := match goal with | [ H: ?x ?s = ?x ?s' |- _ ] => @@ -330,16 +382,17 @@ Proof. + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. eapply 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. unfold nonblock. rewrite <- e2. rewrite H. constructor. - eapply translate_instr_tr_op. apply EQ1. - 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. assert (HST: st_st s4 = st_st s2) by congruence. rewrite HST. + constructor. eapply translate_instr_tr_op. 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. - + inversion H2. inversion H9. rewrite <- e2. rewrite H. econstructor. apply EQ1. - 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. rewrite <- e2. assert (HST: st_st s2 = st_st s0) by congruence. + rewrite HST. 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. @@ -407,9 +460,13 @@ Proof. econstructor; simpl; trivial. intros. inv_incr. - assert (STC: st_controllogic s9 = st_controllogic s3) by congruence. - assert (STD: st_datapath s9 = st_datapath s3) by congruence. - assert (STST: st_st s9 = st_st s3) by congruence. + assert (EQ3D := EQ3). + destruct x3. + apply collect_declare_datapath_trans in EQ3. + apply collect_declare_controllogic_trans in EQ3D. + assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. + assert (STD: st_datapath s10 = st_datapath s3) by congruence. + assert (STST: st_st s10 = st_st s3) by congruence. rewrite STC. rewrite STD. rewrite STST. eapply iter_expand_instr_spec; eauto with htlspec. apply PTree.elements_complete. |