diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 20 | ||||
-rw-r--r-- | src/VericertClflags.ml | 4 | ||||
-rw-r--r-- | src/bourdoncle/BourdoncleAux.ml | 13 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 20 | ||||
-rw-r--r-- | src/hls/Abstr.v | 126 | ||||
-rw-r--r-- | src/hls/Gible.v | 49 | ||||
-rw-r--r-- | src/hls/GiblePar.v | 21 | ||||
-rw-r--r-- | src/hls/GiblePargen.v (renamed from src/hls/RTLPargen.v) | 62 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v (renamed from src/hls/RTLPargenproof.v) | 11 | ||||
-rw-r--r-- | src/hls/GibleSeq.v | 19 | ||||
-rw-r--r-- | src/hls/GibleSeqgen.v | 2 | ||||
-rw-r--r-- | src/hls/GibleSeqgenproof.v | 26 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 182 | ||||
-rw-r--r-- | src/hls/IfConversion.v | 51 | ||||
-rw-r--r-- | src/hls/Partition.ml | 27 | ||||
-rw-r--r-- | src/hls/PipelineOp.v | 8 | ||||
-rw-r--r-- | src/hls/PrintGible.ml (renamed from src/hls/PrintRTLBlockInstr.ml) | 55 | ||||
-rw-r--r-- | src/hls/PrintGiblePar.ml (renamed from src/hls/PrintRTLPar.ml) | 10 | ||||
-rw-r--r-- | src/hls/PrintGibleSeq.ml (renamed from src/hls/PrintRTLBlock.ml) | 10 | ||||
-rw-r--r-- | src/hls/PrintRTLParFU.ml | 120 | ||||
-rw-r--r-- | src/hls/RICtransf.v | 86 | ||||
-rw-r--r-- | src/hls/RTLParFUgen.v | 24 | ||||
-rw-r--r-- | src/hls/Schedule.ml | 66 |
23 files changed, 366 insertions, 646 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index dc3b1c7..a0b3f24 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -62,8 +62,7 @@ Require vericert.hls.Veriloggenproof. Require vericert.hls.HTLgen. Require vericert.hls.GibleSeq. Require vericert.hls.GibleSeqgen. -Require vericert.hls.RTLPargen. -Require vericert.hls.RTLParFUgen. +Require vericert.hls.GiblePargen. Require vericert.hls.HTLPargen. (*Require vericert.hls.Pipeline.*) Require vericert.hls.IfConversion. @@ -84,9 +83,8 @@ intermediate steps in the compilation, such as ``print_RTL``, ``print_HTL`` and Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: Z -> HTL.program -> unit. -Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. -Parameter print_RTLPar: Z -> RTLPar.program -> unit. -Parameter print_RTLParFU: Z -> RTLParFU.program -> unit. +Parameter print_GibleSeq: Z -> GibleSeq.GibleSeq.program -> unit. +Parameter print_GiblePar: Z -> GiblePar.GiblePar.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -260,14 +258,12 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_RTL 6) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) - @@@ RTLBlockgen.transl_program - @@ print (print_RTLBlock 0) + @@@ GibleSeqgen.transl_program + @@ print (print_GibleSeq 0) @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program - @@ print (print_RTLBlock 1) - @@@ RTLPargen.transl_program - @@ print (print_RTLPar 0) - @@@ RTLParFUgen.transl_program - @@ print (print_RTLParFU 0) + @@ print (print_GibleSeq 1) + @@@ GiblePargen.transl_program + @@ print (print_GiblePar 0) @@@ HTLPargen.transl_program @@ print (print_HTL 0) @@ Veriloggen.transl_program. diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml index 0402d49..9dccb53 100644 --- a/src/VericertClflags.ml +++ b/src/VericertClflags.ml @@ -4,8 +4,8 @@ let option_hls = ref true let option_debug_hls = ref false let option_initial = ref false let option_dhtl = ref false -let option_drtlblock = ref false -let option_drtlpar = ref false +let option_dgblseq = ref false +let option_dgblpar = ref false let option_drtlparfu = ref false let option_hls_schedule = ref false let option_fif_conv = ref false diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml index a35004e..1ea4de6 100644 --- a/src/bourdoncle/BourdoncleAux.ml +++ b/src/bourdoncle/BourdoncleAux.ml @@ -4,8 +4,9 @@ open Camlcoq open BinNums open BinPos open Maps -open RTLBlock -open RTLBlockInstr +open Gible +open GibleSeq +open GibleSeq open BourdoncleIterator module B = Bourdoncle @@ -46,7 +47,6 @@ let rec get_exits = function | 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 = @@ -55,7 +55,8 @@ let build_cfg f = (* 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) <- get_exits ins.bb_exit) f.fn_code () in + succ.(int_of_positive n) <- List.map (fun j -> (int_of_positive j, Inop)) + (all_successors ins)) f.fn_code () in { entry = entry; succ = succ } let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list = @@ -65,7 +66,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 : bb coq_function) : B.bourdoncle = +let build_bourdoncle'' (f : coq_function) : B.bourdoncle = let cfg = build_cfg f in match build_bourdoncle' (get_bourdoncle cfg) with | [] -> failwith "assertion error: empty bourdoncle" @@ -102,7 +103,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 : bb coq_function) : (B.bourdoncle * coq_N PMap.t) = +let build_bourdoncle (f : 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 395ec47..88bb3e8 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -19,10 +19,10 @@ From vericert Require Verilog Compiler - RTLBlockgen - RTLBlock - RTLPar - RTLBlockInstr + GibleSeqgen + GibleSeq + GiblePar + Gible HTLgen (*Pipeline*) HLSOpts @@ -145,11 +145,9 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". -Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". -Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". +Extract Constant Compiler.print_GibleSeq => "PrintGibleSeq.print_if". +Extract Constant Compiler.print_GiblePar => "PrintGiblePar.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". -Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". -Extract Constant Compiler.print_RTLParFU => "PrintRTLParFU.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". @@ -184,8 +182,8 @@ 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 RTLBlockgen.partition => "Partition.partition". -Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". +Extract Constant GibleSeqgen.partition => "Partition.partition". +Extract Constant GiblePargen.schedule => "Schedule.schedule_fn". (* Loop normalization *) Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". @@ -197,7 +195,7 @@ Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls vericert.Compiler.transf_hls_temp - RTLBlockgen.transl_program RTLBlockInstr.successors_instr + GibleSeqgen.transl_program Gible.successors_instr HTLgen.tbl_to_case_expr Predicate.sat_pred_simple Verilog.stmnt_to_list diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 9d310fb..ab0511f 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -29,11 +29,12 @@ Require Import compcert.lib.Maps. Require compcert.verilog.Op. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlock. -Require Import vericert.hls.RTLPar. -Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Gible. Require Import vericert.hls.HashTree. Require Import vericert.hls.Predicate. +Require Import vericert.common.DecEq. #[local] Open Scope positive. #[local] Open Scope pred_op. @@ -65,121 +66,6 @@ Proof. decide equality; apply Pos.eq_dec. Defined. -Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. -Proof. - generalize comparison_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - decide equality. -Defined. - -Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize Z.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - decide equality. -Defined. - -Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize condition_eq; intro. - generalize addressing_eq; intro. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. -Proof. - generalize operation_eq; intro. - decide equality. -Defined. - -Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intros. - decide equality. -Defined. - -Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - (*| We then create equality lemmas for a resource and a module to index resources uniquely. The indexing is done by setting Mem to 1, whereas all other @@ -945,8 +831,8 @@ Qed.*) Section CORRECT. - Definition fd := @fundef RTLBlock.bb. - Definition tfd := @fundef RTLPar.bb. + Definition fd := GibleSeq.fundef. + Definition tfd := GiblePar.fundef. Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx). diff --git a/src/hls/Gible.v b/src/hls/Gible.v index 22d25f8..e7378ea 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -68,7 +68,7 @@ These are the instructions that count as control-flow, and will be placed at the end of the basic blocks. |*) -Inductive cf_instr : Type := +Variant cf_instr : Type := | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr | RBtailcall : signature -> reg + ident -> list reg -> cf_instr | RBbuiltin : external_function -> list (builtin_arg reg) -> @@ -76,10 +76,9 @@ Inductive cf_instr : Type := | RBcond : condition -> list reg -> node -> node -> cf_instr | RBjumptable : reg -> list node -> cf_instr | RBreturn : option reg -> cf_instr -| RBgoto : node -> cf_instr -| RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. +| RBgoto : node -> cf_instr. -Inductive instr : Type := +Variant instr : Type := | RBnop : instr | RBop : option pred_op -> operation -> list reg -> reg -> instr @@ -96,7 +95,7 @@ Helper Functions ================ |*) -Fixpoint successors_instr (i : cf_instr) : list node := +Definition successors_instr (i : cf_instr) : list node := match i with | RBcall sig ros args res s => s :: nil | RBtailcall sig ros args => nil @@ -105,11 +104,9 @@ Fixpoint successors_instr (i : cf_instr) : list node := | RBjumptable arg tbl => tbl | RBreturn optarg => nil | RBgoto n => n :: nil - | RBpred_cf p c1 c2 => - concat (successors_instr c1 :: successors_instr c2 :: nil) end. -Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := +Definition max_reg_cfi (m : positive) (i : cf_instr) := match i with | RBcall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) @@ -127,7 +124,6 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := | RBreturn None => m | RBreturn (Some arg) => Pos.max arg m | RBgoto n => m - | RBpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2) end. Definition max_reg_instr (m: positive) (i: instr) := @@ -304,15 +300,12 @@ Top-Level Type Definitions Module Type BlockType. Parameter t: Type. - - Section STEP. - Context {A B : Type}. - Parameter step: Genv.t A B -> val -> istate -> t -> istate -> Prop. - End STEP. - - Parameter max_reg : positive -> node -> t -> positive. - + Parameter foldl : forall A, (A -> instr -> A) -> t -> A -> A. Parameter length : t -> nat. + Parameter step: forall A B, Genv.t A B -> val -> istate -> t -> istate -> Prop. + + Arguments step [A B]. + Arguments foldl [A]. End BlockType. @@ -502,15 +495,7 @@ support if-conversion. | exec_RBgoto: forall s f sp pc rs pr m pc', step_cf_instr (State s f sp pc rs pr m) - (RBgoto pc') E0 (State s f sp pc' rs pr m) - | exec_RBpred_cf: - forall s f sp pc rs pr m cf1 cf2 st' p t, - step_cf_instr - (State s f sp pc - rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> - step_cf_instr - (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) - t st'. + (RBgoto pc') E0 (State s f sp pc' rs pr m). (*| Top-level step @@ -579,9 +564,11 @@ type ~genv~ which was declared earlier. Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). + Definition max_reg_block (m: positive) (n: node) (i: B.t) := B.foldl max_reg_instr i m. + Definition max_reg_function (f: function) := Pos.max - (PTree.fold B.max_reg f.(fn_code) 1%positive) + (PTree.fold max_reg_block f.(fn_code) 1%positive) (fold_left Pos.max f.(fn_params) 1%positive). Definition max_pc_function (f: function) : positive := @@ -592,4 +579,12 @@ type ~genv~ which was declared earlier. with Z.pos p => p | _ => 1 end))%positive) f.(fn_code) 1%positive. + Definition all_successors (b: B.t) : list node := + B.foldl (fun ns i => + match i with + | RBexit _ cf => successors_instr cf ++ ns + | _ => ns + end + ) b nil. + End Gible. diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v index 8eb06ae..9600d16 100644 --- a/src/hls/GiblePar.v +++ b/src/hls/GiblePar.v @@ -35,10 +35,17 @@ RTLBlock ======== |*) -Module BB <: BlockType. +Module ParBB <: BlockType. Definition t := list (list (list instr)). + Definition foldl (A: Type) (f: A -> instr -> A) (bb : t) (m : A): A := + fold_left + (fun x l => fold_left (fun x' l' => fold_left f l' x') l x) + bb m. + + Definition length : t -> nat := @length (list (list instr)). + Section RELSEM. Context {A B: Type} (ge: Genv.t A B). @@ -63,13 +70,7 @@ function that can execute lists of things, given their execution rule. End RELSEM. - Definition max_reg (m : positive) (pc : node) (bb : t) := - fold_left - (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) - bb m. - - Definition length : t -> nat := @length (list (list instr)). - -End BB. +End ParBB. -Module GiblePar := Gible(BB). +Module GiblePar := Gible(ParBB). +Export GiblePar. diff --git a/src/hls/RTLPargen.v b/src/hls/GiblePargen.v index d425049..37273b4 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/GiblePargen.v @@ -27,11 +27,12 @@ Require Import compcert.lib.Maps. Require compcert.verilog.Op. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlock. -Require Import vericert.hls.RTLPar. -Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Gible. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. +Require Import vericert.common.DecEq. Import NE.NonEmptyNotation. #[local] Open Scope positive. @@ -166,37 +167,41 @@ This is done by multiplying the predicates together, and assigning the negation of the expression to the other predicates. |*) -Definition update (f : forest) (i : instr) : forest := +Definition forest_state : Type := forest * list (cf_instr * option pred_op * forest). + +Definition update (flist : forest_state) (i : instr): forest_state := + let (f, fl) := flist in match i with - | RBnop => f + | RBnop => flist | RBop p op rl r => - f # (Reg r) <- + (f # (Reg r) <- (app_predicated p (f # (Reg r)) - (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))) + (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))), fl) | RBload p chunk addr rl r => - f # (Reg r) <- + (f # (Reg r) <- (app_predicated p (f # (Reg r)) (map_predicated (map_predicated (pred_ret (Eload chunk addr)) (merge (list_translation rl f))) - (f # Mem))) + (f # Mem))), fl) | RBstore p chunk addr rl r => - f # Mem <- + (f # Mem <- (app_predicated p (f # Mem) (map_predicated (map_predicated (predicated_apply2 (map_predicated (pred_ret Estore) (f # (Reg r))) chunk addr) - (merge (list_translation rl f))) (f # Mem))) + (merge (list_translation rl f))) (f # Mem))), fl) | RBsetpred p' c args p => - f # (Pred p) <- + (f # (Pred p) <- (app_predicated p' (f # (Pred p)) (map_predicated (pred_ret (Esetpred c)) - (merge (list_translation args f)))) + (merge (list_translation args f)))), fl) + | RBexit p c => (f, (c, p, f) :: fl) end. (*| @@ -207,7 +212,7 @@ code than in the RTLBlock code. Get a sequence from the basic block. |*) -Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := +Fixpoint abstract_sequence (f : forest_state) (b : list instr) : forest_state := match b with | nil => f | i :: l => abstract_sequence (update f i) l @@ -227,7 +232,7 @@ We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling transformation. |*) -Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := +Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool := match bb with | nil => match bbt with @@ -237,11 +242,10 @@ Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := | _ => true end. -Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool := - check (abstract_sequence empty (bb_body bb)) - (abstract_sequence empty (concat (concat (bb_body bbt)))) && - check_control_flow_instr (bb_exit bb) (bb_exit bbt) && - empty_trees (bb_body bb) (bb_body bbt). +Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := + check (fst (abstract_sequence (empty, nil) bb)) + (fst (abstract_sequence (empty, nil) (concat (concat bbt)))) && + empty_trees bb bbt. Definition check_scheduled_trees := beq2 schedule_oracle. @@ -271,22 +275,22 @@ Top-level Functions =================== |*) -Parameter schedule : RTLBlock.function -> RTLPar.function. +Parameter schedule : GibleSeq.function -> GiblePar.function. -Definition transl_function (f: RTLBlock.function) - : Errors.res RTLPar.function := +Definition transl_function (f: GibleSeq.function) + : Errors.res GiblePar.function := let tfcode := fn_code (schedule f) in - if check_scheduled_trees f.(fn_code) tfcode then - Errors.OK (mkfunction f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) + if check_scheduled_trees f.(GibleSeq.fn_code) tfcode then + Errors.OK (mkfunction f.(GibleSeq.fn_sig) + f.(GibleSeq.fn_params) + f.(GibleSeq.fn_stacksize) tfcode - f.(fn_entrypoint)) + f.(GibleSeq.fn_entrypoint)) else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). Definition transl_fundef := transf_partial_fundef transl_function. -Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := +Definition transl_program (p : GibleSeq.program) : Errors.res GiblePar.program := transform_partial_program transl_fundef p. diff --git a/src/hls/RTLPargenproof.v b/src/hls/GiblePargenproof.v index f975601..2abbea4 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -26,10 +26,10 @@ Require Import compcert.common.Values. Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlock. -Require Import vericert.hls.RTLPar. -Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLPargen. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. @@ -89,7 +89,7 @@ Proof. induction l; crush. Qed. Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}. Proof. destruct (check_dest_l i r); tauto. Qed. -Lemma check_dest_update : +(*Lemma check_dest_update : forall f i r, check_dest i r = false -> (update f i) # (Reg r) = f # (Reg r). @@ -1145,3 +1145,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. +*) diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index 1ba28bc..9444f28 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -36,13 +36,13 @@ RTLBlock ======== |*) -Module BB <: BlockType. +Module SeqBB <: BlockType. Definition t := list instr. - Section RELSEM. + Definition foldl {A: Type}: (A -> instr -> A) -> t -> A -> A := @fold_left A instr. - Context {A B: Type} (ge: Genv.t A B). + Definition length : t -> nat := @length instr. (*| Instruction list step @@ -56,16 +56,9 @@ This is simply using the high-level function ``step_list``, which is a general function that can execute lists of things, given their execution rule. |*) - Definition step := step_list (step_instr ge). - - End RELSEM. - - Definition max_reg (m : positive) (n: node) (i : t) : positive := - fold_left max_reg_instr i m. - - Definition length : t -> nat := @length instr. + Definition step {A B: Type} (ge: Genv.t A B) := step_list (step_instr ge). -End BB. +End SeqBB. -Module GibleSeq := Gible(BB). +Module GibleSeq := Gible(SeqBB). Export GibleSeq. diff --git a/src/hls/GibleSeqgen.v b/src/hls/GibleSeqgen.v index 8d52339..31dabf8 100644 --- a/src/hls/GibleSeqgen.v +++ b/src/hls/GibleSeqgen.v @@ -42,7 +42,7 @@ Definition check_valid_node (tc: code) (e: node) := | _ => false end. -Fixpoint check_code (c: RTL.code) (tc: code) (pc: node) (b: BB.t) := +Fixpoint check_code (c: RTL.code) (tc: code) (pc: node) (b: SeqBB.t) := match c ! pc, b with | Some (RTL.Inop pc'), RBnop :: (_ :: _ :: _) as b' => check_code c tc pc' b' diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v index 55b25d1..8fd859b 100644 --- a/src/hls/GibleSeqgenproof.v +++ b/src/hls/GibleSeqgenproof.v @@ -104,7 +104,7 @@ finding is actually done at that higher level already. Definition valid_succ (tc: code) (pc: node) : Prop := exists b, tc ! pc = Some b. - Inductive match_block (c: RTL.code) (tc: code) (pc: node): BB.t -> Prop := + Inductive match_block (c: RTL.code) (tc: code) (pc: node): SeqBB.t -> Prop := (* * Basic Block Instructions *) @@ -195,9 +195,9 @@ the basic block. Definition sem_extrap f pc sp in_s in_s' block := forall out_s block2, - BB.step tge sp in_s block out_s -> + SeqBB.step tge sp in_s block out_s -> f.(fn_code) ! pc = Some block2 -> - BB.step tge sp in_s' block2 out_s. + SeqBB.step tge sp in_s' block2 out_s. Lemma match_block_exists_instr : forall c tc pc a, @@ -224,7 +224,7 @@ proof inside of the ``match_states`` that shows that the execution from the whole execution (in one big step) of the basic block. |*) - Variant match_states : option BB.t -> RTL.state -> state -> Prop := + Variant match_states : option SeqBB.t -> RTL.state -> state -> Prop := | match_state : forall stk stk' f tf sp pc rs m pc0 b rs0 m0 (TF: transl_function f = OK tf) @@ -282,7 +282,7 @@ whole execution (in one big step) of the basic block. inv H; auto. Qed. - Definition measure (b: option BB.t): nat := + Definition measure (b: option SeqBB.t): nat := match b with | None => 0 | Some b' => 1 + length b' @@ -528,7 +528,7 @@ whole execution (in one big step) of the basic block. (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') -> Op.eval_operation ge sp op rs ## args m = Some v -> transl_function f = OK tf -> - (forall (pc0 : positive) (b : BB.t), + (forall (pc0 : positive) (b : SeqBB.t), (fn_code tf) ! pc0 = Some b -> match_block (RTL.fn_code f) (fn_code tf) pc0 b) -> Forall2 match_stackframe s stk' -> star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) -> @@ -737,7 +737,7 @@ whole execution (in one big step) of the basic block. forall b s2, match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 -> exists b' s2', - (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\ match_states b' (RTL.Callstate s fd rs ## args m') s2'. Proof. intros * H H0 H1 H2. @@ -802,7 +802,7 @@ whole execution (in one big step) of the basic block. forall b s2, match_states b (RTL.Callstate s (Internal f) args m) s2 -> exists b' s2', - (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\ match_states b' (RTL.State s f (Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) (RTL.init_regs args (RTL.fn_params f)) m') s2'. Proof. @@ -845,7 +845,7 @@ whole execution (in one big step) of the basic block. forall b s2, match_states b (RTL.Callstate s (External ef) args m) s2 -> exists b' s2', - (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option BB.t) measure b' b) /\ + (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option SeqBB.t) measure b' b) /\ match_states b' (RTL.Returnstate s res m') s2'. Proof. intros * H. @@ -861,7 +861,7 @@ whole execution (in one big step) of the basic block. forall res f sp pc rs s vres m b s2, match_states b (RTL.Returnstate (RTL.Stackframe res f sp pc rs :: s) vres m) s2 -> exists b' s2', - (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\ match_states b' (RTL.State s f sp pc rs # res <- vres m) s2'. Proof. intros. @@ -884,7 +884,7 @@ whole execution (in one big step) of the basic block. forall b0 s2, match_states b0 (RTL.State s f sp pc rs m) s2 -> exists b' s2', - (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b0) /\ + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b0) /\ match_states b' (RTL.State s f sp pc' rs m) s2'. Proof. intros * H H0 H1. @@ -920,7 +920,7 @@ whole execution (in one big step) of the basic block. forall b s2, match_states b (RTL.State s f sp pc rs m) s2 -> exists b' s2', - (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\ match_states b' (RTL.State s f sp pc' rs m) s2'. Proof. intros * H H0 H1. @@ -947,7 +947,7 @@ whole execution (in one big step) of the basic block. forall b s2, match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 -> exists b' s2', - (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option SeqBB.t) measure b' b) /\ match_states b' (RTL.Returnstate s (regmap_optget or Vundef rs) m') s2'. Proof. intros * H H0. diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 8960ef9..a058536 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -30,8 +30,8 @@ Require Import vericert.hls.AssocMap. Require Import vericert.hls.FunctionalUnits. Require Import vericert.hls.HTL. Require Import vericert.hls.Predicate. -Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLParFU. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Gible. Require Import vericert.hls.FunctionalUnits. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. @@ -685,20 +685,26 @@ Definition translate_predicate (a : assignment) ret (a dst (Vternary (pred_expr preg pos) e dst)) end. -Definition translate_inst a (fin rtrn preg : reg) (n : node) (i : instr) - : mon stmnt := - match i with - | FUnop => - ret Vskip - | FUop p op args dst => - do instr <- translate_instr op args; - do _ <- declare_reg None dst 32; - translate_predicate a preg p (Vvar dst) instr - | FUread p1 p2 r => ret Vskip - | FUwrite p1 p2 r => ret Vskip - | FUsetpred _ c args p => - do cond <- translate_condition c args; - ret (a (pred_expr preg (Plit (true, p))) cond) +Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) + (args : list reg) (stack : reg) : mon expr := + match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Mint32, Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vvari stack + (Vbinop Vdivu + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vvari stack (Vlit (ZToValue (a / 4)))) + else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset") + | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") end. Lemma create_new_state_state_incr: @@ -726,28 +732,17 @@ Definition create_new_state (p: node): mon node := s.(st_controllogic)) (create_new_state_state_incr s p). -Definition translate_inst_list (fin rtrn preg: reg) (ni : node * node * list (list instr)) := - match ni with - | (n, p, li) => - do _ <- collectlist - (fun l => - do stmnt <- translate_inst Vblock fin rtrn preg n l; - add_data_instr n stmnt) (concat li); - do st <- get; - add_control_instr n (state_goto st.(st_st) p) - end. - -Fixpoint translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr) +Definition translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr) : mon (stmnt * stmnt) := match cfi with - | FUgoto n' => + | RBgoto n' => do st <- get; ret (Vskip, state_goto st.(st_st) n') - | FUcond c args n1 n2 => + | RBcond c args n1 n2 => do st <- get; do e <- translate_condition c args; ret (Vskip, state_cond st.(st_st) e n1 n2) - | FUreturn r => + | RBreturn r => match r with | Some r' => ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))), @@ -756,18 +751,14 @@ Fixpoint translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr) ret ((Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))), Vskip) end - | FUpred_cf p c1 c2 => - do (tc1s, tc1c) <- translate_cfi' fin rtrn preg c1; - do (tc2s, tc2c) <- translate_cfi' fin rtrn preg c2; - ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c)) - | FUjumptable r tbl => + | RBjumptable r tbl => do s <- get; ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip)) - | FUcall sig ri rl r n => + | RBcall sig ri rl r n => error (Errors.msg "HTLPargen: RPcall not supported.") - | FUtailcall sig ri lr => + | RBtailcall sig ri lr => error (Errors.msg "HTLPargen: RPtailcall not supported.") - | FUbuiltin e lb b n => + | RBbuiltin e lb b n => error (Errors.msg "HTLPargen: RPbuildin not supported.") end. @@ -778,17 +769,50 @@ Definition translate_cfi (fin rtrn preg: reg) (ni: node * cf_instr) do _ <- add_control_instr n c; add_data_instr n s. -Definition transf_bblock (fin rtrn preg: reg) (ni : node * bblock) +Definition translate_inst a (fin rtrn preg stack : reg) (n : node) (i : instr) := + match i with + | RBnop => + do stmnt <- ret Vskip; + add_data_instr n stmnt + | RBop p op args dst => + do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; + do stmnt <- translate_predicate a preg p (Vvar dst) instr; + add_data_instr n stmnt + | RBload p mem addr args dst => + do src <- translate_arr_access mem addr args stack; + do _ <- declare_reg None dst 32; + do stmnt <- translate_predicate a preg p (Vvar dst) src; + add_data_instr n stmnt + | RBstore p mem addr args src => + do dst <- translate_arr_access mem addr args stack; + do stmnt <- translate_predicate a preg p dst (Vvar src); + add_data_instr n stmnt + | RBsetpred _ c args p => + do cond <- translate_condition c args; + do stmnt <- ret (a (pred_expr preg (Plit (true, p))) cond); + add_data_instr n stmnt + | RBexit p cf => + translate_cfi fin rtrn preg (n, cf) + end. + +Definition translate_inst_list (fin rtrn preg stack: reg) (ni : node * node * list (list instr)) := + match ni with + | (n, p, li) => + do _ <- collectlist + (fun l => translate_inst Vblock fin rtrn preg stack n l) (concat li); + do st <- get; + add_control_instr n (state_goto st.(st_st) p) + end. + +Definition transf_bblock (fin rtrn preg stack: reg) (ni : node * ParBB.t) : mon unit := let (n, bb) := ni in - do nstate <- create_new_state ((poslength bb.(bb_body)))%positive; - do _ <- collectlist (translate_inst_list fin rtrn preg) - (prange n (nstate + poslength bb.(bb_body) - 1)%positive - bb.(bb_body)); - match bb.(bb_body) with - | nil => translate_cfi fin rtrn preg (n, bb.(bb_exit)) - | _ => translate_cfi fin rtrn preg (nstate, bb.(bb_exit)) - end. + do nstate <- create_new_state ((poslength bb))%positive; + do _ <- collectlist (translate_inst_list fin rtrn preg stack) + (prange n (nstate + poslength bb - 1)%positive + bb); + add_control_instr nstate Vskip. (*Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. refine (match bool_dec ((a <? b) && (b <? c) && (c <? d) @@ -821,41 +845,43 @@ Definition transf_module (f: function) : mon HTL.module := do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; do preg <- create_reg None 32; - do _ <- collectlist (transf_bblock fin rtrn preg) + do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do _ <- collectlist (transf_bblock fin rtrn preg stack) (Maps.PTree.elements f.(fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(fn_params); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; do clk <- create_reg (Some Vinput) 1; - match get_ram 0 (fn_funct_units f) with - | Some (_, r) => - do _ <- declare_ram r; - do current_state <- get; - match zle (Z.pos (max_pc_map current_state.(st_datapath))) - Integers.Int.max_unsigned, - zle (Z.pos (max_pc_map current_state.(st_controllogic))) + do r_en <- create_reg None 1; + do r_u_en <- create_reg None 1; + do r_addr <- create_reg None 32; + do r_wr_en <- create_reg None 1; + do r_d_in <- create_reg None 32; + do r_d_out <- create_reg None 32; + do current_state <- get; + match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, - max_list_dec (fn_params f) (st_st current_state) - with - | left LEDATA, left LECTRL, left WFPARAMS => - ret (HTL.mkmodule - f.(fn_params) - current_state.(st_datapath) - current_state.(st_controllogic) - f.(fn_entrypoint) - current_state.(st_st) - fin - rtrn - start - rst - clk - current_state.(st_scldecls) - current_state.(st_arrdecls) - r) - | _, _, _=> error (Errors.msg "More than 2^32 states.") - end - | _ => error (Errors.msg "Stack RAM not found.") + zle (Z.pos (max_pc_map current_state.(st_controllogic))) + Integers.Int.max_unsigned, + max_list_dec (fn_params f) (st_st current_state) + with + | left LEDATA, left LECTRL, left WFPARAMS => + ret (HTL.mkmodule + f.(fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + (mk_ram stack_len stack r_en r_u_en r_addr r_wr_en r_d_in r_d_out)) + | _, _, _=> error (Errors.msg "More than 2^32 states.") end else error (Errors.msg "Stack size misalignment."). @@ -874,7 +900,7 @@ Definition transl_module (f : function) : Errors.res HTL.module := Definition transl_fundef := transf_partial_fundef transl_module. -Definition main_is_internal (p : RTLParFU.program) : bool := +Definition main_is_internal (p : GiblePar.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with | Some b => @@ -885,7 +911,7 @@ Definition main_is_internal (p : RTLParFU.program) : bool := | _ => false end. -Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program := +Definition transl_program (p : GiblePar.program) : Errors.res HTL.program := if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). 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)). diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 4e699e6..3b7cdd7 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -16,7 +16,6 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -(* [[file:../../docs/basic-block-generation.org::partition-main][partition-main]] *) open Printf open Clflags open Camlcoq @@ -26,8 +25,9 @@ open Maps open AST open Kildall open Op -open RTLBlockInstr -open RTLBlock +open Gible +open GibleSeq +open GibleSeq (** Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) @@ -41,8 +41,10 @@ let find_edges c = let f = find_edge i n in (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], []) -let prepend_instr i = function - | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} +(* let prepend_instr i = function *) +(* | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} *) + +let prepend_instr i b = i :: b let translate_inst = function | RTL.Inop _ -> Some RBnop @@ -66,14 +68,14 @@ let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = match trans_inst, succ with | (None, Some i'), _ -> if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s } + Errors.OK [RBnop; RBexit (None, (RBgoto s))] else - Errors.OK { bb_body = [RBnop]; bb_exit = i' } + Errors.OK [RBnop; RBexit (None, i')] | (Some i', None), (s', Some i_n)::[] -> if List.exists (fun x -> x = s) (fst e) then - Errors.OK { bb_body = [i']; bb_exit = RBgoto s' } + Errors.OK [i'; RBexit (None, (RBgoto s'))] else if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK { bb_body = []; bb_exit = RBgoto s } + Errors.OK [RBnop; RBexit (None, (RBgoto s))] else begin match next_bblock_from_RTL false e c s' i_n with | Errors.OK bb -> @@ -102,12 +104,12 @@ let rec translate_all edge c s res = | Some i -> match next_bblock_from_RTL true edge c s i with | Errors.Error msg -> Errors.Error msg - | Errors.OK {bb_body = bb; bb_exit = e} -> - let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in + | Errors.OK bb -> + let succ = List.filter (fun x -> P.lt x s) (all_successors bb) in (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with | Errors.Error msg -> Errors.Error msg | Errors.OK (c', t') -> - Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t'))) + Errors.OK (PTree.set s bb c', t'))) (* Partition a function and transform it into RTLBlock. *) let function_from_RTL f = @@ -123,4 +125,3 @@ let function_from_RTL f = } let partition = function_from_RTL -(* partition-main ends here *) diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v index bb01ff9..63d7d5a 100644 --- a/src/hls/PipelineOp.v +++ b/src/hls/PipelineOp.v @@ -28,8 +28,8 @@ Require Import compcert.verilog.Op. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLPar. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePar. Require Import vericert.hls.FunctionalUnits. Import Option.Notation. @@ -56,8 +56,8 @@ Definition div_pos_in_block (il: nat * list (nat * nat * nat)) bb := let dp := snd (List.fold_left div_pos_in_list bb (0%nat, nil)) in (S i, (List.map (fun (yx : nat * nat) => let (y, x) := yx in (i, y, x)) dp) ++ l). -Definition find_divs (bb: bblock) := - snd (List.fold_left div_pos_in_block bb.(bb_body) (0%nat, nil)). +Definition find_divs (bb: ParBB.t) := + snd (List.fold_left div_pos_in_block bb (0%nat, nil)). Fixpoint mapi' {A B: Type} (n: nat) (f: nat -> A -> B) (l: list A): list B := match l with diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintGible.ml index b8e1e2e..16d91af 100644 --- a/src/hls/PrintRTLBlockInstr.ml +++ b/src/hls/PrintGible.ml @@ -3,7 +3,7 @@ open Camlcoq open Datatypes open Maps open AST -open RTLBlockInstr +open Gible open Predicate open PrintAST @@ -33,31 +33,7 @@ let print_pred_option pp = function | Some x -> fprintf pp "(%a)" print_pred_op x | None -> () -let print_bblock_body pp i = - fprintf pp "\t\t"; - match i with - | RBnop -> fprintf pp "nop\n" - | RBop(p, op, ls, dst) -> - fprintf pp "%a %a = %a\n" - print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) - | RBload(p, chunk, addr, args, dst) -> - fprintf pp "%a %a = %s[%a]\n" - print_pred_option p reg dst (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args) - | RBstore(p, chunk, addr, args, src) -> - fprintf pp "%a %s[%a] = %a\n" - print_pred_option p - (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args) - reg src - | RBsetpred (p', c, args, p) -> - fprintf pp "%a %a = %a\n" - print_pred_option p' - pred p - (PrintOp.print_condition reg) (c, args) - -let rec print_bblock_exit pp i = - fprintf pp "\t\t"; +let print_bblock_exit pp i = match i with | RBcall(_, fn, args, res, _) -> fprintf pp "%a = %a(%a)\n" @@ -86,5 +62,28 @@ let rec print_bblock_exit pp i = fprintf pp "return %a\n" reg arg | RBgoto n -> fprintf pp "goto %d\n" (P.to_int n) - | RBpred_cf (p, c1, c2) -> - fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2 + +let print_bblock_body pp i = + fprintf pp "\t\t"; + match i with + | RBnop -> fprintf pp "nop\n" + | RBop(p, op, ls, dst) -> + fprintf pp "%a %a = %a\n" + print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) + | RBload(p, chunk, addr, args, dst) -> + fprintf pp "%a %a = %s[%a]\n" + print_pred_option p reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | RBstore(p, chunk, addr, args, src) -> + fprintf pp "%a %s[%a] = %a\n" + print_pred_option p + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + | RBsetpred (p', c, args, p) -> + fprintf pp "%a %a = %a\n" + print_pred_option p' + pred p + (PrintOp.print_condition reg) (c, args) + | RBexit (p, cf) -> + fprintf pp "%a %a" print_pred_option p print_bblock_exit cf diff --git a/src/hls/PrintRTLPar.ml b/src/hls/PrintGiblePar.ml index ab93fa5..11bea67 100644 --- a/src/hls/PrintRTLPar.ml +++ b/src/hls/PrintGiblePar.ml @@ -17,10 +17,11 @@ open Camlcoq open Datatypes open Maps open AST -open RTLBlockInstr -open RTLPar +open Gible +open GiblePar +open GiblePar open PrintAST -open PrintRTLBlockInstr +open PrintGible (* Printing of RTL code *) @@ -40,8 +41,7 @@ let print_bblock pp (pc, i) = fprintf pp "%5d:{\n" pc; List.iter (fun x -> fprintf pp "{\n"; List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x; - fprintf pp "}\n") i.bb_body; - print_bblock_exit pp i.bb_exit; + fprintf pp "}\n") i; fprintf pp "\t}\n\n" let print_function pp id f = diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintGibleSeq.ml index 8fef401..155f98e 100644 --- a/src/hls/PrintRTLBlock.ml +++ b/src/hls/PrintGibleSeq.ml @@ -17,10 +17,11 @@ open Camlcoq open Datatypes open Maps open AST -open RTLBlockInstr -open RTLBlock +open Gible +open GibleSeq +open GibleSeq open PrintAST -open PrintRTLBlockInstr +open PrintGible (* Printing of RTL code *) @@ -38,8 +39,7 @@ let ros pp = function let print_bblock pp (pc, i) = fprintf pp "%5d:{\n" pc; - List.iter (print_bblock_body pp) i.bb_body; - print_bblock_exit pp i.bb_exit; + List.iter (print_bblock_body pp) i; fprintf pp "\t}\n\n" let print_function pp id f = diff --git a/src/hls/PrintRTLParFU.ml b/src/hls/PrintRTLParFU.ml deleted file mode 100644 index ec4d851..0000000 --- a/src/hls/PrintRTLParFU.ml +++ /dev/null @@ -1,120 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Pretty-printers for RTL code *) - -open Printf -open Camlcoq -open Datatypes -open Maps -open AST -open PrintRTLBlockInstr -open RTLParFU -open PrintAST - -(* Printing of RTL code *) - -let reg pp r = - fprintf pp "x%d" (P.to_int r) - -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl - -let ros pp = function - | Coq_inl r -> reg pp r - | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) - -let print_bblock_body pp i = - fprintf pp "\t\t"; - match i with - | FUnop -> fprintf pp "nop\n" - | FUop(p, op, ls, dst) -> - fprintf pp "%a %a = %a\n" - print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) - | FUsetpred (p', c, args, p) -> - fprintf pp "%a %a = %a\n" - print_pred_option p' - pred p - (PrintOp.print_condition reg) (c, args) - | _ -> assert false - -let rec print_bblock_exit pp i = - fprintf pp "\t\t"; - match i with - | FUcall(_, fn, args, res, _) -> - fprintf pp "%a = %a(%a)\n" - reg res ros fn regs args; - | FUtailcall(_, fn, args) -> - fprintf pp "tailcall %a(%a)\n" - ros fn regs args - | FUbuiltin(ef, args, res, _) -> - fprintf pp "%a = %s(%a)\n" - (print_builtin_res reg) res - (name_of_external ef) - (print_builtin_args reg) args - | FUcond(cond, args, s1, s2) -> - fprintf pp "if (%a) goto %d else goto %d\n" - (PrintOp.print_condition reg) (cond, args) - (P.to_int s1) (P.to_int s2) - | FUjumptable(arg, tbl) -> - let tbl = Array.of_list tbl in - fprintf pp "jumptable (%a)\n" reg arg; - for i = 0 to Array.length tbl - 1 do - fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i)) - done - | FUreturn None -> - fprintf pp "return\n" - | FUreturn (Some arg) -> - fprintf pp "return %a\n" reg arg - | FUgoto n -> - fprintf pp "goto %d\n" (P.to_int n) - | FUpred_cf (p, c1, c2) -> - fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2 - -let print_bblock pp (pc, i) = - fprintf pp "%5d:{\n" pc; - List.iter (fun x -> fprintf pp "{\n"; - List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x; - fprintf pp "}\n") i.bb_body; - print_bblock_exit pp i.bb_exit; - fprintf pp "\t}\n\n" - -let print_function pp id f = - fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; - let instrs = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements f.fn_code)) in - List.iter (print_bblock pp) instrs; - fprintf pp "}\n\n" - -let print_globdef pp (id, gd) = - match gd with - | Gfun(Internal f) -> print_function pp id f - | _ -> () - -let print_program pp (prog: program) = - List.iter (print_globdef pp) prog.prog_defs - -let destination : string option ref = ref None - -let print_if passno prog = - match !destination with - | None -> () - | Some f -> - let oc = open_out (f ^ "." ^ Z.to_string passno) in - print_program oc prog; - close_out oc diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v deleted file mode 100644 index 886c23d..0000000 --- a/src/hls/RICtransf.v +++ /dev/null @@ -1,86 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -Require Import compcert.common.AST. -Require Import compcert.common.Errors. -Require Import compcert.common.Globalenvs. -Require Import compcert.lib.Integers. -Require Import compcert.lib.Maps. - -Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLPar. -Require Import vericert.hls.Predicate. - -(*| -===================== -Reverse If-Conversion -===================== - -This transformation takes a scheduling RTLPar block and removes any predicates -from it. It can then be trivially transformed into linear code again. It works -by iteratively selecting a predicate, then creating a branch based on it and -placing subsequent instructions in one branch or the other. -|*) - -Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B := - match l with - | nil => None - | a :: l0 => - match f a, existsb_val f l0 with - | _, Some v => Some v - | Some v, _ => Some v - | _, _ => None - end - end. - -Definition includes_setpred (bb: bb) := - existsb_val (existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end))) bb. - -Definition add_bb (should_split: bool) (i: bb) (bbc: list bb * list bb) := - match bbc with - | (a, b) => if should_split then (a, i::b) else (i::a, b) - end. - -Fixpoint first_split (saw_pred: bool) (bb: list bb) := - match bb with - | a :: b => - match includes_setpred a with - | Some v => - let (_, res) := first_split true b in - (Some v, add_bb saw_pred a res) - | _ => - let (v, res) := first_split saw_pred b in - (v, add_bb saw_pred a res) - end - | nil => (None, (nil, nil)) - end. - -Definition split_bb (fresh: node) (b: list bb) : list bb * list bb * list bb := - match first_split false b with - | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) - | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) - end. - -Definition transf_function (f: function) : function := f. - -Definition transf_fundef (fd: fundef) : fundef := - transf_fundef transf_function fd. - -Definition transf_program (p: program) : program := - transform_program transf_fundef p. diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index 49ee6e7..a15be1c 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -30,8 +30,8 @@ Require Import vericert.hls.AssocMap. Require Import vericert.hls.Predicate. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. -Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLPar. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePar. Require Import vericert.hls.RTLParFU. Require Import vericert.hls.FunctionalUnits. @@ -43,7 +43,7 @@ Definition update {A: Type} (i: positive) (f: option A -> A) (pt: PTree.t A) := Definition add_instr (instr_: instr) x := match x with Some i => instr_ :: i | None => instr_ :: nil end. -Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.instr) +Definition transl_instr (res: resources) (cycle: positive) (i: Gible.instr) (li: Errors.res (list instr * PTree.t (list instr))): Errors.res (list instr * PTree.t (list instr)) := do (instr_list, d_tree) <- li; @@ -74,9 +74,10 @@ Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.ins | _ => Errors.Error (Errors.msg "Could not find RAM") end | RBsetpred op c args p => Errors.OK (FUsetpred op c args p :: instr_list, d_tree) + | RBexit po cf => Errors.Error (Errors.msg "Wrong.") end. -Fixpoint transl_cf_instr (i: RTLBlockInstr.cf_instr): RTLParFU.cf_instr := +Definition transl_cf_instr (i: Gible.cf_instr): RTLParFU.cf_instr := match i with | RBcall sig r args d n => FUcall sig r args d n | RBtailcall sig r args => FUtailcall sig r args @@ -85,7 +86,6 @@ Fixpoint transl_cf_instr (i: RTLBlockInstr.cf_instr): RTLParFU.cf_instr := | RBjumptable r ns => FUjumptable r ns | RBreturn r => FUreturn r | RBgoto n => FUgoto n - | RBpred_cf po c1 c2 => FUpred_cf po (transl_cf_instr c1) (transl_cf_instr c2) end. Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) := @@ -101,7 +101,7 @@ Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res ( OK (y::ys) end. -Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list RTLBlockInstr.instr) +Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list Gible.instr) (state: Errors.res (list (list instr) * PTree.t (list instr))) : Errors.res (list (list instr) * PTree.t (list instr)) := do (li, tr) <- state; @@ -110,7 +110,7 @@ Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: lis (*Compute transl_op_chain_block initial_resources 10%nat (RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::RBnop::RBnop::nil) (OK (nil, PTree.empty _)).*) -Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list RTLBlockInstr.instr)) +Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list Gible.instr)) (state: Errors.res (list (list (list instr)) * PTree.t (list instr))) : Errors.res (list (list (list instr)) * PTree.t (list instr)) := do (li, tr) <- state; @@ -119,7 +119,7 @@ Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (li (*Compute transl_par_block initial_resources 10%nat ((RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::nil)::(RBop None (Op.Ointconst (Int.repr 2)) nil 2%positive::RBnop::nil)::nil) (OK (((FUnop::nil)::nil)::nil, PTree.empty _)).*) -Definition transl_seq_block (res: resources) (b: list (list RTLBlockInstr.instr)) +Definition transl_seq_block (res: resources) (b: list (list Gible.instr)) (a: Errors.res (list (list (list instr)) * PTree.t (list instr) * positive)) := do (litr, n) <- a; let (li, tr) := litr in @@ -134,14 +134,13 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) | None => ((cycle + 1)%positive, curr :: bb) end. -Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body := +Definition transl_bb (res: resources) (bb: ParBB.t): Errors.res RTLParFU.bblock_body := do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; let (li, tr) := litr in OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). -Definition transl_bblock (res: resources) (bb: RTLPar.bblock): Errors.res bblock := - do bb' <- transl_bb res (RTLBlockInstr.bb_body bb); - OK (mk_bblock bb' (transl_cf_instr (RTLBlockInstr.bb_exit bb))). +(*Definition transl_bblock (res: resources) (bb: ParBB.t): Errors.res ParBB.t := + transl_bb res bb. Definition error_map_ptree {A B: Type} (f: positive -> A -> res B) (pt: PTree.t A) := do ptl' <- map_error (fun x => do x' <- uncurry f x; OK (fst x, x')) (PTree.elements pt); @@ -175,3 +174,4 @@ Definition transl_fundef p := Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program := transform_partial_program transl_fundef p. +*) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 70395e7..9d9700a 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -25,9 +25,12 @@ open Maps open AST open Kildall open Op -open RTLBlockInstr +open Gible open Predicate -open RTLBlock +open GibleSeq +open GibleSeq +open GiblePar +open GiblePar open HTL open Verilog open HTLgen @@ -286,6 +289,7 @@ let comb_delay = function | Omod -> 72 | Omodu -> 72 | _ -> 1) + | RBexit _ -> 8 | _ -> 1 let pipeline_stages = function @@ -330,6 +334,11 @@ let accumulate_RAW_deps map dfg curr = | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst | RBsetpred (_op, _mem, rs, _p) -> acc_dep_instruction_nodst rs | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs) + | RBexit (_, RBcall (_, _, rs, _, _)) -> acc_dep_instruction_nodst rs + | RBexit (_, RBtailcall (_, _, rs)) -> acc_dep_instruction_nodst rs + | RBexit (_, RBcond (_, rs, _, _)) -> acc_dep_instruction_nodst rs + | RBexit (_, RBjumptable (r, _)) -> acc_dep_instruction_nodst [r] + | RBexit (_, RBreturn (Some r)) -> acc_dep_instruction_nodst [r] | _ -> (i + 1, dst_map, graph) (** Finds the next write to the [dst] register. This is a small optimisation so that only one @@ -356,8 +365,13 @@ let rec find_all_next_dst_read i dst i' curr = | RBop (_, _, rs, _) :: curr' -> check_dst rs curr' | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' - | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' | RBsetpred (_, _, rs, _) :: curr' -> check_dst rs curr' + | RBexit (_, RBcall (_, _, rs, _, _)) :: curr' -> check_dst rs curr' + | RBexit (_, RBtailcall (_, _, rs)) :: curr' -> check_dst rs curr' + | RBexit (_, RBcond (_, rs, _, _)) :: curr' -> check_dst rs curr' + | RBexit (_, RBjumptable (r, _)) :: curr' -> check_dst [r] curr' + | RBexit (_, RBreturn (Some r)) :: curr' -> check_dst [r] curr' + | _ :: curr' -> check_dst [] curr' let drop i lst = let rec drop' i' lst' = @@ -525,6 +539,7 @@ let get_pred = function | RBop (op, _, _, _) -> op | RBload (op, _, _, _, _) -> op | RBstore (op, _, _, _, _) -> op + | RBexit (op, _) -> op | RBsetpred (_, _, _, _) -> None let independant_pred p p' = @@ -551,14 +566,14 @@ let remove_unnecessary_deps graph = before the sink of the basic block. After that, there should be constraints for data dependencies between nodes. *) let gather_bb_constraints debug bb = - let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in + let ibody = List.mapi (fun i a -> (i, a)) bb in let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in let _, _, dfg' = List.fold_left (accumulate_RAW_deps ibody) (0, PTree.empty, dfg) - bb.bb_body + bb in - let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg' + let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb) dfg ibody) dfg' [ accumulate_WAW_deps; accumulate_WAR_deps; accumulate_RAW_mem_deps; @@ -570,7 +585,7 @@ let gather_bb_constraints debug bb = ] in let dfg''' = remove_unnecessary_deps dfg'' in - (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit) + (List.length bb, dfg''', GibleSeq.all_successors bb) let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i } let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i } @@ -690,15 +705,15 @@ let add_resource_constr n dfg constr = |> get_constraints (List.rev res.res_udiv) |> get_constraints (List.rev res.res_sdiv) -let gather_cfg_constraints c constr curr = +let gather_cfg_constraints (c: GibleSeq.code) constr curr = let (n, dfg) = curr in match PTree.get (P.of_int n) c with | None -> assert false - | Some { bb_exit = ctrl; _ } -> + | Some bb -> add_super_nodes n dfg constr |> add_initial_sv n dfg |> add_data_deps n dfg - |> add_ctrl_deps n (successors_instr ctrl + |> add_ctrl_deps n (GibleSeq.all_successors bb |> List.map P.to_int |> List.filter (fun n' -> n' < n)) |> add_cycle_constr 8 n dfg @@ -802,10 +817,10 @@ let range s e = (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) let transf_rtlpar c c' schedule = - let f i bb : RTLPar.bblock = + let f i bb : ParBB.t = match bb with - | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c } - | { bb_body = bb_body'; bb_exit = ctrl_flow } -> + | bb_body' -> + (* | { bb_body = bb_body'; bb_exit = ctrl_flow } -> *) let dfg = match PTree.get i c' with None -> assert false | Some x -> x in let bb_st_e = let m = IMap.find (P.to_int i) (snd schedule) in @@ -836,13 +851,12 @@ let transf_rtlpar c c' schedule = (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) |> List.rev) body2*) in - { bb_body = final_body2; - bb_exit = ctrl_flow - } + final_body2 + | _ -> List.map (fun i -> [[i]]) bb in PTree.map f c -let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = +let schedule entry (c : GibleSeq.code) = let debug = true in let transf_graph (_, dfg, _) = dfg in let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in @@ -859,22 +873,22 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = (**printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) transf_rtlpar c c' schedule' -let rec find_reachable_states c e = - match PTree.get e c with - | Some { bb_exit = ex; _ } -> - e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) [] - (successors_instr ex |> List.filter (fun x -> P.lt x e)) - | None -> assert false +(* let rec find_reachable_states c e = *) +(* match PTree.get e c with *) +(* | Some bb -> *) +(* e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) [] *) +(* (all_successors bb |> List.filter (fun x -> P.lt x e)) *) +(* | None -> assert false *) let add_to_tree c nt i = match PTree.get i c with | Some p -> PTree.set i p nt | None -> assert false -let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = +let schedule_fn (f : GibleSeq.coq_function) : GiblePar.coq_function = let scheduled = schedule f.fn_entrypoint f.fn_code in - let reachable = find_reachable_states scheduled f.fn_entrypoint - |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in + (* let reachable = find_reachable_states scheduled f.fn_entrypoint *) + (* |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in *) { fn_sig = f.fn_sig; fn_params = f.fn_params; fn_stacksize = f.fn_stacksize; |