diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | lit/scheduling.org | 302 | ||||
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 49 | ||||
| -rw-r--r-- | src/hls/RTLBlockgen.v | 26 |
4 files changed, 199 insertions, 183 deletions
@@ -87,7 +87,10 @@ clean:: Makefile.coq rm -f Makefile.coq detangle-all: - emacs --batch --eval "(progn(require 'org)(require 'ob-tangle)$(foreach vs,$(VS),(org-babel-detangle \"$(vs)\")))" + emacs --batch --eval "(progn(require 'org)(require 'ob-tangle)\ + (setq org-src-preserve-indentation t)\ + $(foreach vs,$(VS),(org-babel-detangle \"$(vs)\"))\ + (org-save-all-org-buffers))" clean:: rm -f */*.v.d */*.glob */*.vo */*~ *~ diff --git a/lit/scheduling.org b/lit/scheduling.org index 7970019..c3fb12a 100644 --- a/lit/scheduling.org +++ b/lit/scheduling.org @@ -13,7 +13,7 @@ <<license>> #+end_src -#+name: rtlblockinstr-main +#+name: rtlblockinstr-imports #+begin_src coq Require Import Coq.micromega.Lia. @@ -29,20 +29,20 @@ Require Import compcert.verilog.Op. Require Import Predicate. Require Import Vericertlib. +#+end_src -(** * RTLBlock Instructions - -These instructions are used for [RTLBlock] and [RTLPar], so that they have consistent -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. +These instructions are used for ~RTLBlock~ and ~RTLPar~, so that they have consistent 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 next node, as they will be in a basic block, and they also have an optional predicate ([pred_op]). -*) +#+name: rtlblockinstr-instr-def +#+begin_src coq Definition node := positive. Inductive instr : Type := @@ -51,12 +51,15 @@ Inductive instr : Type := | RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr | RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr | RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr. +#+end_src -(** ** Control-Flow Instruction Definition +*** Control-Flow Instruction Definition These are the instructions that count as control-flow, and will be placed at the end of the basic -blocks. *) +blocks. +#+name: rtlblockinstr-cf-instr-def +#+begin_src coq Inductive cf_instr : Type := | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr | RBtailcall : signature -> reg + ident -> list reg -> cf_instr @@ -67,9 +70,12 @@ Inductive cf_instr : Type := | RBreturn : option reg -> cf_instr | RBgoto : node -> cf_instr | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. +#+end_src -(** ** Helper functions *) +*** Helper functions +#+name: rtlblockinstr-helpers +#+begin_src coq Fixpoint successors_instr (i : cf_instr) : list node := match i with | RBcall sig ros args res s => s :: nil @@ -158,24 +164,30 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) | _, _ => Regmap.init Vundef end. +#+end_src -(** *** Instruction State +**** Instruction State Definition of the instruction state, which contains the following: -- [is_rs] This is the current state of the registers. -- [is_ps] This is the current state of the predicate registers, which is in a separate namespace and - area compared to the standard registers in [is_rs]. -- [is_mem] The current state of the memory. *) +- ~is_rs~ :: This is the current state of the registers. +- ~is_ps~ :: This is the current state of the predicate registers, which is in a separate namespace + and area compared to the standard registers in [is_rs]. +- ~is_mem~ :: The current state of the memory. +#+name: rtlblockinstr-instr-state +#+begin_src coq Record instr_state := mk_instr_state { is_rs: regset; is_ps: predset; is_mem: mem; }. +#+end_src -(** ** Top-Level Type Definitions *) +*** Top-Level Type Definitions +#+name: rtlblockinstr-type-def +#+begin_src coq Section DEFINITION. Context {bblock_body: Type}. @@ -238,9 +250,12 @@ Section DEFINITION. state. End DEFINITION. +#+end_src -(** ** Semantics *) +*** Semantics +#+name: rtlblockinstr-semantics +#+begin_src coq Section RELSEM. Context {bblock_body : Type}. @@ -1540,7 +1555,7 @@ Refers to [[rtlblockgen-equalities][rtlblockgen-equalities]]. <<license>> #+end_src -#+name: rtlblockgen-main +#+name: rtlblockgen-imports #+begin_src coq Require compcert.backend.RTL. Require Import compcert.common.AST. @@ -1553,7 +1568,15 @@ Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. #[local] Open Scope positive. +#+end_src +#+name: rtlblockgen-equalities-insert +#+begin_src coq +<<rtlblockgen-equalities>> +#+end_src + +#+name: rtlblockgen-main +#+begin_src coq Parameter partition : RTL.function -> Errors.res function. (** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold @@ -1563,124 +1586,6 @@ Definition find_block (max: positive) (nodes: list positive) (index: positive) : (*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) @@ -1812,6 +1717,129 @@ Definition transl_program : RTL.program -> Errors.res program := transform_partial_program transl_fundef. #+end_src +** Equalities (rtlblockgen-equalities) + +#+name: rtlblockgen-equalities +#+begin_src coq :tangle no +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. +#+end_src + * RTLBlockgenproof :PROPERTIES: :header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockgenproof.v diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 7391f97..770f377 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -(* [[file:../../lit/scheduling.org::rtlblockinstr-main][rtlblockinstr-main]] *) +(* [[file:../../lit/scheduling.org::rtlblockinstr-imports][rtlblockinstr-imports]] *) Require Import Coq.micromega.Lia. Require Import compcert.backend.Registers. @@ -31,20 +31,9 @@ Require Import compcert.verilog.Op. Require Import Predicate. Require Import Vericertlib. +(* rtlblockinstr-imports ends here *) -(** * RTLBlock Instructions - -These instructions are used for [RTLBlock] and [RTLPar], so that they have consistent -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 - -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 -next node, as they will be in a basic block, and they also have an optional predicate ([pred_op]). -*) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-instr-def][rtlblockinstr-instr-def]] *) Definition node := positive. Inductive instr : Type := @@ -53,12 +42,9 @@ Inductive instr : Type := | RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr | RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr | RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr. +(* rtlblockinstr-instr-def ends here *) -(** ** Control-Flow Instruction Definition - -These are the instructions that count as control-flow, and will be placed at the end of the basic -blocks. *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-cf-instr-def][rtlblockinstr-cf-instr-def]] *) Inductive cf_instr : Type := | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr | RBtailcall : signature -> reg + ident -> list reg -> cf_instr @@ -69,9 +55,9 @@ Inductive cf_instr : Type := | RBreturn : option reg -> cf_instr | RBgoto : node -> cf_instr | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. +(* rtlblockinstr-cf-instr-def ends here *) -(** ** Helper functions *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-helpers][rtlblockinstr-helpers]] *) Fixpoint successors_instr (i : cf_instr) : list node := match i with | RBcall sig ros args res s => s :: nil @@ -160,24 +146,17 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) | _, _ => Regmap.init Vundef end. +(* rtlblockinstr-helpers ends here *) -(** *** Instruction State - -Definition of the instruction state, which contains the following: - -- [is_rs] This is the current state of the registers. -- [is_ps] This is the current state of the predicate registers, which is in a separate namespace and - area compared to the standard registers in [is_rs]. -- [is_mem] The current state of the memory. *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-instr-state][rtlblockinstr-instr-state]] *) Record instr_state := mk_instr_state { is_rs: regset; is_ps: predset; is_mem: mem; }. +(* rtlblockinstr-instr-state ends here *) -(** ** Top-Level Type Definitions *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-type-def][rtlblockinstr-type-def]] *) Section DEFINITION. Context {bblock_body: Type}. @@ -240,9 +219,9 @@ Section DEFINITION. state. End DEFINITION. +(* rtlblockinstr-type-def ends here *) -(** ** Semantics *) - +(* [[file:../../lit/scheduling.org::rtlblockinstr-semantics][rtlblockinstr-semantics]] *) Section RELSEM. Context {bblock_body : Type}. @@ -347,4 +326,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 *) +(* rtlblockinstr-semantics ends here *) diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index f45151d..706cb09 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -(* [[file:../../lit/scheduling.org::rtlblockgen-main][rtlblockgen-main]] *) +(* [[file:../../lit/scheduling.org::rtlblockgen-imports][rtlblockgen-imports]] *) Require compcert.backend.RTL. Require Import compcert.common.AST. Require Import compcert.lib.Maps. @@ -28,16 +28,10 @@ Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLBlock. #[local] Open Scope positive. +(* rtlblockgen-imports ends here *) -Parameter partition : RTL.function -> Errors.res function. - -(** [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:../../lit/scheduling.org::rtlblockgen-equalities-insert][rtlblockgen-equalities-insert]] *) +(* [[[[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. @@ -155,6 +149,18 @@ 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 *) +(* rtlblockgen-equalities-insert ends here *) + +(* [[file:../../lit/scheduling.org::rtlblockgen-main][rtlblockgen-main]] *) +Parameter partition : RTL.function -> Errors.res function. + +(** [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.*) Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) := match istr, istr' with |