From a0e6738556fa8aaa019dab6a0a158626385bef4a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 13 Jan 2021 14:49:57 +0000 Subject: Add HTLPargen translation --- src/hls/HTLPargen.v | 180 +++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 130 insertions(+), 50 deletions(-) (limited to 'src/hls') diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 16b0942..474dfef 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -20,6 +20,8 @@ From compcert Require Errors Globalenvs Integers. From compcert Require Import Maps AST. From vericert Require Import Verilog RTLPar HTL Vericertlib AssocMap ValueInt Statemonad. +Import Lia. + Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. Hint Resolve AssocMap.gss : htlh. @@ -55,8 +57,6 @@ Module HTLState <: State. st_st s1 = st_st s2 -> Ple s1.(st_freshreg) s2.(st_freshreg) -> Ple s1.(st_freshstate) s2.(st_freshstate) -> - (forall n, - s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> (forall n, s1.(st_controllogic)!n = None \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> @@ -72,8 +72,7 @@ Module HTLState <: State. 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; intros; try congruence. - - destruct H4 with n; destruct H8 with n; intuition congruence. - - destruct H5 with n; destruct H9 with n; intuition congruence. + destruct H4 with n; destruct H7 with n; intuition congruence. Qed. End HTLState. @@ -104,25 +103,6 @@ Proof. intros. case (s.(st_controllogic)!n); tauto. Defined. -Lemma add_instr_state_incr : - forall s n n' st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - 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. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. - Lemma declare_reg_state_incr : forall i s r sz, st_incr s @@ -147,10 +127,28 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_controllogic)) (declare_reg_state_incr i s r sz). +Lemma add_instr_state_incr : + forall s n n' st, + (st_controllogic s)!n = None -> + st_incr s + (mkstate + 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. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left STM, left TRANS => + match check_empty_node_controllogic s n with + | left TRANS => OK tt (mkstate s.(st_st) s.(st_freshreg) @@ -159,13 +157,12 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := 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) - | _, _ => Error (Errors.msg "HTL.add_instr") + (add_instr_state_incr s n n' st TRANS) + | _ => Error (Errors.msg "HTL.add_instr") end. Lemma add_instr_skip_state_incr : forall s n st, - (st_datapath s)!n = None -> (st_controllogic s)!n = None -> st_incr s (mkstate @@ -184,8 +181,8 @@ Qed. Definition add_instr_skip (n : node) (st : stmnt) : mon unit := fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left STM, left TRANS => + match check_empty_node_controllogic s n with + | left TRANS => OK tt (mkstate s.(st_st) s.(st_freshreg) @@ -194,13 +191,12 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit := 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) - | _, _ => Error (Errors.msg "HTL.add_instr") + (add_instr_skip_state_incr s n st TRANS) + | _ => Error (Errors.msg "HTL.add_instr_skip") end. Lemma add_node_skip_state_incr : forall s n st, - (st_datapath s)!n = None -> (st_controllogic s)!n = None -> st_incr s (mkstate @@ -219,8 +215,8 @@ Qed. Definition add_node_skip (n : node) (st : stmnt) : mon unit := fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left STM, left TRANS => + match check_empty_node_controllogic s n with + | left TRANS => OK tt (mkstate s.(st_st) s.(st_freshreg) @@ -229,8 +225,8 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit := s.(st_arrdecls) (AssocMap.set n Vskip s.(st_datapath)) (AssocMap.set n st s.(st_controllogic))) - (add_node_skip_state_incr s n st STM TRANS) - | _, _ => Error (Errors.msg "HTL.add_instr") + (add_node_skip_state_incr s n st TRANS) + | _ => Error (Errors.msg "HTL.add_node_skip") end. Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. @@ -377,7 +373,6 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := Lemma add_branch_instr_state_incr: forall s e n n1 n2, - (st_datapath s) ! n = None -> (st_controllogic s) ! n = None -> st_incr s (mkstate s.(st_st) @@ -395,8 +390,8 @@ Qed. Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left NSTM, left NTRANS => + match check_empty_node_controllogic s n with + | left NTRANS => OK tt (mkstate s.(st_st) (st_freshreg s) @@ -405,8 +400,8 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := 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) - | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") + (add_branch_instr_state_incr s e n n1 n2 NTRANS) + | _ => Error (Errors.msg "Htlgen: add_branch_instr") end. Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) @@ -508,8 +503,9 @@ Proof. rewrite PTree.gempty. congruence. (* inductive case *) intros. rewrite PTree.gsspec in H2. destruct (peq pc k). - inv H2. xomega. - apply Ple_trans with a. auto. xomega. + inv H2. unfold Ple, Plt in *. lia. + apply Ple_trans with a. auto. + unfold Ple, Plt in *. lia. Qed. Lemma max_pc_wf : @@ -523,19 +519,103 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition Poslength {A : Type} (l : list A) : positive := +Definition poslength {A : Type} (l : list A) : positive := match Zlength l with | Z.pos p => p | _ => 1 end. -Fixpoint Penumerate {A : Type} (p : positive) (l : list A) {struct l} : list (positive * A) := +Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l} : list (positive * A) := match l with - | x :: xs => (p, x) :: Penumerate (Pos.succ p) xs + | x :: xs => (p, x) :: penumerate (Pos.succ p) xs | nil => nil end. -Parameter translate_inst_list : reg -> reg -> reg -> node * list instruction -> mon unit. +Lemma add_data_instr_state_incr : + forall s n st, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath)) + s.(st_controllogic)). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_data_instr (n : node) (st : stmnt) : mon unit := + fun s => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath)) + s.(st_controllogic)) + (add_data_instr_state_incr s n st). + +Lemma add_control_instr_state_incr : + forall s n st, + (st_controllogic s) ! n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + (AssocMap.set n st s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_control_instr (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_controllogic s n with + | left CTRL => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + s.(st_datapath) + (AssocMap.set n st s.(st_controllogic))) + (add_control_instr_state_incr s n st CTRL) + | _ => Error (Errors.msg "HTLPargen.add_control_instr: control logic is not empty") + end. + +Definition translate_inst (fin rtrn stack : reg) (n : node) (i : instruction) : mon unit := + match i with + | RPnop => + add_data_instr n Vskip + | RPop op args dst => + do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; + add_data_instr n (nonblock dst instr) + | RPload chunk addr args dst => + do src <- translate_arr_access chunk addr args stack; + do _ <- declare_reg None dst 32; + add_data_instr n (nonblock dst src) + | RPstore chunk addr args src => + do dst <- translate_arr_access chunk addr args stack; + add_data_instr n (Vnonblock dst (Vvar src)) + end. + +Definition translate_inst_list (fin rtrn stack : reg) (ni : node * list instruction) : mon unit := + let (n, li) := ni in + do _ <- collectlist (translate_inst fin rtrn stack n) li; + do st <- get; + add_control_instr n (state_goto st.(st_st) (Pos.succ n)). Definition translate_cfi (fin rtrn stack : reg) (ni : node * control_flow_inst) : mon unit := let (n, cfi) := ni in @@ -561,9 +641,9 @@ Definition translate_cfi (fin rtrn stack : reg) (ni : node * control_flow_inst) Definition transf_bblock (fin rtrn stack : reg) (ni : node * bblock) : mon unit := let (n, bb) := ni in - do _ <- collectlist (translate_inst_list fin rtrn stack) (Penumerate n bb.(bb_body)); + do _ <- collectlist (translate_inst_list fin rtrn stack) (penumerate n bb.(bb_body)); match bb.(bb_exit) with - | Some e => translate_cfi fin rtrn stack ((n + Poslength bb.(bb_body))%positive, e) + | Some e => translate_cfi fin rtrn stack ((n + poslength bb.(bb_body))%positive, e) | None => ret tt end. -- cgit