diff options
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/RTLBlock.v | 94 | ||||
-rw-r--r-- | src/hls/RTLBlockInstr.v | 6 | ||||
-rw-r--r-- | src/hls/RTLBlockgen.v | 264 | ||||
-rw-r--r-- | src/hls/RTLPar.v | 4 | ||||
-rw-r--r-- | src/hls/RTLPargen.v | 4 | ||||
-rw-r--r-- | src/hls/RTLPargenproof.v | 4 | ||||
-rw-r--r-- | src/hls/Schedule.ml | 4 |
7 files changed, 362 insertions, 18 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index bf5c37a..4fae701 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-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 @@ -16,6 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +(* [[file:../../lit/scheduling.org::rtlblock-main][rtlblock-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Events. @@ -39,9 +40,32 @@ Definition fundef := @fundef bb. Definition program := @program bb. Definition funsig := @funsig bb. Definition stackframe := @stackframe bb. -Definition state := @state bb. + Definition genv := @genv bb. +Inductive state : Type := +| State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (b: bb) (**r current block being executed *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r register state *) + (pr: predset) (**r predicate register state *) + (m: mem), (**r memory state *) + state +| Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (args: list val) (**r arguments to the call *) + (m: mem), (**r memory state *) + state +| Returnstate: + forall (stack: list stackframe) (**r call stack *) + (v: val) (**r return value for the call *) + (m: mem), (**r memory state *) + state. + Section RELSEM. Context (ge: genv). @@ -56,19 +80,68 @@ Section RELSEM. forall state sp, step_instr_list sp state nil state. + Definition find_function + (ros: reg + ident) (rs: regset) : option fundef := + match ros with + | inl r => Genv.find_funct ge rs#r + | inr symb => + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + + Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := + | exec_RBcall: + forall s f b sp rs m res fd ros sig args pc pc' pr, + find_function ros rs = Some fd -> + funsig fd = sig -> + step_cf_instr (State s f b sp pc rs pr m) (RBcall sig ros args res pc') + E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) + | exec_RBtailcall: + forall s f b stk rs m sig ros args fd m' pc pr, + find_function ros rs = Some fd -> + funsig fd = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step_cf_instr (State s f b (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args) + E0 (Callstate s fd rs##args m') + | exec_RBbuiltin: + forall s f b sp rs m ef args res pc' vargs t vres m' pc pr, + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + step_cf_instr (State s f b sp pc rs pr m) (RBbuiltin ef args res pc') + t (State s f b sp pc' (regmap_setres res vres rs) pr m') + | exec_RBcond: + forall s f block sp rs m cond args ifso ifnot b pc pc' pr, + eval_condition cond rs##args m = Some b -> + pc' = (if b then ifso else ifnot) -> + step_cf_instr (State s f block sp pc rs pr m) (RBcond cond args ifso ifnot) + E0 (State s f block sp pc' rs pr m) + | exec_RBjumptable: + forall s f b sp rs m arg tbl n pc pc' pr, + rs#arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + step_cf_instr (State s f b sp pc rs pr m) (RBjumptable arg tbl) + E0 (State s f b sp pc' rs pr m) + | exec_RBreturn: + forall s f b stk rs m or pc m' pr, + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step_cf_instr (State s f b (Vptr stk Ptrofs.zero) pc rs pr m) (RBreturn or) + E0 (Returnstate s (regmap_optget or Vundef rs) m') + | exec_RBgoto: + forall s f b sp pc rs pr m pc', + step_cf_instr (State s f b sp pc rs pr m) (RBgoto pc') E0 (State s f b sp pc' rs pr m) + | exec_RBpred_cf: + forall s f b sp pc rs pr m cf1 cf2 st' p t, + step_cf_instr (State s f b sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> + step_cf_instr (State s f b sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'. + Inductive step: state -> trace -> state -> Prop := - | exec_bblock: - forall s f sp pc rs rs' m m' t s' bb pr pr', - f.(fn_code)!pc = Some bb -> - step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> - step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> - step (State s f sp pc rs pr m) t s' | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> step (Callstate s (Internal f) args m) - E0 (State s - f + E0 (State s f (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) @@ -101,3 +174,4 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +(* rtlblock-main ends here *) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 52259a0..7391f97 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-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 @@ -16,6 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +(* [[file:../../lit/scheduling.org::rtlblockinstr-main][rtlblockinstr-main]] *) Require Import Coq.micromega.Lia. Require Import compcert.backend.Registers. @@ -37,7 +38,7 @@ These instructions are used for [RTLBlock] and [RTLPar], so that they have consi instructions, which greatly simplifies the proofs, as they will by default have the same instruction syntax and semantics. The only changes are therefore at the top-level of the instructions. -** Instruction Definition + ** Instruction Definition First, we define the instructions that can be placed into a basic block, meaning they won't branch. The main changes to how instructions are defined in [RTL], is that these instructions don't have a @@ -346,3 +347,4 @@ Section RELSEM. step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'. End RELSEM. +(* rtlblockinstr-main ends here *) diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index 889e104..af2c5af 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-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 @@ -16,15 +16,275 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +(* [[file:../../lit/scheduling.org::rtlblockgen-main][rtlblockgen-main]] *) Require compcert.backend.RTL. Require Import compcert.common.AST. Require Import compcert.lib.Maps. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Floats. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. +#[local] Open Scope positive. + Parameter partition : RTL.function -> Errors.res function. -Definition transl_fundef := transf_partial_fundef partition. +(** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold + function to find the desired element. *) +Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive := + List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes). + +(*Compute find_block (2::94::28::40::19::nil) 40.*) + +(* [[[[file:~/projects/vericert/lit/scheduling.org::rtlblockgen-equalities][rtlblockgen-equalities]]][rtlblockgen-equalities]] *) +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_pos_eq : forall (x y : list positive), {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_pos_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_pos_eq; intro. + generalize AST.ident_eq; intro. + repeat decide equality. +Defined. + +Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool := + if eqd a b then true else false. +(* rtlblockgen-equalities ends here *) + +Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) := + match istr, istr' with + | RTL.Inop n', RBnop => (n' + 1 =? n) + | RTL.Iop op args dst n', RBop None op' args' dst' => + ceq operation_eq op op' && + ceq list_pos_eq args args' && + ceq peq dst dst' && (n' + 1 =? n) + | RTL.Iload chunk addr args dst n', RBload None chunk' addr' args' dst' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq dst dst' && + (n' + 1 =? n) + | RTL.Istore chunk addr args src n', RBstore None chunk' addr' args' src' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq src src' && + (n' + 1 =? n) + | _, _ => false + end. + +Definition check_cf_instr_body (istr: RTL.instruction) (istr': instr): bool := + match istr, istr' with + | RTL.Iop op args dst _, RBop None op' args' dst' => + ceq operation_eq op op' && + ceq list_pos_eq args args' && + ceq peq dst dst' + | RTL.Iload chunk addr args dst _, RBload None chunk' addr' args' dst' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq dst dst' + | RTL.Istore chunk addr args src _, RBstore None chunk' addr' args' src' => + ceq memory_chunk_eq chunk chunk' && + ceq addressing_eq addr addr' && + ceq list_pos_eq args args' && + ceq peq src src' + | RTL.Inop _, RBnop + | RTL.Icall _ _ _ _ _, RBnop + | RTL.Itailcall _ _ _, RBnop + | RTL.Ibuiltin _ _ _ _, RBnop + | RTL.Icond _ _ _ _, RBnop + | RTL.Ijumptable _ _, RBnop + | RTL.Ireturn _, RBnop => true + | _, _ => false + end. + +Definition check_cf_instr (istr: RTL.instruction) (istr': cf_instr) := + match istr, istr' with + | RTL.Inop n, RBgoto n' => (n =? n') + | RTL.Iop _ _ _ n, RBgoto n' => (n =? n') + | RTL.Iload _ _ _ _ n, RBgoto n' => (n =? n') + | RTL.Istore _ _ _ _ n, RBgoto n' => (n =? n') + | RTL.Icall sig (inl r) args dst n, RBcall sig' (inl r') args' dst' n' => + ceq signature_eq sig sig' && + ceq peq r r' && + ceq list_pos_eq args args' && + ceq peq dst dst' && + (n =? n') + | RTL.Icall sig (inr i) args dst n, RBcall sig' (inr i') args' dst' n' => + ceq signature_eq sig sig' && + ceq peq i i' && + ceq list_pos_eq args args' && + ceq peq dst dst' && + (n =? n') + | RTL.Itailcall sig (inl r) args, RBtailcall sig' (inl r') args' => + ceq signature_eq sig sig' && + ceq peq r r' && + ceq list_pos_eq args args' + | RTL.Itailcall sig (inr r) args, RBtailcall sig' (inr r') args' => + ceq signature_eq sig sig' && + ceq peq r r' && + ceq list_pos_eq args args' + | RTL.Icond cond args n1 n2, RBcond cond' args' n1' n2' => + ceq condition_eq cond cond' && + ceq list_pos_eq args args' && + ceq peq n1 n1' && ceq peq n2 n2' + | RTL.Ijumptable r ns, RBjumptable r' ns' => + ceq peq r r' && ceq list_pos_eq ns ns' + | RTL.Ireturn (Some r), RBreturn (Some r') => + ceq peq r r' + | RTL.Ireturn None, RBreturn None => true + | _, _ => false + end. + +Definition is_cf_instr (n: positive) (i: RTL.instruction) := + match i with + | RTL.Inop n' => negb (n' + 1 =? n) + | RTL.Iop _ _ _ n' => negb (n' + 1 =? n) + | RTL.Iload _ _ _ _ n' => negb (n' + 1 =? n) + | RTL.Istore _ _ _ _ n' => negb (n' + 1 =? n) + | RTL.Icall _ _ _ _ _ => true + | RTL.Itailcall _ _ _ => true + | RTL.Ibuiltin _ _ _ _ => true + | RTL.Icond _ _ _ _ => true + | RTL.Ijumptable _ _ => true + | RTL.Ireturn _ => true + end. + +Definition check_present_blocks (c: code) (n: list positive) (max: positive) (i: positive) (istr: RTL.instruction) := + let blockn := find_block max n i in + match c ! blockn with + | Some istrs => + match List.nth_error istrs.(bb_body) (Pos.to_nat blockn - Pos.to_nat i)%nat with + | Some istr' => + if is_cf_instr i istr + then check_cf_instr istr istrs.(bb_exit) && check_cf_instr_body istr istr' + else check_instr i istr istr' + | None => false + end + | None => false + end. + +Definition transl_function (f: RTL.function) := + match partition f with + | Errors.OK f' => + let blockids := map fst (PTree.elements f'.(fn_code)) in + if forall_ptree (check_present_blocks f'.(fn_code) blockids (fold_right Pos.max 1 blockids)) + f.(RTL.fn_code) then + Errors.OK f' + else Errors.Error (Errors.msg "check_present_blocks failed") + | Errors.Error msg => Errors.Error msg + end. + +Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program : RTL.program -> Errors.res program := transform_partial_program transl_fundef. +(* rtlblockgen-main ends here *) diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 4986cff..bcb51c6 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-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 @@ -16,6 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +(* [[file:../../lit/scheduling.org::rtlpar-main][rtlpar-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Events. @@ -138,3 +139,4 @@ Definition max_pc_function (f: function) : positive := (pc + match Zlength i.(bb_body) with Z.pos p => p | _ => 1 end))%positive) f.(fn_code) 1%positive. +(* rtlpar-main ends here *) diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index ab4c0da..f3d13f5 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-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 @@ -16,6 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +(* [[file:../../lit/scheduling.org::rtlpargen-main][rtlpargen-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. @@ -260,3 +261,4 @@ Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. +(* rtlpargen-main ends here *) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 0023edc..63a294e 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-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 @@ -16,6 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +(* [[file:../../lit/scheduling.org::rtlpargenproof-main][rtlpargenproof-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. @@ -1135,3 +1136,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. +(* rtlpargenproof-main ends here *) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 11c7308..88aa6fd 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-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 @@ -16,6 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +(* [[file:../../lit/scheduling.org::scheduler-main][scheduler-main]] *) open Printf open Clflags open Camlcoq @@ -881,3 +882,4 @@ let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = fn_code = scheduled (*List.fold_left (add_to_tree scheduled) PTree.empty reachable*); fn_entrypoint = f.fn_entrypoint } +(* scheduler-main ends here *) |