diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-12 11:37:42 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-12 11:37:42 +0100 |
commit | 13b880f99b7355010551ad1b93242cf7773aa202 (patch) | |
tree | 7b3bbb28641da2db6bda8078cf26cd0e8f0bffd9 /src/translation/HTLgenspec.v | |
parent | f470234beafacccf743a75d4d0e6213b8861ca30 (diff) | |
download | vericert-kvx-13b880f99b7355010551ad1b93242cf7773aa202.tar.gz vericert-kvx-13b880f99b7355010551ad1b93242cf7773aa202.zip |
Declare all registers properly in HTL
Diffstat (limited to 'src/translation/HTLgenspec.v')
-rw-r--r-- | src/translation/HTLgenspec.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 4bf3843..8bb90c6 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -184,41 +184,41 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk m, + forall data control fin rtrn st stk 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) -> m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk fin rtrn) -> + st stk 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 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. @@ -239,11 +239,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 @@ -329,11 +329,11 @@ 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. |