From 538e3a285010fe16e459268c516c22d770aabe71 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 31 May 2022 02:04:08 +0100 Subject: Simplify if-conversion pass --- src/hls/IfConversion.v | 110 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 80 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 1825ee7..961182c 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -16,6 +16,9 @@ * along with this program. If not, see . *) +Require Import Coq.Structures.Orders. +Require Import Coq.Sorting.Mergesort. + Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Globalenvs. @@ -39,40 +42,64 @@ This conversion is a verified conversion from RTLBlock back to itself, which performs if-conversion on basic blocks to make basic blocks larger. |*) -Definition combine_pred (p: pred_op) (optp: option pred_op) := - match optp with - | Some p' => Pand p p' - | None => p - end. - -Definition map_if_convert (p: pred_op) (i: instr) := +Definition map_if_convert (p: option pred_op) (i: instr) := match i with - | RBop p' op args dst => RBop (Some (combine_pred p p')) op args dst + | RBop p' op args dst => RBop (combine_pred p p') op args dst | RBload p' chunk addr args dst => - RBload (Some (combine_pred p p')) chunk addr args dst + RBload (combine_pred p p') chunk addr args dst | RBstore p' chunk addr args src => - RBstore (Some (combine_pred p p')) chunk addr args src + RBstore (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 + RBsetpred (combine_pred p p') c l pred + | RBexit p' cf => RBexit (combine_pred p p') cf | _ => i end. -Definition get_unconditional_exit (bb: SeqBB.t) := List.nth_error bb (length bb - 1). +Definition if_convert_block (next: node) (b_next: SeqBB.t) (u: unit) (i: instr) := + match i with + | RBexit p (RBgoto next') => + if (next =? next')%positive + then (u, map (map_if_convert p) b_next) + else (u, i::nil) + | _ => (u, i::nil) + end. -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 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 +Definition predicated_store i := + match i with + | RBstore _ _ _ _ _ => true + | _ => false end. +Definition no_predicated_store bb := + match filter predicated_store bb with + | nil => true + | _ => false + end. + +Definition if_convert (c: code) (main next: node) := + match c ! main, c ! next with + | Some b_main, Some b_next => + if (length b_next <=? 50)%nat && no_predicated_store b_next then + PTree.set main (snd (replace_section (if_convert_block next b_next) tt b_main)) c + else c + | _, _ => c + end. + +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 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) := match cfi with | RBcond _ _ _ _ => true @@ -141,16 +168,39 @@ Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * SeqB (all_successors (snd x)) ) (PTree.elements c). -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)). +Module TupOrder <: TotalLeBool. + Definition t : Type := positive * positive. + Definition leb (x y: t) := (fst x <=? fst y)%positive. + Infix "<=?" := leb (at level 70, no associativity). + Theorem leb_total : forall a1 a2, (a1 <=? a2) = true \/ (a2 <=? a1) = true. + Proof. unfold leb; intros; repeat rewrite Pos.leb_le; lia. Qed. +End TupOrder. + +Module Import TupSort := Sort TupOrder. + +Definition ifconv_list (headers: list node) (c: code) := + let all_succ := PTree.fold (fun l n i => (n, all_successors i) :: l) c nil in + let filtered := filter (fun x => match x with (_, l) => (length l <=? 2)%nat end) all_succ in + let expanded := + fold_left (fun l (e: node * list node) => + let (e1, e2) := e in + map (fun x => (e1, x)) e2 ++ l + ) filtered nil in + let filtered2 := filter (fun x: node * node => + let (x1, x2) := x in + negb (is_loop headers x2) + ) expanded in + sort filtered2. + +(* 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)). *) Definition transf_function (f: function) : function := let (b, _) := build_bourdoncle f in let b' := get_loops b in - let (_, c) := List.fold_left if_convert_code - (find_blocks_with_cond f.(fn_entrypoint) b' f.(fn_code)) - (1%nat, f.(fn_code)) in + let iflist := ifconv_list b' f.(fn_code) in + let c := fold_left (fun c n => if_convert c (fst n) (snd n)) iflist f.(fn_code) in mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := -- cgit