From 8d5047ca436ba42e9253d24d6b5b2c0c62dd7437 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 3 Feb 2021 01:05:32 +0000 Subject: Fix state generation for if-conversion --- src/hls/IfConversion.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/hls/IfConversion.v') 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 -- cgit