Update if-conversion function

2 files changed, 10 insertions, 3 deletions

diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 53ca944..92702e8 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -80,10 +80,13 @@ Definition no_predicated_store bb :=
   | _ => false
   end.
 
-Definition if_convert (c: code) (main next: node) :=
-  match c ! main, c ! next with
+Definition decide_if_convert b_next :=
+  (length b_next <=? 50)%nat && no_predicated_store 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 (length b_next <=? 50)%nat && no_predicated_store b_next then
+      if decide_if_convert b_next then
         PTree.set main (snd (replace_section (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 51a2841..6071d9e 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -40,6 +40,10 @@ Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.IfConversion.
 Require Import vericert.hls.Predicate.
 
+#[local] Opaque decide_if_convert.
+#[local] Opaque get_loops.
+#[local] Opaque ifconv_list.
+
 #[local] Open Scope positive.
 #[local] Notation "'mki'" := (mk_instr_state) (at level 1).