aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLBlockInstr.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
-rw-r--r--src/hls/RTLBlockInstr.v309
1 files changed, 182 insertions, 127 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index d9f3e74..4631b5a 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -1,20 +1,32 @@
-(*
- * 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/>.
- *)
+(*|
+..
+ Vericert: Verified high-level synthesis.
+ Copyright (C) 2019-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/>.
+
+=============
+RTLBlockInstr
+=============
+
+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.
+
+.. coq:: none
+|*)
Require Import Coq.micromega.Lia.
@@ -31,38 +43,41 @@ Require Import compcert.verilog.Op.
Require Import Predicate.
Require Import Vericertlib.
-(*|
-=====================
-RTLBlock Instructions
-=====================
+Definition node := positive.
-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.
+(*|
+.. index::
+ triple: definition; RTLBlockInstr; instruction
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``).
+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``).
|*)
-Definition node := positive.
-
Inductive instr : Type :=
| RBnop : instr
-| RBop : option pred_op -> operation -> list reg -> reg -> instr
-| 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.
+| RBop :
+ option pred_op -> operation -> list reg -> reg -> instr
+| 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.
(*|
+.. index::
+ triple: definition; RTLBlockInstr; control-flow instruction
+
Control-Flow Instruction Definition
===================================
-These are the instructions that count as control-flow, and will be placed at the end of the basic
-blocks.
+These are the instructions that count as control-flow, and will be placed at the
+end of the basic blocks.
|*)
Inductive cf_instr : Type :=
@@ -77,7 +92,7 @@ Inductive cf_instr : Type :=
| RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
(*|
-Helper functions
+Helper Functions
================
|*)
@@ -90,35 +105,36 @@ Fixpoint successors_instr (i : cf_instr) : list node :=
| RBjumptable arg tbl => tbl
| RBreturn optarg => nil
| RBgoto n => n :: nil
- | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil)
+ | RBpred_cf p c1 c2 =>
+ concat (successors_instr c1 :: successors_instr c2 :: nil)
end.
Definition max_reg_instr (m: positive) (i: instr) :=
match i with
| RBnop => m
| RBop p op args res =>
- fold_left Pos.max args (Pos.max res m)
+ fold_left Pos.max args (Pos.max res m)
| RBload p chunk addr args dst =>
- fold_left Pos.max args (Pos.max dst m)
+ fold_left Pos.max args (Pos.max dst m)
| RBstore p chunk addr args src =>
- fold_left Pos.max args (Pos.max src m)
+ fold_left Pos.max args (Pos.max src m)
| RBsetpred p' c args p =>
- fold_left Pos.max args m
+ fold_left Pos.max args m
end.
Fixpoint 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))
+ 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)
+ fold_left Pos.max args (Pos.max res m)
| RBtailcall sig (inl r) args =>
- fold_left Pos.max args (Pos.max r m)
+ fold_left Pos.max args (Pos.max r m)
| RBtailcall sig (inr id) args =>
- fold_left Pos.max args m
+ 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)
+ (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
@@ -134,7 +150,7 @@ Definition eval_predf (pr: predset) (p: pred_op) :=
sat_predicate p (fun x => pr !! (Pos.of_nat x)).
#[global]
-Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
+ Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
Proof.
unfold Proper. simplify. unfold "==>".
intros.
@@ -159,9 +175,10 @@ Lemma eval_predf_pr_equiv :
eval_predf ps p = eval_predf ps' p.
Proof.
induction p; simplify; auto;
- try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
- [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
- erewrite IHp1; try eassumption; erewrite IHp2; eauto.
+ try (unfold eval_predf; simplify;
+ repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
+ [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
+ erewrite IHp1; try eassumption; erewrite IHp2; eauto.
Qed.
Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
@@ -177,16 +194,16 @@ 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_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.
|*)
Record instr_state := mk_instr_state {
- is_rs: regset;
- is_ps: predset;
- is_mem: mem;
-}.
+ is_rs: regset;
+ is_ps: predset;
+ is_mem: mem;
+ }.
(*|
Top-Level Type Definitions
@@ -198,19 +215,19 @@ Section DEFINITION.
Context {bblock_body: Type}.
Record bblock : Type := mk_bblock {
- bb_body: bblock_body;
- bb_exit: cf_instr
- }.
+ bb_body: list bblock_body;
+ bb_exit: cf_instr
+ }.
Definition code: Type := PTree.t bblock.
Record function: Type := mkfunction {
- fn_sig: signature;
- fn_params: list reg;
- fn_stacksize: Z;
- fn_code: code;
- fn_entrypoint: node
- }.
+ fn_sig: signature;
+ fn_params: list reg;
+ fn_stacksize: Z;
+ fn_code: code;
+ fn_entrypoint: node
+ }.
Definition fundef := AST.fundef function.
@@ -224,35 +241,45 @@ Section DEFINITION.
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 *)
- (pr: predset), (**r predicate state of the calling function *)
+ 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 *)
+ (pr: predset), (**r predicate state of the calling
+ function *)
stackframe.
- Inductive state : Type :=
- | State:
+(*|
+State Definition
+----------------
+
+Definition of the ``state`` type, which is used by the ``step`` functions.
+|*)
+
+ Variant 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] *)
+ (il: list bblock_body) (**r basic block body that is
+ currently executing. *)
(rs: regset) (**r register state *)
(pr: predset) (**r predicate register state *)
(m: mem), (**r memory state *)
- state
- | Callstate:
+ 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:
+ state
+ | Returnstate:
forall (stack: list stackframe) (**r call stack *)
(v: val) (**r return value for the call *)
(m: mem), (**r memory state *)
- state.
+ state.
End DEFINITION.
@@ -274,94 +301,122 @@ Section RELSEM.
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
+ match Genv.find_symbol ge symb with
+ | None => None
+ | Some b => Genv.find_funct_ptr ge b
+ end
end.
- Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+ Inductive eval_pred:
+ option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
| eval_pred_true:
- forall i i' p,
+ forall i i' p,
eval_predf (is_ps i) p = true ->
eval_pred (Some p) i i' i'
| eval_pred_false:
- forall i i' p,
+ forall i i' p,
eval_predf (is_ps i) p = false ->
eval_pred (Some p) i i' i
| eval_pred_none:
- forall i i', eval_pred None i i' i.
+ forall i i', eval_pred None i i' i.
+
+ (*|
+.. index::
+ triple: semantics; RTLBlockInstr; instruction
+
+Step Instruction
+=============================
+|*)
Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
| exec_RBnop:
- forall sp ist,
- step_instr sp ist RBnop ist
+ forall sp ist,
+ step_instr sp ist RBnop ist
| exec_RBop:
- forall op v res args rs m sp p ist pr,
- eval_operation ge sp op rs##args m = Some v ->
- eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist ->
- step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist
+ forall op v res args rs m sp p ist pr,
+ eval_operation ge sp op rs##args m = Some v ->
+ eval_pred p (mk_instr_state rs pr m)
+ (mk_instr_state (rs#res <- v) pr m) ist ->
+ step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist
| exec_RBload:
- forall addr rs args a chunk m v dst sp p pr ist,
- eval_addressing ge sp addr rs##args = Some a ->
- Mem.loadv chunk m a = Some v ->
- eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist ->
- step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist
+ forall addr rs args a chunk m v dst sp p pr ist,
+ eval_addressing ge sp addr rs##args = Some a ->
+ Mem.loadv chunk m a = Some v ->
+ eval_pred p (mk_instr_state rs pr m)
+ (mk_instr_state (rs#dst <- v) pr m) ist ->
+ step_instr sp (mk_instr_state rs pr m)
+ (RBload p chunk addr args dst) ist
| exec_RBstore:
- forall addr rs args a chunk m src m' sp p pr ist,
- eval_addressing ge sp addr rs##args = Some a ->
- Mem.storev chunk m a rs#src = Some m' ->
- eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist ->
- step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist
+ forall addr rs args a chunk m src m' sp p pr ist,
+ eval_addressing ge sp addr rs##args = Some a ->
+ Mem.storev chunk m a rs#src = Some m' ->
+ eval_pred p (mk_instr_state rs pr m)
+ (mk_instr_state rs pr m') ist ->
+ step_instr sp (mk_instr_state rs pr m)
+ (RBstore p chunk addr args src) ist
| exec_RBsetpred:
- forall sp rs pr m p c b args p' ist,
+ forall sp rs pr m p c b args p' ist,
Op.eval_condition c rs##args m = Some b ->
- eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist ->
- step_instr sp (mk_instr_state rs pr m) (RBsetpred p' c args p) ist.
+ eval_pred p' (mk_instr_state rs pr m)
+ (mk_instr_state rs (pr#p <- b) m) ist ->
+ step_instr sp (mk_instr_state rs pr m)
+ (RBsetpred p' c args p) ist.
+
+ (*|
+.. index::
+ triple: semantics; RTLBlockInstr; control-flow instruction
+
+Step Control-Flow Instruction
+=============================
+|*)
Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
| exec_RBcall:
forall s f 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 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)
+ step_cf_instr (State s f sp pc nil 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 stk rs m sig ros args fd m' pc pr,
+ forall s f 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 (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args)
- E0 (Callstate s fd rs##args m')
+ step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc nil rs pr m)
+ (RBtailcall sig ros args)
+ E0 (Callstate s fd rs##args m')
| exec_RBbuiltin:
- forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
+ forall s f 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 sp pc rs pr m) (RBbuiltin ef args res pc')
- t (State s f sp pc' (regmap_setres res vres rs) pr m')
+ step_cf_instr (State s f sp pc nil rs pr m) (RBbuiltin ef args res pc')
+ t (State s f sp pc' nil (regmap_setres res vres rs) pr m')
| exec_RBcond:
- forall s f sp rs m cond args ifso ifnot b pc pc' pr,
+ forall s f 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 sp pc rs pr m) (RBcond cond args ifso ifnot)
- E0 (State s f sp pc' rs pr m)
+ step_cf_instr (State s f sp pc nil rs pr m) (RBcond cond args ifso ifnot)
+ E0 (State s f sp pc' nil rs pr m)
| exec_RBjumptable:
- forall s f sp rs m arg tbl n pc pc' pr,
+ forall s f 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 sp pc rs pr m) (RBjumptable arg tbl)
- E0 (State s f sp pc' rs pr m)
+ step_cf_instr (State s f sp pc nil rs pr m) (RBjumptable arg tbl)
+ E0 (State s f sp pc' nil rs pr m)
| exec_RBreturn:
- forall s f stk rs m or pc m' pr,
+ forall s f stk rs m or pc m' pr,
Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
- step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBreturn or)
- E0 (Returnstate s (regmap_optget or Vundef rs) m')
+ step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc nil rs pr m) (RBreturn or)
+ E0 (Returnstate s (regmap_optget or Vundef rs) m')
| exec_RBgoto:
- forall s f sp pc rs pr m pc',
- step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m)
+ forall s f sp pc rs pr m pc',
+ step_cf_instr (State s f sp pc nil rs pr m) (RBgoto pc') E0
+ (State s f sp pc' nil rs pr m)
| exec_RBpred_cf:
- forall s f sp pc rs pr m cf1 cf2 st' p t,
- step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
- step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'.
+ forall s f sp pc rs pr m cf1 cf2 st' p t,
+ step_cf_instr (State s f sp pc nil rs pr m)
+ (if eval_predf pr p then cf1 else cf2) t st' ->
+ step_cf_instr (State s f sp pc nil rs pr m)
+ (RBpred_cf p cf1 cf2) t st'.
End RELSEM.
generated by cgit (git 2.34.1) at 2024-07-17 05:46:01 +0000