diff options
Diffstat (limited to 'mppa_k1c/lib/RTLpathLiveproofs.v')
| -rw-r--r-- | mppa_k1c/lib/RTLpathLiveproofs.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/mppa_k1c/lib/RTLpathLiveproofs.v b/mppa_k1c/lib/RTLpathLiveproofs.v index a807279b..8e2c22cd 100644 --- a/mppa_k1c/lib/RTLpathLiveproofs.v +++ b/mppa_k1c/lib/RTLpathLiveproofs.v @@ -98,10 +98,10 @@ Proof. Qed. Record eqlive_istate alive (st1 st2: istate): Prop := - { eqlive_continue: continue st1 = continue st2; - eqlive_the_pc: the_pc st1 = the_pc st2; - eqlive_the_rs: eqlive_reg alive (the_rs st1) (the_rs st2); - eqlive_the_mem: (the_mem st1) = (the_mem st2) }. + { eqlive_continue: icontinue st1 = icontinue st2; + eqlive_ipc: ipc st1 = ipc st2; + eqlive_irs: eqlive_reg alive (irs st1) (irs st2); + eqlive_imem: (imem st1) = (imem st2) }. Lemma iinst_checker_eqlive ge sp pm alive i res rs1 rs2 m st1: eqlive_reg (ext alive) rs1 rs2 -> @@ -174,8 +174,8 @@ Qed. Lemma iinst_checker_istep_continue ge sp pm alive i res rs m st: iinst_checker pm alive i = Some res -> istep ge i sp rs m = Some st -> - continue st = true -> - (snd res)=(the_pc st). + icontinue st = true -> + (snd res)=(ipc st). Proof. intros; exploit iinst_checker_default_succ; eauto. erewrite istep_normal_exit; eauto. @@ -199,8 +199,8 @@ Lemma iinst_checker_eqlive_stopped ge sp pm alive i res rs1 rs2 m st1: eqlive_reg (ext alive) rs1 rs2 -> istep ge i sp rs1 m = Some st1 -> iinst_checker pm alive i = Some res -> - continue st1 = false -> - exists path st2, pm!(the_pc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. + icontinue st1 = false -> + exists path st2, pm!(ipc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. Proof. intros EQLIVE. set (tmp := istep ge i sp rs2). @@ -220,7 +220,7 @@ Lemma ipath_checker_eqlive_normal ge ps (f:function) sp pm: forall alive pc res eqlive_reg (ext alive) rs1 rs2 -> ipath_checker ps f pm alive pc = Some res -> isteps ge ps f sp rs1 m pc = Some st1 -> - continue st1 = true -> + icontinue st1 = true -> exists st2, isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2. Proof. induction ps as [|ps]; simpl; try_simplify_someHyps. @@ -233,7 +233,7 @@ Proof. destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]). try_simplify_someHyps. rewrite <- CONT, <- MEM, <- PC. - destruct (continue st0) eqn:CONT'. + destruct (icontinue st0) eqn:CONT'. * intros; exploit iinst_checker_istep_continue; eauto. rewrite <- PC; intros X; rewrite X in * |-. eauto. * try_simplify_someHyps. @@ -243,14 +243,14 @@ Qed. Lemma ipath_checker_isteps_continue ge ps (f:function) sp pm: forall alive pc res rs m st, ipath_checker ps f pm alive pc = Some res -> isteps ge ps f sp rs m pc = Some st -> - continue st = true -> - (snd res)=(the_pc st). + icontinue st = true -> + (snd res)=(ipc st). Proof. induction ps as [|ps]; simpl; try_simplify_someHyps. inversion_SOME i; try_simplify_someHyps. inversion_SOME res0. inversion_SOME st0. - destruct (continue st0) eqn:CONT'. + destruct (icontinue st0) eqn:CONT'. - intros; exploit iinst_checker_istep_continue; eauto. intros EQ; rewrite EQ in * |-; clear EQ; eauto. - try_simplify_someHyps; congruence. @@ -260,15 +260,15 @@ Lemma ipath_checker_eqlive_stopped ge ps (f:function) sp pm: forall alive pc res eqlive_reg (ext alive) rs1 rs2 -> ipath_checker ps f pm alive pc = Some res -> isteps ge ps f sp rs1 m pc = Some st1 -> - continue st1 = false -> - exists path st2, pm!(the_pc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. + icontinue st1 = false -> + exists path st2, pm!(ipc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2. Proof. induction ps as [|ps]; simpl; try_simplify_someHyps; try congruence. inversion_SOME i; try_simplify_someHyps. inversion_SOME res0. inversion_SOME st0. intros. - destruct (continue st0) eqn:CONT'; try_simplify_someHyps; intros. + destruct (icontinue st0) eqn:CONT'; try_simplify_someHyps; intros. * intros; exploit iinst_checker_eqlive; eauto. destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]). exploit iinst_checker_istep_continue; eauto. @@ -452,7 +452,7 @@ Proof. intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto. inversion_SOME res. intros. - destruct (continue st1) eqn: CONT. + destruct (icontinue st1) eqn: CONT. - (* CONT => true *) exploit iinst_checker_eqlive; eauto. destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]). |