From 88553f08d8f2ad96ae615e9648b7c1417573247a Mon Sep 17 00:00:00 2001 From: James Pollard Date: Tue, 2 Jun 2020 14:46:40 +0100 Subject: Keep track of declarations in HTLgen. --- src/translation/HTLgen.v | 85 +++++++++++++++++++++++++++++++++++------------- 1 file changed, 62 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index aa965fc..0fe6656 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -27,10 +27,15 @@ Hint Resolve AssocMap.gss : htlh. Hint Resolve Ple_refl : htlh. Hint Resolve Ple_succ : htlh. +Inductive scl_decl : Type := Scalar (sz : nat). +Inductive arr_decl : Type := Array (sz : nat) (ln : nat). + Record state: Type := mkstate { st_st : reg; st_freshreg: reg; st_freshstate: node; + st_scldecls: AssocMap.t scl_decl; + st_arrdecls: AssocMap.t arr_decl; st_datapath: datapath; st_controllogic: controllogic; }. @@ -39,6 +44,8 @@ Definition init_state (st : reg) : state := mkstate st 1%positive 1%positive + (AssocMap.empty scl_decl) + (AssocMap.empty arr_decl) (AssocMap.empty stmnt) (AssocMap.empty stmnt). @@ -68,19 +75,9 @@ Module HTLState <: State. Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. Proof. - intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans. - - rewrite H1. rewrite H. reflexivity. - - intros. destruct H4 with n. - + left; assumption. - + destruct H8 with n; - [ rewrite <- H0; left; assumption - | right; rewrite <- H0; apply H10 - ]. - - intros. destruct H5 with n. - + left; assumption. - + destruct H9 with n. - * rewrite <- H0. left. assumption. - * right. rewrite <- H0. apply H10. + intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence. + - destruct H4 with n; destruct H8 with n; intuition congruence. + - destruct H5 with n; destruct H9 with n; intuition congruence. Qed. End HTLState. @@ -102,13 +99,13 @@ Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := Definition check_empty_node_datapath: forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. Proof. - intros. case (s.(st_datapath)!n); intros. right; auto. left; auto. + intros. case (s.(st_datapath)!n); tauto. Defined. Definition check_empty_node_controllogic: forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }. Proof. - intros. case (s.(st_controllogic)!n); intros. right; auto. left; auto. + intros. case (s.(st_controllogic)!n); tauto. Defined. Lemma add_instr_state_incr : @@ -120,6 +117,8 @@ Lemma add_instr_state_incr : s.(st_st) s.(st_freshreg) (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). Proof. @@ -136,6 +135,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := s.(st_st) s.(st_freshreg) (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) (add_instr_state_incr s n n' st STM TRANS) @@ -151,6 +152,8 @@ Lemma add_instr_skip_state_incr : s.(st_st) s.(st_freshreg) (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) (AssocMap.set n Vskip s.(st_controllogic))). Proof. @@ -167,6 +170,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit := s.(st_st) s.(st_freshreg) (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) (AssocMap.set n Vskip s.(st_controllogic))) (add_instr_skip_state_incr s n st STM TRANS) @@ -274,6 +279,8 @@ Lemma add_branch_instr_state_incr: s.(st_st) (st_freshreg s) (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) (AssocMap.set n Vskip (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). Proof. @@ -290,6 +297,8 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := s.(st_st) (st_freshreg s) (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) (AssocMap.set n Vskip (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) @@ -324,32 +333,60 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := end. Lemma create_reg_state_incr: - forall s, + forall s sz, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls)) + s.(st_arrdecls) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_reg (sz : nat) : mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (Scalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) + (create_reg_state_incr s sz). + +Lemma create_arr_state_incr: + forall s sz ln, st_incr s (mkstate s.(st_st) (Pos.succ (st_freshreg s)) (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)). Proof. constructor; simpl; auto with htlh. Qed. -Definition create_reg: mon reg := +Definition create_arr (sz : nat) (ln : nat) : mon reg := fun s => let r := s.(st_freshreg) in OK r (mkstate s.(st_st) (Pos.succ r) (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (Array sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)) - (create_reg_state_incr s). + (create_arr_state_incr s sz ln). Definition transf_module (f: function) : mon module := - do fin <- create_reg; - do rtrn <- create_reg; + do fin <- create_reg 1; + do rtrn <- create_reg 32; do _ <- collectlist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code)); - do start <- create_reg; - do rst <- create_reg; - do clk <- create_reg; + do start <- create_reg 1; + do rst <- create_reg 1; + do clk <- create_reg 1; do current_state <- get; ret (mkmodule f.(RTL.fn_params) @@ -365,6 +402,8 @@ Definition max_state (f: function) : state := mkstate st (Pos.succ st) (Pos.succ (max_pc_function f)) + (st_scldecls (init_state st)) + (st_arrdecls (init_state st)) (st_datapath (init_state st)) (st_controllogic (init_state st)). -- cgit