From 6cdb6490437b9e609afbf5e8749b24d31c02fce1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 6 Jul 2023 18:43:34 +0100 Subject: Add if-conversion decision procedure --- src/Compiler.v | 9 +++++++-- src/hls/HTLgen.v | 12 ++++++------ src/hls/HTLgenproof.v | 12 ++++++------ src/hls/HTLgenspec.v | 8 ++++---- src/hls/IfConversion.v | 29 ++++++++++++++++++++++++++--- src/hls/IfConversionproof.v | 19 +++++++++++-------- 6 files changed, 60 insertions(+), 29 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index 2fb909e..49464c0 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -280,10 +280,15 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_GibleSeq 0) @@ total_if HLSOpts.optim_if_conversion CondElim.transf_program @@ print (print_GibleSeq 1) - @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (PTree.empty _ :: PTree.empty _ :: nil)) + (* @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (PTree.empty _ :: PTree.empty _ :: nil)) *) + @@ total_if HLSOpts.optim_if_conversion (IfConversion.transf_program (PTree.empty _)) @@ print (print_GibleSeq 2) - @@@ DeadBlocks.transf_program + @@ total_if HLSOpts.optim_if_conversion (IfConversion.transf_program (PTree.empty _)) @@ print (print_GibleSeq 3) + @@ total_if HLSOpts.optim_if_conversion (IfConversion.transf_program (PTree.empty _)) + @@ print (print_GibleSeq 4) + @@@ DeadBlocks.transf_program + @@ print (print_GibleSeq 5) @@@ GiblePargen.transl_program @@ print (print_GiblePar 0) @@@ HTLPargen.transl_program diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 6e632b8..0460e54 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -102,10 +102,10 @@ Export MonadNotation. #[local] Open Scope monad_scope. Definition state_goto (st : reg) (n : node) : stmnt := - Vnonblock (Vvar st) (Vlit (posToValue n)). + Vblock (Vvar st) (Vlit (posToValue n)). Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := - Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). + Vblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). Definition check_empty_node_datapath: forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. @@ -454,7 +454,7 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := List.map (fun a => match a with - (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) + (i, n) => (Vlit (natToValue i), Vblock (Vvar st) (Vlit (posToValue n))) end) (enumerate 0 ns). @@ -470,18 +470,18 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni if Z.leb (Z.pos n') Integers.Int.max_unsigned then do instr <- translate_instr op args; do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst instr) + add_instr n n' (block dst instr) else error (Errors.msg "State is larger than 2^32.") | Iload mem addr args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do src <- translate_arr_access mem addr args stack; do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst src) + add_instr n n' (block dst src) else error (Errors.msg "State is larger than 2^32.") | Istore mem addr args src n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + add_instr n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) else error (Errors.msg "State is larger than 2^32.") | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 4fc00bc..272a434 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -406,7 +406,7 @@ Section CORRECTNESS. Lemma op_stack_based : forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk, tr_instr fin rtrn st stk (RTL.Iop op args res0 pc') - (Verilog.Vnonblock (Verilog.Vvar res0) e) + (Verilog.Vblock (Verilog.Vvar res0) e) (state_goto st pc') -> reg_stack_based_pointers sp rs -> (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> @@ -1097,12 +1097,12 @@ rs assoc``. inv CONST; assumption. (* processing of state *) econstructor. - crush. - econstructor. - econstructor. - econstructor. + (* crush. *) + (* econstructor. *) + (* econstructor. *) + (* econstructor. *) - all: inv MARR; big_tac. Abort. + (* all: inv MARR; big_tac. *) Abort. (* inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 0259be9..7abdf82 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -142,7 +142,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall n op args dst s s' e i, Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> - tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) + tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vblock (Vvar dst) e) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, Z.pos n1 <= Int.max_unsigned -> @@ -160,12 +160,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall mem addr args s s' i c dst n, Z.pos n <= Int.max_unsigned -> 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) + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (block dst c) (state_goto st n) | tr_instr_Istore : forall mem addr args s s' i c src n, Z.pos n <= Int.max_unsigned -> 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)) + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src)) (state_goto st n). (* tr_instr_Ijumptable : forall cexpr tbl r, @@ -549,7 +549,7 @@ Proof. + 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. + + inversion H2. inversion H14. unfold block. replace (st_st s4) with (st_st s2) by congruence. econstructor. apply Z.leb_le; assumption. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 6693b82..8ca9cb6 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -98,13 +98,36 @@ Definition no_predicated_store bb := | _ => false end. -Definition decide_if_convert b_next := - (length b_next <=? 50)%nat && no_predicated_store b_next. +Definition gather_set_predicate (l: list positive) (i: instr): list positive := + match i with + | RBsetpred _ _ _ p => p::l + | _ => l + end. + +Definition gather_all_set_predicate i := + fold_left gather_set_predicate i nil. + +Definition gather_rbgoto (l: list positive) (i: instr): list positive := + match i with + | RBexit _ (RBgoto p) => p::l + | _ => l + end. + +Definition gather_all_rbgoto i := + fold_left gather_rbgoto i nil. + +Definition distinct_lists (l1 l2: list positive): bool := + forallb (fun x => negb (existsb (Pos.eqb x) l2)) l1. + +Definition decide_if_convert b_main b_next := + (length b_next <=? 50)%nat && no_predicated_store b_next + && distinct_lists (gather_all_set_predicate b_main) (gather_all_set_predicate b_next) + && distinct_lists (gather_all_rbgoto b_main) (gather_all_rbgoto b_next). Definition if_convert (orig_c c: code) (main next: node) := match orig_c ! main, orig_c ! next with | Some b_main, Some b_next => - if decide_if_convert b_next then + if decide_if_convert b_main b_next then PTree.set main (snd (replace_section (wrap_unit (if_convert_block next b_next)) tt b_main)) c else c | _, _ => c diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index f24a4c4..3c9d2bd 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -153,21 +153,24 @@ Proof. Qed. Lemma if_convert_decide_false : - forall pc pc' c b y, + forall pc pc' c b y x, c ! pc' = Some y -> - decide_if_convert y = false -> + c ! pc = Some x -> + decide_if_convert x y = false -> (if_convert c b pc pc') ! pc = b ! pc. Proof. unfold if_convert; intros. repeat (destruct_match; auto; []). - setoid_rewrite Heqo0 in H; crush. + setoid_rewrite Heqo0 in H. + setoid_rewrite Heqo in H0. + crush. Qed. Lemma if_convert_decide_true : forall pc pc' c b y z, c ! pc = Some z -> c ! pc' = Some y -> - decide_if_convert y = true -> + decide_if_convert z y = true -> (if_convert c b pc pc') ! pc = Some (snd (replace_section (wrap_unit (if_convert_block pc' y)) tt z)). Proof. unfold if_convert; intros. @@ -181,12 +184,12 @@ Lemma transf_spec_correct_in : (fold_left (fun s n => if_convert c s (fst n) (snd n)) l b) = c' -> b ! pc = Some z \/ (exists pc' y, c ! pc' = Some y - /\ decide_if_convert y = true + /\ decide_if_convert z y = true /\ b ! pc = Some (snd (replace_section (wrap_unit (if_convert_block pc' y)) tt z))) -> c ! pc = Some z -> c' ! pc = Some z \/ exists pc' y, c ! pc' = Some y - /\ decide_if_convert y = true + /\ decide_if_convert z y = true /\ c' ! pc = Some (snd (replace_section (wrap_unit (if_convert_block pc' y)) tt z)). Proof. induction l; crush. inv H0. tauto. @@ -196,7 +199,7 @@ Proof. destruct (peq p pc); [|left; rewrite <- H2; eapply if_convert_neq; eauto]; subst; []. destruct (c ! p0) eqn:?; [|left; rewrite <- H2; eapply if_convert_ne_pc'; eauto]; []. - destruct (decide_if_convert t) eqn:?; [|left; rewrite <- H2; eapply if_convert_decide_false; eauto]; []. + destruct (decide_if_convert z t) eqn:?; [|left; rewrite <- H2; eapply if_convert_decide_false; eauto]; []. right. do 2 econstructor; simplify; eauto. apply if_convert_decide_true; auto. @@ -207,7 +210,7 @@ Proof. destruct (c ! p0) eqn:?; [|do 2 econstructor; simplify; eauto; rewrite <- H3; eapply if_convert_ne_pc'; auto]; []. - destruct (decide_if_convert t) eqn:?; + destruct (decide_if_convert z t) eqn:?; [|do 2 econstructor; simplify; try eapply H; eauto; rewrite <- H3; eapply if_convert_decide_false; eauto]. do 2 econstructor; simplify; eauto. -- cgit