diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compiler.v | 76 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 17 | ||||
| -rw-r--r-- | src/common/Maps.v | 12 | ||||
| -rw-r--r-- | src/common/Vericertlib.v | 32 | ||||
| -rw-r--r-- | src/hls/Array.v | 10 | ||||
| -rw-r--r-- | src/hls/HTLPargen.v | 20 | ||||
| -rw-r--r-- | src/hls/RTLBlock.v | 115 | ||||
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 154 | ||||
| -rw-r--r-- | src/hls/RTLPar.v | 203 | ||||
| -rw-r--r-- | src/hls/RTLPargen.v | 51 | ||||
| -rw-r--r-- | src/hls/Scheduleoracle.v | 181 |
11 files changed, 546 insertions, 325 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index ce36d5b..0578f57 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -36,49 +36,39 @@ Imports We first need to import all of the modules that are used in the correctness proof, which includes all of the passes that are performed in Vericert and the CompCert front end. |*) -From vericert Require Import HTLgenproof. - -From compcert.common Require Import - Errors - Linking. - -From compcert.lib Require Import - Coqlib. - -From compcert.backend Require - Selection - RTL - RTLgen - Tailcall - Inlining - Renumber - Constprop - CSE - Deadcode - Unusedglob. - -From compcert.cfrontend Require - Csyntax - SimplExpr - SimplLocals - Cshmgen - Cminorgen. - -From compcert.driver Require - Compiler. - -From vericert Require - Verilog - Veriloggen - Veriloggenproof - HTLgen - RTLBlock - RTLBlockgen - RTLPargen - HTLPargen - Pipeline. - -From compcert Require Import Smallstep. +Require compcert.backend.Selection. +Require compcert.backend.RTL. +Require compcert.backend.RTLgen. +Require compcert.backend.Tailcall. +Require compcert.backend.Inlining. +Require compcert.backend.Renumber. +Require compcert.backend.Constprop. +Require compcert.backend.CSE. +Require compcert.backend.Deadcode. +Require compcert.backend.Unusedglob. +Require compcert.cfrontend.Csyntax. +Require compcert.cfrontend.SimplExpr. +Require compcert.cfrontend.SimplLocals. +Require compcert.cfrontend.Cshmgen. +Require compcert.cfrontend.Cminorgen. +Require compcert.driver.Compiler. + +Require Import compcert.common.Errors. +Require Import compcert.common.Linking. +Require Import compcert.common.Smallstep. +Require Import compcert.lib.Coqlib. + +Require vericert.hls.Verilog. +Require vericert.hls.Veriloggen. +Require vericert.hls.Veriloggenproof. +Require vericert.hls.HTLgen. +Require vericert.hls.RTLBlock. +Require vericert.hls.RTLBlockgen. +Require vericert.hls.RTLPargen. +Require vericert.hls.HTLPargen. +Require vericert.hls.Pipeline. + +Require Import vericert.hls.HTLgenproof. (*| Declarations diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index d36fcee..2b6cded 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -17,13 +17,14 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import BinInt. -Require Import Lia. -Require Import ZBinary. +Require Import Coq.ZArith.BinInt. +Require Import Coq.micromega.Lia. +Require Import Coq.Numbers.Integer.Binary.ZBinary. -From compcert Require Import Integers Coqlib. +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. -Require Import Vericertlib. +Require Import vericert.common.Vericertlib. Local Open Scope Z_scope. @@ -337,7 +338,7 @@ Module IntExtra. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. - apply zlt_true. omega. omega. + apply zlt_true. lia. lia. Qed. Lemma bits_byte3: @@ -347,7 +348,7 @@ Module IntExtra. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). - apply zlt_true. omega. omega. + apply zlt_true. lia. lia. Qed. Lemma bits_byte4: @@ -357,7 +358,7 @@ Module IntExtra. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). - apply zlt_true. omega. omega. + apply zlt_true. lia. lia. Qed. Lemma bits_ofwords: diff --git a/src/common/Maps.v b/src/common/Maps.v index 696c9b8..f0f264d 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -17,13 +17,15 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From vericert Require Import Vericertlib. +Set Implicit Arguments. -From compcert Require Export Maps. -From compcert Require Import Errors. -Import PTree. +Require Export compcert.lib.Maps. -Set Implicit Arguments. +Require Import compcert.common.Errors. + +Require Import vericert.common.Vericertlib. + +Import PTree. Local Open Scope error_monad_scope. diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index d9176db..4f6c6fa 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -1,6 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2021 Yann Herklotz <yann@yannherklotz.com> + * 2020 James Pollard <j@mes.dev> * * 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,21 +17,23 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From Coq Require Export - String - ZArith - Znumtheory - List - Bool. +Set Implicit Arguments. -Require Import Lia. +Require Export Coq.Bool.Bool. +Require Export Coq.Lists.List. +Require Export Coq.Strings.String. +Require Export Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coq.micromega.Lia. -From vericert Require Import Show. +Require Export compcert.lib.Coqlib. +Require Import compcert.lib.Integers. + +Require Export vericert.common.VericertTactics. +Require Import vericert.common.Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) -From compcert.lib Require Export Coqlib. -From compcert Require Import Integers. Local Open Scope Z_scope. @@ -70,7 +73,9 @@ Ltac solve_by_invert := solve_by_inverts 1. Ltac invert x := inversion x; subst; clear x. Ltac destruct_match := - match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end. + match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? end. + +Ltac auto_destruct x := destruct_with_eqn x; simpl in *; try discriminate; try congruence. Ltac nicify_hypotheses := repeat match goal with @@ -180,7 +185,8 @@ Ltac liapp := | _ => idtac end. -Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption. +Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; + try assumption; try (solve [auto]). Global Opaque Nat.div. Global Opaque Z.mul. diff --git a/src/hls/Array.v b/src/hls/Array.v index 5c7ebc7..dec1335 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -18,9 +18,11 @@ Set Implicit Arguments. -Require Import Lia. -Require Import Vericertlib. -From Coq Require Import Lists.List Datatypes. +Require Import Coq.Init.Datatypes. +Require Import Coq.Lists.List. +Require Import Coq.micromega.Lia. + +Require Import vericert.common.Vericertlib. Import ListNotations. @@ -74,7 +76,7 @@ Lemma array_set_wf {A : Type} : Proof. induction l; intros; destruct i; auto. - invert H; crush; auto. + invert H; crush. Qed. Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 474dfef..70c0454 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -16,11 +16,21 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Errors Globalenvs Integers. -From compcert Require Import Maps AST. -From vericert Require Import Verilog RTLPar HTL Vericertlib AssocMap ValueInt Statemonad. - -Import Lia. +Require Import Coq.micromega.Lia. + +Require Import compcert.common.AST. +Require compcert.common.Errors. +Require compcert.common.Globalenvs. +Require compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.HTL. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.ValueInt. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index dc505ed..a8efa33 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,25 +52,63 @@ 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. +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. -(* Definition genv := Genv.t fundef unit. -Definition regset := Regmap.t val. +Inductive state : Type := +| State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r 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. + +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. +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: state -> trace -> state -> Prop := + | exec_bblock: + forall f pc bb cfi, + (fn_code f)!pc = Some (mk_bblock _ bb cfi) -> + step_instr_list (InstrState rs m) bb (InstrState rs' m') + step . + +End RELSEM. + +(* Inductive stackframe : Type := | Stackframe: diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v new file mode 100644 index 0000000..f9d1073 --- /dev/null +++ b/src/hls/RTLBlockInstr.v @@ -0,0 +1,154 @@ +(* + * 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 mk_bblock [bblock_body]. +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. + +Inductive cf_instr_state : Type := +| CfInstrState: + forall () + +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. + + Inductive step_cf_instr: + +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."). diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index b5aa86d..7c22995 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -20,9 +20,18 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import Globalenvs Values Integers Floats Maps. -Require RTLBlock RTLPar Op Memory AST Registers. -Require Import Vericertlib. +Require compcert.backend.Registers. +Require compcert.common.AST. +Require Import compcert.common.Globalenvs. +Require compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.lib.Floats. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require compcert.verilog.Op. +Require vericert.hls.RTLBlock. +Require vericert.hls.RTLPar. +Require Import vericert.common.Vericertlib. (*| Schedule Oracle @@ -154,9 +163,7 @@ Module R_indexed. end. Lemma index_inj: forall (x y: t), index x = index y -> x = y. - Proof. - destruct x; destruct y; intro; try (simpl in H; congruence). - Qed. + Proof. destruct x; destruct y; crush. Qed. Definition eq := resource_eq. End R_indexed. @@ -309,61 +316,16 @@ Scheme expression_ind2 := Induction for expression Sort Prop Lemma beq_expression_correct: forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. Proof. - intro e1. + intro e1; apply expression_ind2 with - (P := fun (e1: expression) => forall e2, beq_expression e1 e2 = true -> e1 = e2) - (P0 := fun (e1: expression_list) => forall e2, beq_expression_list e1 e2 = true -> e1 = e2). - (* Ebase *) - intros r e2. - destruct e2; simpl; try congruence. - case (resource_eq r r0); congruence. - - (* Eop *) - intros o e HR e2. destruct e2; simpl; try congruence. - case (operation_eq o o0); intros. generalize (HR _ H). - congruence. congruence. - - (* Eload *) - intros m a e HR e3 HR3. destruct e2 ; simpl ; try congruence. - case (memory_chunk_eq m m0). - case (addressing_eq a a0). - caseEq (beq_expression_list e e0). - caseEq (beq_expression e3 e2). - intros. - generalize (HR e0 H0). generalize (HR3 e2 H). intros. - subst. trivial. - intros; discriminate. - intros; discriminate. - intros; discriminate. - intros; discriminate. - - (* Estore *) - intros e3 HR2 m a e HR e4 HR4 e2. - destruct e2; simpl; try congruence. - case (memory_chunk_eq m m0). case (addressing_eq a a0). - (*case (beq_expression_list e e0). case (beq_expression e3 e2). *) - intros. - caseEq (beq_expression_list e e0). intro. rewrite H0 in H. - caseEq (beq_expression e3 e2_1). intro. rewrite H1 in H. - generalize (HR2 e2_1 H1). intro. generalize (HR e0 H0). - generalize (HR4 e2_2 H). - congruence. - intro. rewrite H1 in H. discriminate. - intro. rewrite H0 in H. discriminate. - intros; congruence. - intros; congruence. - - (* Enil *) - intro e2. - unfold beq_expression_list. - case e2; intros; try congruence; trivial. - - (* Econs *) - intros e HR1 e0 HR2 e2. - destruct e2; simpl; try congruence. - caseEq (beq_expression e e2); caseEq (beq_expression_list e0 e3); simpl; try congruence. - intros. clear H1. generalize (HR1 e2 H0). generalize (HR2 e3 H). - congruence. + (P := fun (e1 : expression) => + forall e2, beq_expression e1 e2 = true -> e1 = e2) + (P0 := fun (e1 : expression_list) => + forall e2, beq_expression_list e1 e2 = true -> e1 = e2); simplify; + repeat match goal with + | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? + | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? + end; subst; f_equal; crush. Qed. Definition empty : forest := Rtree.empty _. @@ -377,67 +339,93 @@ Definition check := Rtree.beq beq_expression. Lemma check_correct: forall (fa fb : forest) (x : resource), check fa fb = true -> (forall x, fa # x = fb # x). Proof. - unfold check, get_forest. - intros fa fb res Hbeq x. - pose proof Hbeq as Hbeq2. - pose proof (Rtree.beq_sound beq_expression fa fb) as Hsound. - specialize (Hsound Hbeq2 x). - destruct (Rtree.get x fa) eqn:?; destruct (Rtree.get x fb) eqn:?; try contradiction. - apply beq_expression_correct. assumption. trivial. + unfold check, get_forest; intros; + pose proof beq_expression_correct; + match goal with + [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => + apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq + end; + repeat destruct_match; crush. Qed. Lemma get_empty: forall r, empty#r = Ebase r. Proof. - intros r. unfold get_forest. - destruct (Rtree.get r empty) eqn:Heq; auto. - rewrite Rtree.gempty in Heq. discriminate. + intros; unfold get_forest; + destruct_match; auto; [ ]; + match goal with + [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H + end; discriminate. +Qed. + +Fixpoint beq2 {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 + && beq2 beqA l1 l2 && beq2 beqA r1 r2 + end. + +Lemma beq2_correct: + forall A B beqA m1 m2, + @beq2 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 beq2. 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. Lemma map0: forall r, empty # r = Ebase r. -Proof. - intros. eapply get_empty. -Qed. +Proof. intros; eapply get_empty. Qed. Lemma map1: forall w dst dst', dst <> dst' -> (empty # dst <- w) # dst' = Ebase dst'. -Proof. - intros. - unfold get_forest. - rewrite Rtree.gso. eapply map0. auto. -Qed. +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply map0. Qed. Lemma genmap1: forall (f : forest) w dst dst', dst <> dst' -> (f # dst <- w) # dst' = f # dst'. -Proof. - intros. - unfold get_forest. - rewrite Rtree.gso. reflexivity. auto. -Qed. +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. Lemma map2: forall (v : expression) x rs, (rs # x <- v) # x = v. -Proof. - intros. - unfold get_forest. - rewrite Rtree.gss. trivial. -Qed. +Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. Lemma tri1: forall x y, Reg x <> Reg y -> x <> y. -Proof. - intros. unfold not in *; intros. - rewrite H0 in H. generalize (H (refl_equal (Reg y))). - auto. -Qed. +Proof. unfold not; intros; subst; auto. Qed. (*| Update functions. @@ -472,6 +460,13 @@ Definition update_par (f : forest) (i : RTLPar.instruction) : forest := end. (*| +Implementing which are necessary to show the correctness of the translation validation by showing +that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code. +|*) + + + +(*| Get a sequence from the basic block. |*) |