diff options
Diffstat (limited to 'src/hls/IfConversion.v')
-rw-r--r-- | src/hls/IfConversion.v | 50 |
1 files changed, 39 insertions, 11 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 943e1a8..39d9fd2 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -72,21 +72,49 @@ Definition is_cond_cfi (cfi: cf_instr) := | _ => 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 +Fixpoint any {A: Type} (f: A -> bool) (a: list A) := + match a with + | x :: xs => f x || any f xs + | nil => false 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) 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 +Fixpoint all {A: Type} (f: A -> bool) (a: list A) := + match a with + | x :: xs => f x && all f xs + | nil => true end. +Definition find_backedge (nb: node * bblock) := + let (n, b) := nb in + let succs := successors_instr b.(bb_exit) in + filter (fun x => Pos.ltb n x) succs. + +Definition find_all_backedges (c: code) : list node := + List.concat (List.map find_backedge (PTree.elements c)). + +Definition has_backedge (entry: node) (be: list node) := + any (fun x => Pos.eqb entry x) be. + +Definition find_blocks_with_cond (c: code) : list (node * bblock) := + let backedges := find_all_backedges c in + List.filter (fun x => is_cond_cfi (snd x).(bb_exit) && + negb (has_backedge (fst x) backedges) && + all (fun x' => negb (has_backedge x' backedges)) + (successors_instr (snd x).(bb_exit)) + ) (PTree.elements c). + +Definition if_convert_code (p: nat * code) (nb: node * bblock) := + let (n, bb) := nb in + let (p', c) := p in + let nbb := if_convert_block c p' bb in + (S p', PTree.set n nbb c). + +Definition transf_function (f: function) : function := + let (_, c) := List.fold_left if_convert_code + (find_blocks_with_cond f.(fn_code)) + (1%nat, f.(fn_code)) in + mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint). + Definition transf_fundef (fd: fundef) : fundef := transf_fundef transf_function fd. |