From cb82a024b748ccaa7d607741a21b3eb6e0e347ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 26 May 2021 19:24:46 +0100 Subject: Change naturals to positive in predicates --- src/hls/HTLPargen.v | 2 +- src/hls/RTLBlockInstr.v | 122 +++++++++++++++++++++++++++++++----------------- 2 files changed, 79 insertions(+), 45 deletions(-) (limited to 'src/hls') diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 7ce6c7a..9746f92 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -659,7 +659,7 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with | Pvar pred => - Vrange preg (Vlit (natToValue pred)) (Vlit (natToValue pred)) + Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) | Pnot pred => Vunop Vnot (pred_expr preg pred) | Pand p1 p2 => diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 86f8eba..ecd644b 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -34,7 +34,7 @@ Require Import vericert.hls.Sat. Local Open Scope rtl. Definition node := positive. -Definition predicate := nat. +Definition predicate := positive. Inductive pred_op : Type := | Pvar: predicate -> pred_op @@ -44,7 +44,7 @@ Inductive pred_op : Type := Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool := match p with - | Pvar p' => a p' + | Pvar p' => a (Pos.to_nat 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 @@ -152,7 +152,7 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := | O => None | S n => match p with - | Pvar p' => Some (((true, p') :: nil) :: nil) + | Pvar p' => Some (((true, Pos.to_nat p') :: nil) :: nil) | Pand p1 p2 => match trans_pred_temp n p1, trans_pred_temp n p2 with | Some p1', Some p2' => @@ -165,7 +165,7 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := Some (mult p1' p2') | _, _ => None end - | Pnot (Pvar p') => Some (((false, p') :: nil) :: nil) + | Pnot (Pvar p') => Some (((false, Pos.to_nat 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)) @@ -180,7 +180,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | O => None | S n => match p with - | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _) + | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _) | Pand p1 p2 => match trans_pred n p1, trans_pred n p2 with | Some (exist p1' _), Some (exist p2' _) => @@ -193,7 +193,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) | _ => None end end); split; intros; simpl in *; auto. @@ -310,6 +310,15 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := end. Definition regset := Regmap.t val. +Definition predset := PMap.t bool. + +Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} := + match p with + | Pvar p' => PMap.get p' pr + | Pnot p' => negb (eval_predf pr p') + | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'') + | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'') + end. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with @@ -320,6 +329,7 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := Inductive instr_state : Type := | InstrState: forall (rs: regset) + (pr: predset) (m: mem), instr_state. @@ -358,7 +368,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 := @@ -368,6 +379,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: @@ -403,67 +415,89 @@ Section RELSEM. end end. + Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop := + | eval_pred_true: + forall (pr: predset) p rs pr m i, + eval_predf pr p = true -> + eval_pred (Some p) (InstrState rs pr m) i i + | eval_pred_false: + forall (pr: predset) p rs pr m i, + eval_predf pr p = false -> + eval_pred (Some p) (InstrState rs pr m) i (InstrState rs pr m) + | 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 (InstrState rs pr m) (InstrState (rs#res <- v) pr m) ist -> + step_instr sp (InstrState 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 (InstrState rs pr m) (InstrState (rs#dst <- v) pr m) ist -> + step_instr sp (InstrState 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 (InstrState rs pr m) (InstrState rs pr m') ist -> + step_instr sp (InstrState rs pr m) (RBstore p chunk addr args src) ist + | exec_RBsetpred: + forall sp rs pr m p c b args, + Op.eval_condition c rs##args m = Some b -> + step_instr sp (InstrState rs pr m) (RBsetpred c args p) + (InstrState rs (PMap.set p b pr) m). 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. -- cgit