Fix state generation for if-conversion

1 files changed, 6 insertions, 6 deletions

diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 9e600af..943e1a8 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -51,16 +51,16 @@ Definition map_if_convert (p: pred_op) (i: instr) :=
   | _ => i
   end.
 
-Definition if_convert_block (c: code) (p: pred_op) (bb: bblock) : bblock :=
+Definition if_convert_block (c: code) (p: predicate) (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))
+      let bb1' := List.map (map_if_convert (Pvar p)) bb1.(bb_body) in
+      let bb2' := List.map (map_if_convert (Pnot (Pvar p))) bb2.(bb_body) in
+      mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred cond args p) :: bb1') :: bb2' :: nil))
+                (RBpred_cf (Pvar p) bb1.(bb_exit) bb2.(bb_exit))
     | _, _ => bb
     end
   | _ => bb
@@ -81,7 +81,7 @@ Definition find_block_with_cond (c: code) : option (node * bblock) :=
 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
+    let nbb := if_convert_block f.(fn_code) 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