diff options
| -rw-r--r-- | src/hls/RTLBlock.v | 62 | ||||
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 147 | ||||
| -rw-r--r-- | src/hls/RTLPar.v | 203 | ||||
| -rw-r--r-- | src/hls/RTLPargen.v | 51 |
4 files changed, 314 insertions, 149 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index dc505ed..8a8f7f9 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2021 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,36 +16,23 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import Coqlib Maps. -Require Import AST Integers Values Events Memory Globalenvs Smallstep. -Require Import Op Registers. +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Events. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Values. +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. -Definition node := positive. +Require Import vericert.hls.RTLBlockInstr. -Inductive instruction : Type := -| RBnop : instruction -| RBop : operation -> list reg -> reg -> instruction -| RBload : memory_chunk -> addressing -> list reg -> reg -> instruction -| RBstore : memory_chunk -> addressing -> list reg -> reg -> instruction. +Definition bblock_body : Type := list instr. -Definition bblock_body : Type := list instruction. - -Inductive control_flow_inst : Type := -| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst -| RBtailcall : signature -> reg + ident -> list reg -> control_flow_inst -| RBbuiltin : external_function -> list (builtin_arg reg) -> - builtin_res reg -> node -> control_flow_inst -| RBcond : condition -> list reg -> node -> node -> control_flow_inst -| RBjumptable : reg -> list node -> control_flow_inst -| RBreturn : option reg -> control_flow_inst -| RBgoto : node -> control_flow_inst. - -Record bblock : Type := mk_bblock { - bb_body: bblock_body; - bb_exit: option control_flow_inst - }. - -Definition code : Type := PTree.t bblock. +Definition code : Type := PTree.t (bblock bblock_body). Record function: Type := mkfunction { fn_sig: signature; @@ -65,18 +52,7 @@ Definition funsig (fd: fundef) := | External ef => ef_sig ef end. -Definition successors_instr (i : control_flow_inst) : list node := - match i with - | RBcall sig ros args res s => s :: nil - | RBtailcall sig ros args => nil - | RBbuiltin ef args res s => s :: nil - | RBcond cond args ifso ifnot => ifso :: ifnot :: nil - | RBjumptable arg tbl => tbl - | RBreturn optarg => nil - | RBgoto n => n :: nil - end. - -(* Definition genv := Genv.t fundef unit. +Definition genv := Genv.t fundef unit. Definition regset := Regmap.t val. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := @@ -85,6 +61,12 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | _, _ => Regmap.init Vundef end. +Section RELSEM. + +End RELSEM. + +(* + Inductive stackframe : Type := | Stackframe: forall (res: reg) (**r where to store the result *) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v new file mode 100644 index 0000000..8549209 --- /dev/null +++ b/src/hls/RTLBlockInstr.v @@ -0,0 +1,147 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 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.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.verilog.Op. + +Require Import vericert.common.Vericertlib. + +Local Open Scope rtl. + +Definition node := positive. + +Inductive instr : Type := +| RBnop : instr +| RBop : operation -> list reg -> reg -> instr +| RBload : memory_chunk -> addressing -> list reg -> reg -> instr +| RBstore : memory_chunk -> addressing -> list reg -> reg -> instr. + +Inductive 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) -> + builtin_res reg -> node -> cf_instr +| RBcond : condition -> list reg -> node -> node -> cf_instr +| RBjumptable : reg -> list node -> cf_instr +| RBreturn : option reg -> cf_instr +| RBgoto : node -> cf_instr. + +Record bblock (bblock_body : Type) : Type := mk_bblock { + bb_body: bblock_body; + bb_exit: option cf_instr + }. +Arguments bb_body [bblock_body]. +Arguments bb_exit [bblock_body]. + +Definition successors_instr (i : cf_instr) : list node := + match i with + | RBcall sig ros args res s => s :: nil + | RBtailcall sig ros args => nil + | RBbuiltin ef args res s => s :: nil + | RBcond cond args ifso ifnot => ifso :: ifnot :: nil + | RBjumptable arg tbl => tbl + | RBreturn optarg => nil + | RBgoto n => n :: nil + end. + +Definition max_reg_instr (m: positive) (i: instr) := + match i with + | RBnop => m + | RBop op args res => fold_left Pos.max args (Pos.max res m) + | RBload chunk addr args dst => fold_left Pos.max args (Pos.max dst m) + | RBstore chunk addr args src => fold_left Pos.max args (Pos.max src m) + end. + +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)) + | RBcall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m) + | RBtailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m) + | RBtailcall sig (inr id) args => fold_left Pos.max args m + | RBbuiltin ef args res s => + fold_left Pos.max (params_of_builtin_args args) + (fold_left Pos.max (params_of_builtin_res res) m) + | RBcond cond args ifso ifnot => fold_left Pos.max args m + | RBjumptable arg tbl => Pos.max arg m + | RBreturn None => m + | RBreturn (Some arg) => Pos.max arg m + | RBgoto n => m + end. + +Definition regset := Regmap.t val. + +Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := + match rl, vl with + | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) + | _, _ => Regmap.init Vundef + end. + +Inductive instr_state : Type := + | InstrState : + forall (rs : regset) + (m : mem), + instr_state. + +Section RELSEM. + + Context (fundef : Type). + + Definition genv := Genv.t fundef unit. + + Context (ge : genv) (sp : val). + + Inductive step_instr : instr_state -> instr -> instr_state -> Prop := + | exec_RBnop : + forall rs m, + step_instr (InstrState rs m) RBnop (InstrState rs m) + | exec_RBop : + forall op v res args rs m, + eval_operation ge sp op rs##args m = Some v -> + step_instr (InstrState rs m) + (RBop op args res) + (InstrState (rs#res <- v) m) + | exec_RBload : + forall addr rs args a chunk m v dst, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + step_instr (InstrState rs m) + (RBload chunk addr args dst) + (InstrState (rs#dst <- v) m) + | exec_RBstore : + forall addr rs args a chunk m src m', + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + step_instr (InstrState rs m) + (RBstore chunk addr args src) + (InstrState rs m'). + + Inductive step_instr_list : instr_state -> list instr -> instr_state -> Prop := + | exec_RBcons : + forall state i state' state'' instrs, + step_instr state i state' -> + step_instr_list state' instrs state'' -> + step_instr_list state (i :: instrs) state'' + | exec_RBnil : + forall state, + step_instr_list state nil state. + +End RELSEM. diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index cb755e5..36431ae 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -16,34 +16,21 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import Coqlib Maps. -From compcert Require Import AST Integers Values Events Memory Globalenvs Smallstep. -From compcert Require Import Op Registers. - -Definition node := positive. - -Inductive instruction : Type := -| RPnop : instruction -| RPop : operation -> list reg -> reg -> instruction -| RPload : memory_chunk -> addressing -> list reg -> reg -> instruction -| RPstore : memory_chunk -> addressing -> list reg -> reg -> instruction. - -Definition bblock_body : Type := list (list instruction). - -Inductive control_flow_inst : Type := -| RPcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst -| RPtailcall : signature -> reg + ident -> list reg -> control_flow_inst -| RPbuiltin : external_function -> list (builtin_arg reg) -> - builtin_res reg -> node -> control_flow_inst -| RPcond : condition -> list reg -> node -> node -> control_flow_inst -| RPjumptable : reg -> list node -> control_flow_inst -| RPreturn : option reg -> control_flow_inst -| RPgoto : node -> control_flow_inst. - -Record bblock : Type := mk_bblock { - bb_body: bblock_body; - bb_exit: option control_flow_inst - }. +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Events. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Values. +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. + +Require Import vericert.hls.RTLBlockInstr. + +Definition bblock := RTLBlockInstr.bblock (list (list instr)). Definition code : Type := PTree.t bblock. @@ -65,41 +52,6 @@ Definition funsig (fd: fundef) := | External ef => ef_sig ef end. -Definition successors_instr (i : control_flow_inst) : list node := - match i with - | RPcall sig ros args res s => s :: nil - | RPtailcall sig ros args => nil - | RPbuiltin ef args res s => s :: nil - | RPcond cond args ifso ifnot => ifso :: ifnot :: nil - | RPjumptable arg tbl => tbl - | RPreturn optarg => nil - | RPgoto n => n :: nil - end. - -Definition max_reg_instr (m: positive) (i: instruction) := - match i with - | RPnop => m - | RPop op args res => fold_left Pos.max args (Pos.max res m) - | RPload chunk addr args dst => fold_left Pos.max args (Pos.max dst m) - | RPstore chunk addr args src => fold_left Pos.max args (Pos.max src m) - end. - -Definition max_reg_cfi (m : positive) (i : control_flow_inst) := - match i with - | RPcall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) - | RPcall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m) - | RPtailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m) - | RPtailcall sig (inr id) args => fold_left Pos.max args m - | RPbuiltin ef args res s => - fold_left Pos.max (params_of_builtin_args args) - (fold_left Pos.max (params_of_builtin_res res) m) - | RPcond cond args ifso ifnot => fold_left Pos.max args m - | RPjumptable arg tbl => Pos.max arg m - | RPreturn None => m - | RPreturn (Some arg) => Pos.max arg m - | RPgoto n => m - end. - Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) := let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in match bb.(bb_exit) with @@ -118,7 +70,24 @@ Definition max_pc_function (f: function) : positive := with Z.pos p => p | _ => 1 end))%positive) f.(fn_code) 1%positive. -(*Inductive state : Type := +Definition genv := Genv.t fundef unit. + +Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := + match rl, vl with + | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) + | _, _ => Regmap.init Vundef + end. + +Inductive stackframe : Type := + | Stackframe: + forall (res: reg) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (pc: node) (**r program point in calling function *) + (rs: regset), (**r register state in calling function *) + stackframe. + +Inductive state : Type := | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r current function *) @@ -138,4 +107,108 @@ Definition max_pc_function (f: function) : positive := (v: val) (**r return value for the call *) (m: mem), (**r memory state *) state. -*) + +Section RELSEM. + + Context (ge : genv). + + 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_instruction : state -> trace -> state -> Prop := + | exec_Inop: + forall s f sp pc rs m pc', + (fn_code f)!pc = Some(RPnop pc') -> + step (State s f sp pc rs m) + E0 (State s f sp pc' rs m) + | exec_Iop: + forall s f sp pc rs m op args res pc' v, + (fn_code f)!pc = Some(Iop op args res pc') -> + eval_operation ge sp op rs##args m = Some v -> + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#res <- v) m) + | exec_Iload: + forall s f sp pc rs m chunk addr args dst pc' a v, + (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#dst <- v) m) + | exec_Istore: + forall s f sp pc rs m chunk addr args src pc' a m', + (fn_code f)!pc = Some(Istore chunk addr args src pc') -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + step (State s f sp pc rs m) + E0 (State s f sp pc' rs m') + | exec_Icall: + forall s f sp pc rs m sig ros args res pc' fd, + (fn_code f)!pc = Some(Icall sig ros args res pc') -> + find_function ros rs = Some fd -> + funsig fd = sig -> + step (State s f sp pc rs m) + E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m) + | exec_Itailcall: + forall s f stk pc rs m sig ros args fd m', + (fn_code f)!pc = Some(Itailcall sig ros args) -> + find_function ros rs = Some fd -> + funsig fd = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s f (Vptr stk Ptrofs.zero) pc rs m) + E0 (Callstate s fd rs##args m') + | exec_Ibuiltin: + forall s f sp pc rs m ef args res pc' vargs t vres m', + (fn_code f)!pc = Some(Ibuiltin ef args res pc') -> + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + step (State s f sp pc rs m) + t (State s f sp pc' (regmap_setres res vres rs) m') + | exec_Icond: + forall s f sp pc rs m cond args ifso ifnot b pc', + (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> + eval_condition cond rs##args m = Some b -> + pc' = (if b then ifso else ifnot) -> + step (State s f sp pc rs m) + E0 (State s f sp pc' rs m) + | exec_Ijumptable: + forall s f sp pc rs m arg tbl n pc', + (fn_code f)!pc = Some(Ijumptable arg tbl) -> + rs#arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + step (State s f sp pc rs m) + E0 (State s f sp pc' rs m) + | exec_Ireturn: + forall s f stk pc rs m or m', + (fn_code f)!pc = Some(Ireturn or) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s f (Vptr stk Ptrofs.zero) pc rs m) + E0 (Returnstate s (regmap_optget or Vundef rs) m') + | 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 + (Vptr stk Ptrofs.zero) + f.(fn_entrypoint) + (init_regs args f.(fn_params)) + m') + | exec_function_external: + forall s ef args res t m m', + external_call ef ge args m t res m' -> + step (Callstate s (External ef) args m) + t (Returnstate s res m') + | exec_return: + forall res f sp pc rs s vres m, + step (Returnstate (Stackframe res f sp pc rs :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) m). + +End RELSEM. diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 836ceac..55bf71c 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -16,56 +16,19 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import AST Maps. -From vericert Require Import Vericertlib RTLBlock RTLPar Scheduleoracle. +Require Import compcert.common.AST. +Require Import compcert.lib.Maps. -Fixpoint beq {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool := - match m1, m2 with - | PTree.Leaf, _ => PTree.bempty m2 - | _, PTree.Leaf => PTree.bempty m1 - | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => - match o1, o2 with - | None, None => true - | Some y1, Some y2 => beqA y1 y2 - | _, _ => false - end - && beq beqA l1 l2 && beq beqA r1 r2 - end. - -Lemma beq_correct: - forall A B beqA m1 m2, - @beq A B beqA m1 m2 = true <-> - (forall (x: PTree.elt), - match PTree.get x m1, PTree.get x m2 with - | None, None => True - | Some y1, Some y2 => beqA y1 y2 = true - | _, _ => False - end). -Proof. - induction m1; intros. - - simpl. rewrite PTree.bempty_correct. split; intros. - rewrite PTree.gleaf. rewrite H. auto. - generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto. - - destruct m2. - + unfold beq. rewrite PTree.bempty_correct. split; intros. - rewrite H. rewrite PTree.gleaf. auto. - generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto. - + simpl. split; intros. - * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. - destruct x; simpl. apply H1. apply H3. - destruct o; destruct o0; auto || congruence. - * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. - apply IHm1_1. intros; apply (H (xO x)). - apply IHm1_2. intros; apply (H (xI x)). -Qed. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.Scheduleoracle. Parameter schedule : RTLBlock.function -> RTLPar.function. Definition transl_function (f : RTLBlock.function) : Errors.res RTLPar.function := let tf := schedule f in - if beq schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then + if beq2 schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then Errors.OK tf else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). |