Add if-conversion decision procedure

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.