diff options
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
-rw-r--r-- | src/hls/RTLBlockInstr.v | 418 |
1 files changed, 154 insertions, 264 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 69cc709..d9f3e74 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -28,232 +28,42 @@ Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. -Require Import vericert.common.Vericertlib. -Require Import vericert.hls.Sat. -Require Import vericert.hls.FunctionalUnits. +Require Import Predicate. +Require Import Vericertlib. -Local Open Scope rtl. +(*| +===================== +RTLBlock Instructions +===================== -Definition node := positive. -Definition predicate := nat. - -Inductive pred_op : Type := -| Pvar: predicate -> pred_op -| Pnot: pred_op -> pred_op -| Pand: pred_op -> pred_op -> pred_op -| Por: pred_op -> pred_op -> pred_op. - -Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool := - match p with - | Pvar p' => a p' - | Pnot p' => negb (sat_predicate p' a) - | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a - | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a - end. - -Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := - match a with - | nil => nil - | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b) - end. - -Lemma satFormula_concat: - forall a b agn, - satFormula a agn -> - satFormula b agn -> - satFormula (a ++ b) agn. -Proof. induction a; crush. Qed. - -Lemma satFormula_concat2: - forall a b agn, - satFormula (a ++ b) agn -> - satFormula a agn /\ satFormula b agn. -Proof. - induction a; simplify; - try apply IHa in H1; crush. -Qed. - -Lemma satClause_concat: - forall a a1 a0, - satClause a a1 -> - satClause (a0 ++ a) a1. -Proof. induction a0; crush. Qed. - -Lemma satClause_concat2: - forall a a1 a0, - satClause a0 a1 -> - satClause (a0 ++ a) a1. -Proof. - induction a0; crush. - inv H; crush. -Qed. - -Lemma satClause_concat3: - forall a b c, - satClause (a ++ b) c -> - satClause a c \/ satClause b c. -Proof. - induction a; crush. - inv H; crush. - apply IHa in H0; crush. - inv H0; crush. -Qed. - -Lemma satFormula_mult': - forall p2 a a0, - satFormula p2 a0 \/ satClause a a0 -> - satFormula (map (fun x : list lit => a ++ x) p2) a0. -Proof. - induction p2; crush. - - inv H. inv H0. apply satClause_concat. auto. - apply satClause_concat2; auto. - - apply IHp2. - inv H; crush; inv H0; crush. -Qed. - -Lemma satFormula_mult2': - forall p2 a a0, - satFormula (map (fun x : list lit => a ++ x) p2) a0 -> - satClause a a0 \/ satFormula p2 a0. -Proof. - induction p2; crush. - apply IHp2 in H1. inv H1; crush. - apply satClause_concat3 in H0. - inv H0; crush. -Qed. - -Lemma satFormula_mult: - forall p1 p2 a, - satFormula p1 a \/ satFormula p2 a -> - satFormula (mult p1 p2) a. -Proof. - induction p1; crush. - apply satFormula_concat; crush. - inv H. inv H0. - apply IHp1. auto. - apply IHp1. auto. - apply satFormula_mult'; - inv H; crush. -Qed. - -Lemma satFormula_mult2: - forall p1 p2 a, - satFormula (mult p1 p2) a -> - satFormula p1 a \/ satFormula p2 a. -Proof. - induction p1; crush. - apply satFormula_concat2 in H; crush. - apply IHp1 in H0. - inv H0; crush. - apply satFormula_mult2' in H1. inv H1; crush. -Qed. - -Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := - match bound with - | O => None - | S n => - match p with - | Pvar p' => Some (((true, p') :: nil) :: nil) - | Pand p1 p2 => - match trans_pred_temp n p1, trans_pred_temp n p2 with - | Some p1', Some p2' => - Some (p1' ++ p2') - | _, _ => None - end - | Por p1 p2 => - match trans_pred_temp n p1, trans_pred_temp n p2 with - | Some p1', Some p2' => - Some (mult p1' p2') - | _, _ => None - end - | Pnot (Pvar p') => Some (((false, p') :: nil) :: nil) - | Pnot (Pnot p) => trans_pred_temp n p - | Pnot (Pand p1 p2) => trans_pred_temp n (Por (Pnot p1) (Pnot p2)) - | Pnot (Por p1 p2) => trans_pred_temp n (Pand (Pnot p1) (Pnot p2)) - end - end. +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. -Fixpoint trans_pred (bound: nat) (p: pred_op) : - option {fm: formula | forall a, - sat_predicate p a = true <-> satFormula fm a}. - refine - (match bound with - | O => None - | S n => - match p with - | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _) - | Pand p1 p2 => - match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => - Some (exist _ (p1' ++ p2') _) - | _, _ => None - end - | Por p1 p2 => - match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => - Some (exist _ (mult p1' p2') _) - | _, _ => None - end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) - | _ => None - end - end); split; intros; simpl in *; auto. - - inv H. inv H0; auto. - - admit. - - admit. - - apply satFormula_concat. - apply andb_prop in H. inv H. apply i in H0. auto. - apply andb_prop in H. inv H. apply i0 in H1. auto. - - apply satFormula_concat2 in H. simplify. apply andb_true_intro. - split. apply i in H0. auto. - apply i0 in H1. auto. - - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto. - apply i0 in H0. auto. - - apply orb_true_intro. - apply satFormula_mult2 in H. inv H. apply i in H0. auto. - apply i0 in H0. auto. -Admitted. - -Definition sat_pred (bound: nat) (p: pred_op) : - option ({al : alist | sat_predicate p (interp_alist al) = true} - + {forall a : asgn, sat_predicate p a = false}). - refine - ( match trans_pred bound p with - | Some (exist fm _) => - match boundedSat bound fm with - | Some (inleft (exist a _)) => Some (inleft (exist _ a _)) - | Some (inright _) => Some (inright _) - | None => None - end - | None => None - end ). - - apply i in s2. auto. - - intros. specialize (n a). specialize (i a). - destruct (sat_predicate p a). exfalso. - apply n. apply i. auto. auto. -Qed. +Instruction Definition +====================== -Definition sat_pred_simple (bound: nat) (p: pred_op) := - match sat_pred bound p with - | Some (inleft (exist al _)) => Some (Some al) - | Some (inright _) => Some None - | None => None - end. +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 sat_pred_temp (bound: nat) (p: pred_op) := - match trans_pred_temp bound p with - | Some fm => boundedSatSimple bound fm - | None => None - end. +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 -| RBpiped : option pred_op -> funct_node -> list reg -> instr -| RBassign : option pred_op -> funct_node -> reg -> reg -> instr -| RBsetpred : condition -> list reg -> predicate -> instr. +| RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr. + +(*| +Control-Flow Instruction Definition +=================================== + +These are the instructions that count as control-flow, and will be placed at the end of the basic +blocks. +|*) Inductive cf_instr : Type := | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr @@ -266,6 +76,11 @@ Inductive cf_instr : Type := | RBgoto : node -> cf_instr | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. +(*| +Helper functions +================ +|*) + Fixpoint successors_instr (i : cf_instr) : list node := match i with | RBcall sig ros args res s => s :: nil @@ -287,11 +102,7 @@ Definition max_reg_instr (m: positive) (i: instr) := fold_left Pos.max args (Pos.max dst m) | RBstore p chunk addr args src => fold_left Pos.max args (Pos.max src m) - | RBpiped p f args => - fold_left Pos.max args m - | RBassign p f src dst => - Pos.max src (Pos.max dst m) - | RBsetpred c args p => + | RBsetpred p' c args p => fold_left Pos.max args m end. @@ -317,6 +128,41 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := end. Definition regset := Regmap.t val. +Definition predset := PMap.t bool. + +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. +Proof. + unfold Proper. simplify. unfold "==>". + intros. + unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0. +Qed. + +#[local] Open Scope pred_op. + +Lemma eval_predf_Pand : + forall ps p p', + eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'. +Proof. unfold eval_predf; split; simplify; auto with bool. Qed. + +Lemma eval_predf_Por : + forall ps p p', + eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'. +Proof. unfold eval_predf; split; simplify; auto with bool. Qed. + +Lemma eval_predf_pr_equiv : + forall p ps ps', + (forall x, ps !! x = ps' !! x) -> + 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. +Qed. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with @@ -324,11 +170,28 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | _, _ => Regmap.init Vundef end. -Inductive instr_state : Type := -| InstrState: - forall (rs: regset) - (m: mem), - instr_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. +|*) + +Record instr_state := mk_instr_state { + is_rs: regset; + is_ps: predset; + is_mem: mem; +}. + +(*| +Top-Level Type Definitions +========================== +|*) Section DEFINITION. @@ -346,7 +209,6 @@ Section DEFINITION. fn_params: list reg; fn_stacksize: Z; fn_code: code; - fn_funct_units: funct_units; fn_entrypoint: node }. @@ -366,7 +228,8 @@ Section DEFINITION. (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 *) + (rs: regset) (**r register state in calling function *) + (pr: predset), (**r predicate state of the calling function *) stackframe. Inductive state : Type := @@ -376,6 +239,7 @@ Section DEFINITION. (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: @@ -392,6 +256,11 @@ Section DEFINITION. End DEFINITION. +(*| +Semantics +========= +|*) + Section RELSEM. Context {bblock_body : Type}. @@ -411,67 +280,88 @@ Section RELSEM. end end. + Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop := + | eval_pred_true: + 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, + 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. + Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop := | exec_RBnop: - forall rs m sp, - step_instr sp (InstrState rs m) RBnop (InstrState rs m) + forall sp ist, + step_instr sp ist RBnop ist | exec_RBop: - forall op v res args rs m sp p, - eval_operation ge sp op rs##args m = Some v -> - step_instr sp (InstrState rs m) - (RBop p op args res) - (InstrState (rs#res <- v) m) + 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, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - step_instr sp (InstrState rs m) - (RBload p chunk addr args dst) - (InstrState (rs#dst <- v) m) + 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, - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a rs#src = Some m' -> - step_instr sp (InstrState rs m) - (RBstore p chunk addr args src) - (InstrState rs m'). + 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, + 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. 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', + 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 m) (RBcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m) + 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) | exec_RBtailcall: - forall s f stk rs m sig ros args fd m' pc, + 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 m) (RBtailcall sig ros args) + 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') | exec_RBbuiltin: - forall s f sp rs m ef args res pc' vargs t vres m' pc, + 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 m) (RBbuiltin ef args res pc') - t (State s f sp pc' (regmap_setres res vres rs) 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') | exec_RBcond: - forall s f sp rs m cond args ifso ifnot b pc pc', + 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 m) (RBcond cond args ifso ifnot) - E0 (State s f sp pc' rs m) + 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) | exec_RBjumptable: - forall s f sp rs m arg tbl n pc pc', + 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 m) (RBjumptable arg tbl) - E0 (State s f sp pc' rs m) - | exec_Ireturn: - forall s f stk rs m or pc m', + step_cf_instr (State s f sp pc rs pr m) (RBjumptable arg tbl) + E0 (State s f sp pc' rs pr m) + | exec_RBreturn: + 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 m) (RBreturn or) - E0 (Returnstate s (regmap_optget or Vundef rs) 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') + | 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) + | 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'. End RELSEM. |