diff options
Diffstat (limited to 'src/hls')
| -rw-r--r-- | src/hls/Abstr.v | 42 | ||||
| -rw-r--r-- | src/hls/Partition.ml | 8 | ||||
| -rw-r--r-- | src/hls/RTLBlock.v | 94 | ||||
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 6 | ||||
| -rw-r--r-- | src/hls/RTLBlockgen.v | 262 | ||||
| -rw-r--r-- | src/hls/RTLBlockgenproof.v | 52 | ||||
| -rw-r--r-- | src/hls/RTLPar.v | 4 | ||||
| -rw-r--r-- | src/hls/RTLPargen.v | 4 | ||||
| -rw-r--r-- | src/hls/RTLPargenproof.v | 10 | ||||
| -rw-r--r-- | src/hls/Sat.v | 2 | ||||
| -rw-r--r-- | src/hls/Schedule.ml | 4 |
11 files changed, 419 insertions, 69 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 8c77636..43d7783 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -692,48 +692,6 @@ Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool := equiv_check p1 p2 end. -Definition forall_ptree {A:Type} (f:positive->A->bool) (m:Maps.PTree.t A) : bool := - Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true. - -Ltac boolInv := - match goal with - | [ H: _ && _ = true |- _ ] => - destruct (andb_prop _ _ H); clear H; boolInv - | [ H: proj_sumbool _ = true |- _ ] => - generalize (proj_sumbool_true _ H); clear H; - let EQ := fresh in (intro EQ; try subst; boolInv) - | _ => - idtac - end. - -Remark ptree_forall: - forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A), - Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true = true -> - forall i x, Maps.PTree.get i m = Some x -> f i x = true. -Proof. - intros. - set (f' := fun (res: bool) (i: positive) (x: A) => res && f i x). - set (P := fun (m: Maps.PTree.t A) (res: bool) => - res = true -> Maps.PTree.get i m = Some x -> f i x = true). - assert (P m true). - rewrite <- H. fold f'. apply Maps.PTree_Properties.fold_rec. - unfold P; intros. rewrite <- H1 in H4. auto. - red; intros. now rewrite Maps.PTree.gempty in H2. - unfold P; intros. unfold f' in H4. boolInv. - rewrite Maps.PTree.gsspec in H5. destruct (peq i k). - subst. inv H5. auto. - apply H3; auto. - red in H1. auto. -Qed. - -Lemma forall_ptree_true: - forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A), - forall_ptree f m = true -> - forall i x, Maps.PTree.get i m = Some x -> f i x = true. -Proof. - apply ptree_forall. -Qed. - Definition tree_equiv_check_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := match np2 ! n with | Some p' => equiv_check p p' diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 19c6048..d7972e5 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -28,7 +28,7 @@ open Op open RTLBlockInstr open RTLBlock -(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass +(** 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. *) let find_edge i n = let succ = RTL.successors_instr i in @@ -65,14 +65,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 = []; bb_exit = RBgoto s } + Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s } else - Errors.OK { bb_body = []; bb_exit = i' } + Errors.OK { bb_body = [RBnop]; bb_exit = 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' } else if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK { bb_body = []; bb_exit = RBgoto s } + Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s } else begin match next_bblock_from_RTL false e c s' i_n with | Errors.OK bb -> 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..f45151d 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,273 @@ * 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.*) + +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. + +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/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v new file mode 100644 index 0000000..b65abca --- /dev/null +++ b/src/hls/RTLBlockgenproof.v @@ -0,0 +1,52 @@ +(* + * Vericert: Verified high-level synthesis. + * 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 + * 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/>. + *) + +(* [[file:../../lit/scheduling.org::rtlblockgenproof-imports][rtlblockgenproof-imports]] *) +Require compcert.backend.RTL. +Require Import compcert.common.AST. +Require Import compcert.lib.Maps. + +Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLBlockgen. +(* rtlblockgenproof-imports ends here *) + +(* [[file:../../lit/scheduling.org::rtlblockgenproof-match-states][rtlblockgenproof-match-states]] *) +Inductive match_states : RTL.state -> RTLBlock.state -> Prop := +| match_state : + forall stk f tf sp pc rs m + (TF: transl_function f = OK tf), + match_states (RTL.State stk f sp pc rs m) + (RTLBlock.State stk tf sp (find_block max n i) rs m). +(* rtlblockgenproof-match-states ends here *) + +(* [[file:../../lit/scheduling.org::rtlblockgenproof-correctness][rtlblockgenproof-correctness]] *) +Section CORRECTNESS. + + Context (prog : RTL.program). + Context (tprog : RTLBlock.program). + + Context (TRANSL : match_prog prog tprog). + + Theorem transf_program_correct: + Smallstep.forward_simulation (RTL.semantics prog) (RTLBlock.semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus; eauto with htlproof. + apply senv_preserved. + +End CORRECTNESS. +(* rtlblockgenproof-correctness 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..7b262db 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-imports][rtlpargenproof-imports]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. @@ -36,7 +37,9 @@ Require Import vericert.hls.Abstr. #[local] Open Scope positive. #[local] Open Scope forest. #[local] Open Scope pred_op. +(* rtlpargenproof-imports ends here *) +(* [[file:../../lit/scheduling.org::rtlpargenproof-main][rtlpargenproof-main]] *) (*Definition is_regs i := match i with mk_instr_state rs _ => rs end. Definition is_mem i := match i with mk_instr_state _ m => m end. @@ -46,10 +49,6 @@ Inductive state_lessdef : instr_state -> instr_state -> Prop := (forall x, rs1 !! x = rs2 !! x) -> state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1). -(** *** RTLBlock to abstract translation - -Correctness of translation from RTLBlock to the abstract interpretation language. *) - Ltac inv_simp := repeat match goal with | H: exists _, _ |- _ => inv H @@ -1135,3 +1134,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. +(* rtlpargenproof-main ends here *) diff --git a/src/hls/Sat.v b/src/hls/Sat.v index b7596f6..428c176 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -119,7 +119,6 @@ Lemma satLit_contra : forall s l a cl, -> satClause cl a. unfold satLit, upd; simpl; intros. destruct (eq_nat_dec (snd l) (snd l)); intuition. - assert False; intuition. Qed. #[local] Hint Resolve satLit_contra : core. @@ -287,6 +286,7 @@ Lemma unitClauseTrue : forall l a fm, induction fm; intuition. inversion H. inversion H; subst; simpl in H0; intuition. + apply IHfm; eauto. inv H0. eauto. Qed. #[local] Hint Resolve unitClauseTrue : core. 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 *) |