diff options
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
| -rw-r--r-- | src/hls/RTLBlockInstr.v | 51 |
1 files changed, 25 insertions, 26 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index c1d74b5..8cd3468 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -183,36 +183,36 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | 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' _) => + | 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 _ p1' _), Some (exist _ p2' _) => 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) _) | Pnot (Pnot p') => match trans_pred n p' with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Pand p1 p2) => match trans_pred n (Por (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Por p1 p2) => match trans_pred n (Pand (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - - split; auto. destruct (a p') eqn:?; crush. + - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. crush. - rewrite negb_involutive in H. apply i in H. auto. @@ -239,9 +239,9 @@ Definition sat_pred (bound: nat) (p: pred_op) : + {forall a : asgn, sat_predicate p a = false}). refine ( match trans_pred bound p with - | Some (exist fm _) => + | Some (exist _ fm _) => match boundedSat bound fm with - | Some (inleft (exist a _)) => Some (inleft (exist _ a _)) + | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _)) | Some (inright _) => Some (inright _) | None => None end @@ -255,7 +255,7 @@ Qed. Definition sat_pred_simple (bound: nat) (p: pred_op) := match sat_pred bound p with - | Some (inleft (exist al _)) => Some (Some al) + | Some (inleft (exist _ al _)) => Some (Some al) | Some (inright _) => Some None | None => None end. @@ -347,12 +347,11 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | _, _ => Regmap.init Vundef end. -Inductive instr_state : Type := -| InstrState: - forall (rs: regset) - (pr: predset) - (m: mem), - instr_state. +Record instr_state := mk_instr_state { + instr_st_regset: regset; + instr_st_predset: predset; + instr_st_mem: mem; +}. Section DEFINITION. @@ -440,11 +439,11 @@ Section RELSEM. | 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 (Some p) (mk_instr_state 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 (Some p) (mk_instr_state rs pr m) i (mk_instr_state rs pr m) | eval_pred_none: forall i i', eval_pred None i i' i. @@ -456,25 +455,25 @@ Section RELSEM. | 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 (InstrState rs pr m) (InstrState (rs#res <- v) pr m) ist -> - step_instr sp (InstrState rs pr m) (RBop p op args res) ist + 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 (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 + 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 (InstrState rs pr m) (InstrState rs pr m') ist -> - step_instr sp (InstrState rs pr m) (RBstore p chunk addr args src) ist + 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, 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). + step_instr sp (mk_instr_state rs pr m) (RBsetpred c args p) + (mk_instr_state rs (PMap.set p b pr) m). Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: |