diff options
Diffstat (limited to 'src/hls/IfConversion.v')
-rw-r--r-- | src/hls/IfConversion.v | 51 |
1 files changed, 31 insertions, 20 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 4e62a68..1825ee7 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -23,8 +23,8 @@ 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. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSeq. Require Import vericert.hls.Predicate. Require Import vericert.bourdoncle.Bourdoncle. @@ -52,30 +52,39 @@ Definition map_if_convert (p: pred_op) (i: instr) := 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 + | RBsetpred p' c l pred => + RBsetpred (Some (combine_pred p p')) c l pred + | RBexit p' cf => RBexit (Some (combine_pred p p')) cf | _ => i end. -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 => +Definition get_unconditional_exit (bb: SeqBB.t) := List.nth_error bb (length bb - 1). + +Definition if_convert_block (c: code) (p: predicate) (bb: SeqBB.t) : SeqBB.t := + match get_unconditional_exit bb with + | Some (RBexit None (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 (Plit (true, p))) bb1.(bb_body) in - let bb2' := List.map (map_if_convert (Plit (false, p))) bb2.(bb_body) in - mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred None cond args p) :: bb1') :: bb2' :: nil)) - (RBpred_cf (Plit (true, p)) bb1.(bb_exit) bb2.(bb_exit)) + let bb1' := List.map (map_if_convert (Plit (true, p))) bb1 in + let bb2' := List.map (map_if_convert (Plit (false, p))) bb2 in + List.concat (bb :: ((RBsetpred None cond args p) :: bb1') :: bb2' :: nil) | _, _ => bb end | _ => bb end. -Definition is_cond_cfi (cfi: cf_instr) := +Definition is_cond_cfi' (cfi: cf_instr) := match cfi with | RBcond _ _ _ _ => true | _ => false end. +Definition is_cond_cfi (b: SeqBB.t) := + match get_unconditional_exit b with + | Some (RBexit None (RBcond _ _ _ _)) => true + | _ => false + end. + Fixpoint any {A: Type} (f: A -> bool) (a: list A) := match a with | x :: xs => f x || any f xs @@ -88,9 +97,9 @@ Fixpoint all {A: Type} (f: A -> bool) (a: list A) := | nil => true end. -Definition find_backedge (nb: node * bblock) := +Definition find_backedge (nb: node * SeqBB.t) := let (n, b) := nb in - let succs := successors_instr b.(bb_exit) in + let succs := all_successors b in filter (fun x => Pos.ltb n x) succs. Definition find_all_backedges (c: code) : list node := @@ -108,29 +117,31 @@ Fixpoint get_loops (b: bourdoncle): list node := Definition is_loop (b: list node) (n: node) := any (Pos.eqb n) b. -Definition is_flat_cfi (n: cf_instr) := +Definition is_flat_cfi' (n: cf_instr) := match n with | RBcond _ _ _ _ => false | RBjumptable _ _ => false - | RBpred_cf _ _ _ => false | _ => true end. +Definition is_flat_cfi (n: SeqBB.t) := + (length (all_successors n) =? 1)%nat. + Definition is_flat (c: code) (succ: node) := match c ! succ with - | Some bblock => is_flat_cfi bblock.(bb_exit) + | Some bblock => is_flat_cfi bblock | None => false end. -Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * bblock) := +Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * SeqBB.t) := let backedges := find_all_backedges c in - List.filter (fun x => is_cond_cfi (snd x).(bb_exit) && + List.filter (fun x => is_cond_cfi (snd x) && (negb (is_loop b (fst x)) || Pos.eqb (fst x) ep) && all (fun x' => is_flat c x') - (successors_instr (snd x).(bb_exit)) + (all_successors (snd x)) ) (PTree.elements c). -Definition if_convert_code (p: nat * code) (nb: node * bblock) := +Definition if_convert_code (p: nat * code) (nb: node * SeqBB.t) := let nbb := if_convert_block (snd p) (Pos.of_nat (fst p)) (snd nb) in (S (fst p), PTree.set (fst nb) nbb (snd p)). |