Add new if-conversion pass with top-level fold

3 files changed, 83 insertions, 65 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 1dc9826..5ff291e 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -139,6 +139,21 @@ Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop)
   : A -> A -> Prop :=
   if flag tt then R else eq.
 
+Definition match_rep {A: Type} (R: A -> A -> Prop): A -> A -> Prop :=
+  Relation_Operators.clos_refl_trans A R.
+
+Global Instance TransfIfLink {A: Type} {LA: Linker A}
+                      (transf: A -> A -> Prop) (TL: TransfLink transf)
+                      : TransfLink (match_rep transf).
+Admitted.
+
+Lemma total_rep_match:
+  forall (A B: Type) (n: list B) (f: A -> B -> A)
+         (rel: A -> A -> Prop) (prog: A),
+    (forall b p, rel p (f p b)) ->
+  match_rep rel prog (fold_left f n prog).
+Proof. Admitted.
+
 Lemma total_if_match:
   forall (A: Type) (flag: unit -> bool) (f: A -> A)
          (rel: A -> A -> Prop) (prog: A),
@@ -264,7 +279,7 @@ 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 IfConversion.transf_program
+   @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (Maps.PTree.empty _ :: Maps.PTree.empty _ :: nil))
    @@ print (print_GibleSeq 2)
   @@@ DeadBlocks.transf_program
    @@ print (print_GibleSeq 3)
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 9719ae6..6693b82 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -35,10 +35,9 @@ Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.Predicate.
 Require Import vericert.bourdoncle.Bourdoncle.
 
-Definition if_conv_t : Type := PTree.t (list (node * node)).
+Definition if_conv_t : Type := list (node * node).
 
 Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).
-Parameter get_if_conv_t : program -> list if_conv_t.
 
 #[local] Open Scope positive.
 
@@ -225,7 +224,7 @@ Definition ifconv_list (headers: list node) (c: code) :=
 Definition if_convert_code (c: code) iflist :=
   fold_left (fun s n => if_convert c s (fst n) (snd n)) iflist c.
 
-Definition transf_function (l: if_conv_t) (i: ident) (f: function) : function :=
+Definition transf_function (l: option if_conv_t) (f: function) : function :=
   let (b, _) := build_bourdoncle f in
   let b' := get_loops b in
   let iflist := ifconv_list b' f.(fn_code) in
@@ -235,28 +234,25 @@ Definition transf_function (l: if_conv_t) (i: ident) (f: function) : function :=
 
 Section TRANSF_PROGRAM.
 
-  Context {A B V: Type}.
-  Variable transf: ident -> A -> B.
+  Context {A B V DATA: Type}.
+  Variable transf: option DATA -> A -> B.
 
-  Definition transform_program_globdef' (idg: ident * globdef A V) : ident * globdef B V :=
+  Definition transform_program_globdef' (data: PTree.t DATA) (idg: ident * globdef A V) : ident * globdef B V :=
     match idg with
-    | (id, Gfun f) => (id, Gfun (transf id f))
+    | (id, Gfun f) => (id, Gfun (transf (data!id) f))
     | (id, Gvar v) => (id, Gvar v)
     end.
 
-  Definition transform_program' (p: AST.program A V) : AST.program B V :=
+  Definition transform_program_data (data: PTree.t DATA) (p: AST.program A V) : AST.program B V :=
     mkprogram
-      (List.map transform_program_globdef' p.(prog_defs))
+      (List.map (transform_program_globdef' data) p.(prog_defs))
       p.(prog_public)
           p.(prog_main).
 
 End TRANSF_PROGRAM.
 
-Definition transf_fundef (l: if_conv_t) (i: ident) (fd: fundef) : fundef :=
-  transf_fundef (transf_function l i) fd.
+Definition transf_fundef (l: option if_conv_t) (fd: fundef) : fundef :=
+  transf_fundef (transf_function l) fd.
 
-Definition transf_program_rec (p: program) (l: if_conv_t) : program :=
-  transform_program' (transf_fundef l) p.
-
-Definition transf_program (p: program) : program :=
-  fold_left transf_program_rec (get_if_conv_t p) p.
+Definition transf_program (l: PTree.t if_conv_t) (p: program) : program :=
+  transform_program_data transf_fundef l p.
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index 70d5fe3..e13db00 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -50,8 +50,8 @@ Require Import vericert.hls.Predicate.
 
 Variant match_stackframe : stackframe -> stackframe -> Prop :=
   | match_stackframe_init :
-    forall res f tf sp pc rs p l i
-           (TF: transf_function l i f = tf),
+    forall res f tf sp pc rs p l
+           (TF: transf_function l f = tf),
       match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p).
 
 Definition bool_order (b: bool): nat := if b then 1 else 0.
@@ -231,8 +231,8 @@ Proof.
 Qed.
 
 Lemma transf_spec_correct :
-  forall f pc l i,
-    if_conv_spec f.(fn_code) (transf_function l i f).(fn_code) pc.
+  forall f pc l,
+    if_conv_spec f.(fn_code) (transf_function l f).(fn_code) pc.
 Proof.
   intros; unfold transf_function; destruct_match; cbn.
   unfold if_convert_code.
@@ -306,8 +306,8 @@ Section CORRECTNESS.
 
   Variant match_states : option SeqBB.t -> state -> state -> Prop :=
     | match_state_some :
-      forall stk stk' f tf sp pc rs p m b pc0 rs0 p0 m0 l i
-             (TF: transf_function l i f = tf)
+      forall stk stk' f tf sp pc rs p m b pc0 rs0 p0 m0 l
+             (TF: transf_function l f = tf)
              (STK: Forall2 match_stackframe stk stk')
              (* This can be improved with a recursive relation for a more general structure of the
                 if-conversion proof. *)
@@ -319,13 +319,13 @@ Section CORRECTNESS.
              (SIM: step ge (State stk f sp pc0 rs0 p0 m0) E0 (State stk f sp pc rs p m)),
         match_states (Some b) (State stk f sp pc rs p m) (State stk' tf sp pc0 rs0 p0 m0)
     | match_state_none :
-      forall stk stk' f tf sp pc rs p m l i
-             (TF: transf_function l i f = tf)
+      forall stk stk' f tf sp pc rs p m l
+             (TF: transf_function l f = tf)
              (STK: Forall2 match_stackframe stk stk'),
         match_states None (State stk f sp pc rs p m) (State stk' tf sp pc rs p m)
     | match_callstate :
-      forall cs cs' f tf args m l i
-             (TF: transf_fundef l i f = tf)
+      forall cs cs' f tf args m l
+             (TF: transf_fundef l f = tf)
              (STK: Forall2 match_stackframe cs cs'),
         match_states None (Callstate cs f args m) (Callstate cs' tf args m)
     | match_returnstate :
@@ -334,46 +334,51 @@ Section CORRECTNESS.
         match_states None (Returnstate cs v m) (Returnstate cs' v m).
 
   Definition match_prog (p: program) (tp: program) :=
-    Linking.match_program (fun cu f tf => forall l i, tf = transf_fundef l i f) eq p tp.
+    match_program (fun _ f tf => exists l, transf_fundef l f = tf) eq p tp.
 
   Context (TRANSL : match_prog prog tprog).
 
   Lemma symbols_preserved:
     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-  Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+  Proof using TRANSL.
+    intros. eapply (Genv.find_symbol_match TRANSL).
+  Qed.
 
   Lemma senv_preserved:
     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
   Proof using TRANSL.
-    Admitted.
-    (*intros; eapply (Genv.senv_transf TRANSL). Qed.*)
+    intros; eapply (Genv.senv_match TRANSL).
+  Qed.
 
   Lemma function_ptr_translated:
-    forall b f l i,
+    forall b f l,
       Genv.find_funct_ptr ge b = Some f ->
-      Genv.find_funct_ptr tge b = Some (transf_fundef l i f).
-  Proof. Admitted.
+      Genv.find_funct_ptr tge b = Some (transf_fundef l f).
+  Proof.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    crush.
+  Qed.
 
   Lemma sig_transf_function:
-    forall (f tf: fundef) l i,
-      funsig (transf_fundef l i f) = funsig f.
+    forall (f tf: fundef) l,
+      funsig (transf_fundef l f) = funsig f.
   Proof using.
     unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f.
     unfold transf_function. destruct_match. auto. auto.
   Qed.
 
   Lemma functions_translated:
-    forall (v: Values.val) (f: GibleSeq.fundef) l i,
+    forall (v: Values.val) (f: GibleSeq.fundef) l,
       Genv.find_funct ge v = Some f ->
-      Genv.find_funct tge v = Some (transf_fundef l i f).
+      Genv.find_funct tge v = Some (transf_fundef l f).
   Proof using TRANSL.
     intros. exploit (Genv.find_funct_match TRANSL); eauto. simplify. eauto.
-    Admitted.
+  Qed.
 
   Lemma find_function_translated:
-    forall ros rs f l i,
+    forall ros rs f l,
       find_function ge ros rs = Some f ->
-      find_function tge ros rs = Some (transf_fundef l i f).
+      find_function tge ros rs = Some (transf_fundef l f).
   Proof using TRANSL.
     Ltac ffts := match goal with
                  | [ H: forall _, Val.lessdef _ _, r: Registers.reg |- _ ] =>
@@ -398,11 +403,12 @@ Section CORRECTNESS.
     induction 1.
     exploit function_ptr_translated; eauto; intros.
     do 2 econstructor; simplify. econstructor.
-    (*apply (Genv.init_mem_transf TRANSL); eauto.
+    apply (Genv.init_mem_match TRANSL); eauto.
     replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto.
     symmetry; eapply Linking.match_program_main; eauto. eauto.
-    erewrite sig_transf_function; eauto. constructor. auto. auto.
-  Qed.*) Admitted.
+    erewrite sig_transf_function; eauto. econstructor. auto. auto.
+    Unshelve. exact None.
+  Qed.
 
   Lemma transf_final_states :
     forall s1 s2 r b,
@@ -498,8 +504,8 @@ Section CORRECTNESS.
   Qed.
 
   Lemma fn_all_eq :
-    forall f tf l i,
-      transf_function l i f = tf ->
+    forall f tf l,
+      transf_function l f = tf ->
       fn_stacksize f = fn_stacksize tf
       /\ fn_sig f = fn_sig tf
       /\ fn_params f = fn_params tf
@@ -512,16 +518,16 @@ Section CORRECTNESS.
 
   Ltac func_info :=
     match goal with
-      H: transf_function _ _ _ = _ |- _ =>
+      H: transf_function _ _ = _ |- _ =>
         let H2 := fresh "ALL_EQ" in
-        pose proof (fn_all_eq _ _ _ _ H) as H2; simplify
+        pose proof (fn_all_eq _ _ _ H) as H2; simplify
     end.
 
   Lemma step_cf_eq :
-    forall stk stk' f tf sp pc rs pr m cf s t pc' l i,
+    forall stk stk' f tf sp pc rs pr m cf s t pc' l,
       step_cf_instr ge (State stk f sp pc rs pr m) cf t s ->
       Forall2 match_stackframe stk stk' ->
-      transf_function l i f = tf ->
+      transf_function l f = tf ->
       exists s', step_cf_instr tge (State stk' tf sp pc' rs pr m) cf t s'
                  /\ match_states None s s'.
   Proof.
@@ -534,7 +540,8 @@ Section CORRECTNESS.
       rewrite H2 in *. rewrite H12. auto. econstructor; auto.
     - func_info. do 2 econstructor. econstructor; eauto. rewrite H2 in *.
       eauto. econstructor; auto.
-  Admitted.
+    Unshelve. all: exact None.
+  Qed.
 
   Definition cf_dec :
     forall a pc, {a = RBgoto pc} + {a <> RBgoto pc}.
@@ -768,19 +775,19 @@ Section CORRECTNESS.
   Qed.
 
   Lemma match_none_correct :
-    forall t s1' stk f sp pc rs m pr rs' m' bb pr' cf stk' l i,
+    forall t s1' stk f sp pc rs m pr rs' m' bb pr' cf stk' l,
       (fn_code f) ! pc = Some bb ->
       SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
       step_cf_instr ge (State stk f sp pc rs' pr' m') cf t s1' ->
       Forall2 match_stackframe stk stk' ->
       exists b' s2',
-        (plus step tge (State stk' (transf_function l i f) sp pc rs pr m) t s2' \/
-           star step tge (State stk' (transf_function l i f) sp pc rs pr m) t s2'
+        (plus step tge (State stk' (transf_function l f) sp pc rs pr m) t s2' \/
+           star step tge (State stk' (transf_function l f) sp pc rs pr m) t s2'
            /\ ltof (option SeqBB.t) measure b' None) /\
           match_states b' s1' s2'.
   Proof.
     intros * H H0 H1 STK.
-    pose proof (transf_spec_correct f pc l i) as X; inv X.
+    pose proof (transf_spec_correct f pc l) as X; inv X.
     - apply sim_plus. rewrite H in H2. symmetry in H2.
       exploit step_cf_eq; eauto; simplify.
       do 3 econstructor. apply plus_one. econstructor; eauto.
@@ -790,7 +797,7 @@ Section CORRECTNESS.
       destruct (cf_wf_dec x b' cf pc'); subst; simplify.
       + inv H1.
         exploit exec_if_conv; eauto; simplify.
-        apply sim_star. exists (Some b'). exists (State stk' (transf_function l i f) sp pc rs pr m).
+        apply sim_star. exists (Some b'). exists (State stk' (transf_function l f) sp pc rs pr m).
         simplify; try (unfold ltof; auto). apply star_refl.
         econstructor; auto.
         simplify. econstructor; eauto.
@@ -810,21 +817,21 @@ Section CORRECTNESS.
   Qed.
 
   Lemma match_some_correct:
-    forall t s1' s f sp pc rs m pr rs' m' bb pr' cf stk' b0 pc1 rs1 p0 m1 l i,
+    forall t s1' s f sp pc rs m pr rs' m' bb pr' cf stk' b0 pc1 rs1 p0 m1 l,
       step ge (State s f sp pc rs pr m) t s1' ->
       (fn_code f) ! pc = Some bb ->
       SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
       step_cf_instr ge (State s f sp pc rs' pr' m') cf t s1' ->
       Forall2 match_stackframe s stk' ->
       (fn_code f) ! pc = Some b0 ->
-      sem_extrap (transf_function l i f) pc1 sp (Iexec (mki rs pr m)) (Iexec (mki rs1 p0 m1)) b0 ->
+      sem_extrap (transf_function l f) pc1 sp (Iexec (mki rs pr m)) (Iexec (mki rs1 p0 m1)) b0 ->
       (forall b',
           f.(fn_code)!pc1 = Some b' ->
-          exists tb, (transf_function l i f).(fn_code)!pc1 = Some tb /\ if_conv_replace pc b0 b' tb) ->
+          exists tb, (transf_function l f).(fn_code)!pc1 = Some tb /\ if_conv_replace pc b0 b' tb) ->
       step ge (State s f sp pc1 rs1 p0 m1) E0 (State s f sp pc rs pr m) ->
       exists b' s2',
-        (plus step tge (State stk' (transf_function l i f) sp pc1 rs1 p0 m1) t s2' \/
-           star step tge (State stk' (transf_function l i f) sp pc1 rs1 p0 m1) t s2' /\
+        (plus step tge (State stk' (transf_function l f) sp pc1 rs1 p0 m1) t s2' \/
+           star step tge (State stk' (transf_function l f) sp pc1 rs1 p0 m1) t s2' /\
              ltof (option SeqBB.t) measure b' (Some b0)) /\ match_states b' s1' s2'.
   Proof.
     intros * H H0 H1 H2 STK IS_B EXTRAP IS_TB SIM.
@@ -853,17 +860,17 @@ Section CORRECTNESS.
       match goal with H: context[match_states] |- _ => inv H end.
     - eauto using match_some_correct.
     - eauto using match_none_correct.
-    - apply sim_plus. remember (transf_function l i f) as tf. symmetry in Heqtf. func_info.
+    - apply sim_plus. remember (transf_function l f) as tf. symmetry in Heqtf. func_info.
       exists None. eexists. split.
       apply plus_one. constructor; eauto. rewrite <- H1. eassumption.
       rewrite <- H4. rewrite <- H2. econstructor; auto.
     - apply sim_plus. exists None. eexists. split.
       apply plus_one. constructor; eauto.
       constructor; auto.
-(*    - apply sim_plus. remember (transf_function l i f) as tf. symmetry in Heqtf. func_info.
+   - apply sim_plus. remember (transf_function None f) as tf. symmetry in Heqtf. func_info.
       exists None. inv STK. inv H7. eexists. split. apply plus_one. constructor.
-      constructor; auto.
-  Qed.*) Admitted.
+      econstructor; auto.
+  Qed.
 
   Theorem transf_program_correct:
     forward_simulation (semantics prog) (semantics tprog).