Start work on reverse if-conversion

2 files changed, 84 insertions, 1 deletions

diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 9b8f4d4..1879205 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -30,7 +30,7 @@ Require Import vericert.bourdoncle.Bourdoncle.
 
 Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).
 
-(** * If conversion
+(** * If-Conversion
 
 This conversion is a verified conversion from RTLBlock back to itself, which performs if-conversion
 on basic blocks to make basic blocks larger.  *)
diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v
new file mode 100644
index 0000000..d6e926b
--- /dev/null
+++ b/src/hls/RICtransf.v
@@ -0,0 +1,83 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import compcert.common.AST.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.Predicate.
+
+(** * Reverse If-Conversion
+
+This transformation takes a scheduling RTLPar block and removes any predicates from it.  It can then
+be trivially transformed into linear code again.  It works by iteratively selecting a predicate,
+then creating a branch based on it and placing subsequent instructions in one branch or the other.
+*)
+
+Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B :=
+  match l with
+  | nil => None
+  | a :: l0 =>
+      match f a, existsb_val f l0 with
+      | _, Some v => Some v
+      | Some v, _ => Some v
+      | _, _ => None
+      end
+  end.
+
+Definition includes_setpred (bb: list (list instr)) :=
+  existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end)) bb.
+
+Definition add_bb (should_split: bool) (i: list (list instr))
+           (bbc: list (list (list instr)) * list (list (list instr))) :=
+  match bbc with
+  | (a, b) => if should_split then (a, i::b) else (i::a, b)
+  end.
+
+Fixpoint first_split (saw_pred: bool) (bb: bb) :=
+  match bb with
+  | a :: b =>
+      match includes_setpred a with
+      | Some v =>
+          let (_, res) := first_split true b in
+          (Some v, add_bb saw_pred a res)
+      | _ =>
+          let (v, res) := first_split saw_pred b in
+          (v, add_bb saw_pred a res)
+      end
+  | nil => (None, (nil, nil))
+  end.
+
+Definition split_bb (fresh: node) (b: bb) : bb * bb * bb :=
+  match first_split false b with
+  | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
+  | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
+  end.
+
+Definition transf_function (f: function) : function := f.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.