From e68848fc6970acc9b973a2c9dff5eddedb833914 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 2 Feb 2021 20:34:04 +0000
Subject: Add if conversion pass

---
 src/hls/IfConversion.v | 68 +++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 65 insertions(+), 3 deletions(-)

(limited to 'src/hls/IfConversion.v')

diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 2e200f8..9e600af 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -17,11 +17,15 @@
  *)
 
 Require Import compcert.common.AST.
-Require compcert.common.Errors.
-Require compcert.common.Globalenvs.
-Require compcert.lib.Integers.
+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.RTLBlock.
+
 (*|
 =============
 If conversion
@@ -30,3 +34,61 @@ 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.
 |*)
+
+Definition combine_pred (p: pred_op) (optp: option pred_op) :=
+  match optp with
+  | Some p' => Pand p p'
+  | None => p
+  end.
+
+Definition map_if_convert (p: pred_op) (i: instr) :=
+  match i with
+  | RBop p' op args dst => RBop (Some (combine_pred p p')) op args dst
+  | RBload p' chunk addr args dst =>
+    RBload (Some (combine_pred p p')) chunk addr args dst
+  | RBstore p' chunk addr args src =>
+    RBstore (Some (combine_pred p p')) chunk addr args src
+  | _ => i
+  end.
+
+Definition if_convert_block (c: code) (p: pred_op) (bb: bblock) : bblock :=
+  let cfi := bb_exit bb in
+  match cfi with
+  | RBcond cond args n1 n2 =>
+    match PTree.get n1 c, PTree.get n2 c with
+    | Some bb1, Some bb2 =>
+      let bb1' := List.map (map_if_convert p) bb1.(bb_body) in
+      let bb2' := List.map (map_if_convert (Pnot p)) bb2.(bb_body) in
+      mk_bblock (List.concat (bb.(bb_body) :: bb1' :: bb2' :: nil))
+                (RBpred_cf p bb1.(bb_exit) bb2.(bb_exit))
+    | _, _ => bb
+    end
+  | _ => bb
+  end.
+
+Definition is_cond_cfi (cfi: cf_instr) :=
+  match cfi with
+  | RBcond _ _ _ _ => true
+  | _ => false
+  end.
+
+Definition find_block_with_cond (c: code) : option (node * bblock) :=
+  match List.filter (fun x => is_cond_cfi (snd x).(bb_exit)) (PTree.elements c) with
+  | (a :: b)%list => Some a
+  | nil => None
+  end.
+
+Definition transf_function (f: function) : function :=
+  match find_block_with_cond f.(fn_code) with
+  | Some (n, bb) =>
+    let nbb := if_convert_block f.(fn_code) (Pvar 1%positive) bb in
+    mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize)
+               (PTree.set n nbb f.(fn_code)) f.(fn_entrypoint)
+  | None => f
+  end.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
-- 
cgit