diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 2 | ||||
-rw-r--r-- | src/bourdoncle/BourdoncleAux.ml | 31 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 10 | ||||
-rw-r--r-- | src/hls/IfConversion.v | 36 | ||||
-rw-r--r-- | src/hls/Pipeline.v | 3 | ||||
-rw-r--r-- | src/hls/PipelineOp.v | 3 | ||||
-rw-r--r-- | src/hls/Schedule.ml | 5 |
7 files changed, 63 insertions, 27 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index e4ab607..b907629 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -67,7 +67,7 @@ Require vericert.hls.RTLBlockgen. Require vericert.hls.RTLPargen. Require vericert.hls.RTLParFUgen. Require vericert.hls.HTLPargen. -Require vericert.hls.Pipeline. +(*Require vericert.hls.Pipeline.*) Require vericert.hls.IfConversion. (*Require vericert.hls.PipelineOp.*) Require vericert.HLSOpts. diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml index 3c7fd58..a35004e 100644 --- a/src/bourdoncle/BourdoncleAux.ml +++ b/src/bourdoncle/BourdoncleAux.ml @@ -4,7 +4,8 @@ open Camlcoq open BinNums open BinPos open Maps -open RTL +open RTLBlock +open RTLBlockInstr open BourdoncleIterator module B = Bourdoncle @@ -38,25 +39,23 @@ let bourdoncleListToString (l : B.bourdoncle list) : string = (* Dummy type to avoid redefining existing functions *) type instr = | Inop +let rec get_exits = function + | RBgoto j -> [(int_of_positive j, Inop)] + | RBcall (_,_,_,dst,j) -> [(int_of_positive j, Inop)] + | RBtailcall _ -> [] + | RBbuiltin (_,_,dst,j) -> [(int_of_positive j, Inop)] + | RBcond (c,args,j,k) -> [(int_of_positive j, Inop);(int_of_positive k, Inop)] + | RBjumptable (_,tbl) -> List.map (fun j -> (int_of_positive j, Inop)) tbl + | RBpred_cf (p, cf1, cf2) -> List.append (get_exits cf1) (get_exits cf2) + | RBreturn _ -> [] + let build_cfg f = let entry = int_of_positive f.fn_entrypoint in let max = PTree.fold (fun m n _ -> max m (int_of_positive n)) f.fn_code 0 in (* nodes are between 1 and max+1 *) let succ = Array.make (max+1) [] in let _ = PTree.fold (fun () n ins -> - succ.(int_of_positive n) <- - let inop : instr = Inop in - match ins with - | RTL.Inop j -> [(int_of_positive j, inop)] - | RTL.Iop (op,args,dst,j) -> [(int_of_positive j, Inop)] - | RTL.Iload (_,_,_,dst,j) -> [(int_of_positive j, Inop)] - | RTL.Istore (_,_,_,_,j) -> [(int_of_positive j, Inop)] - | RTL.Icall (_,_,_,dst,j) -> [(int_of_positive j, Inop)] - | RTL.Itailcall _ -> [] - | RTL.Ibuiltin (_,_,dst,j) -> [(int_of_positive j, Inop)] - | RTL.Icond (c,args,j,k) -> [(int_of_positive j, Inop);(int_of_positive k, Inop)] - | RTL.Ijumptable (_,tbl) -> List.map (fun j -> (int_of_positive j, inop)) tbl - | RTL.Ireturn _ -> []) f.fn_code () in + succ.(int_of_positive n) <- get_exits ins.bb_exit) f.fn_code () in { entry = entry; succ = succ } let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list = @@ -66,7 +65,7 @@ let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list = | (L ((I h) :: l, _)) :: r -> B.L (positive_of_int h, build_bourdoncle' l) :: (build_bourdoncle' r) | _ -> failwith "Assertion error: invalid bourdoncle ist" -let build_bourdoncle'' (f : coq_function) : B.bourdoncle = +let build_bourdoncle'' (f : bb coq_function) : B.bourdoncle = let cfg = build_cfg f in match build_bourdoncle' (get_bourdoncle cfg) with | [] -> failwith "assertion error: empty bourdoncle" @@ -103,7 +102,7 @@ let build_order (b : B.bourdoncle) : coq_N PMap.t = let bo = build_order' (linearize b) (succ_pos N0) in (succ_pos N0, bo) -let build_bourdoncle (f : coq_function) : (B.bourdoncle * coq_N PMap.t) = +let build_bourdoncle (f : bb coq_function) : (B.bourdoncle * coq_N PMap.t) = let b = build_bourdoncle'' f in let bo = build_order b in (b, bo) diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 9b82e1b..395ec47 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -24,9 +24,10 @@ From vericert Require RTLPar RTLBlockInstr HTLgen - Pipeline + (*Pipeline*) HLSOpts Predicate + Bourdoncle . From Coq Require DecidableClass. @@ -182,10 +183,13 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false". Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". -Extract Constant Pipeline.pipeline => "pipelining.pipeline". +(*Extract Constant Pipeline.pipeline => "pipelining.pipeline".*) Extract Constant RTLBlockgen.partition => "Partition.partition". Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". +(* Loop normalization *) +Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". + (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -195,9 +199,9 @@ Separate Extraction vericert.Compiler.transf_hls_temp RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr - Pipeline.pipeline Predicate.sat_pred_simple Verilog.stmnt_to_list + Bourdoncle.bourdoncle Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index b397d43..4585770 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -26,6 +26,9 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. Require Import vericert.hls.Predicate. +Require Import vericert.bourdoncle.Bourdoncle. + +Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N). (*| ============= @@ -96,11 +99,34 @@ Definition find_all_backedges (c: code) : list node := 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) := +Fixpoint get_loops (b: bourdoncle): list node := + match b with + | L h b' => h::(fold_right (fun a b => get_loops a ++ b) nil b') + | I h => nil + end. + +Definition is_loop (b: list node) (n: node) := + any (fun x => Pos.eqb x n) b. + +Definition is_flat_cfi (n: cf_instr) := + match n with + | RBcond _ _ _ _ => false + | RBjumptable _ _ => false + | RBpred_cf _ _ _ => false + | _ => true + end. + +Definition is_flat (c: code) (succ: node) := + match c ! succ with + | Some bblock => is_flat_cfi bblock.(bb_exit) + | None => false + end. + +Definition find_blocks_with_cond ep (b: list node) (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)) + (negb (is_loop b (fst x)) || Pos.eqb (fst x) ep) && + all (fun x' => is_flat c x') (successors_instr (snd x).(bb_exit)) ) (PTree.elements c). @@ -109,8 +135,10 @@ Definition if_convert_code (p: nat * code) (nb: node * bblock) := (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_code)) + (find_blocks_with_cond f.(fn_entrypoint) b' f.(fn_code)) (1%nat, f.(fn_code)) in mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint). diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v index 7f1485a..67ab1f5 100644 --- a/src/hls/Pipeline.v +++ b/src/hls/Pipeline.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import compcert.lib.Maps. +(*Require Import compcert.lib.Maps. Require Import compcert.common.AST. Require Import compcert.backend.RTL. @@ -26,3 +26,4 @@ Definition transf_fundef := transf_fundef pipeline. Definition transf_program : program -> program := transform_program transf_fundef. +*) diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v index 793b752..bb01ff9 100644 --- a/src/hls/PipelineOp.v +++ b/src/hls/PipelineOp.v @@ -79,7 +79,7 @@ Definition map_at_err {A: Type} (n: nat) (f: A -> A) (l: list A): option (list A then None else Some (map_at n f l). -Definition replace_div' sdiv udiv (d: instr) := +(*Definition replace_div' sdiv udiv (d: instr) := match d with | RBop op Odiv args dst => RBpiped op sdiv args | RBop op Odivu args dst => RBpiped op udiv args @@ -190,3 +190,4 @@ Definition transf_fundef (fd: fundef) : fundef := Definition transf_program (p: program) : program := transform_program transf_fundef p. +*) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index e557d4b..1969cad 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -637,7 +637,10 @@ let add_cycle_constr maxf n dfg constr = - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int maxf))) - 1), encode_var n (fst v') 0) ) constr (DFG.fold_vertex (fun v l -> - List.append l (longest_path v |> constrained_paths |> List.map (function (v', w) -> (v, v', - w))) + List.append l (longest_path v (*|> (function l -> List.iter (function (a, x) -> + printf "c: %d %d\n" (fst a) x) l; l)*) |> constrained_paths (* |> (function l -> List.iter (function (a, x) -> + printf "%d %d\n" (fst a) x) l; l)*) + |> List.map (function (v', w) -> (v, v', - w))) ) dfg []) type resource = |