aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asmblock.v4
-rw-r--r--mppa_k1c/Asmblockdeps.v40
-rw-r--r--mppa_k1c/Asmblockgenproof1.v6
3 files changed, 25 insertions, 25 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 9938b386..621ed8a7 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -1390,8 +1390,8 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem)
end
| Pcbu bt r l =>
match cmpu_for_btest bt with
- | (Some c, Int) => eval_branch f l rs m (Val.cmpu_bool (Mem.valid_pointer m) c rs#r (Vint (Int.repr 0)))
- | (Some c, Long) => eval_branch f l rs m (Val.cmplu_bool (Mem.valid_pointer m) c rs#r (Vlong (Int64.repr 0)))
+ | (Some c, Int) => eval_branch f l rs m (Val_cmpu_bool c rs#r (Vint (Int.repr 0)))
+ | (Some c, Long) => eval_branch f l rs m (Val_cmplu_bool c rs#r (Vlong (Int64.repr 0)))
| (None, _) => Stuck
end
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 616c5f2a..c6052337 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -179,10 +179,10 @@ Definition control_eval (o: control_op) (l: list value) :=
| (Some c, Long) => eval_branch_deps fn l vpc (Val.cmpl_bool c v (Vlong (Int64.repr 0)))
| (None, _) => None
end
- | Ocbu bt l, [Val v; Val vpc; Memstate m] =>
+ | Ocbu bt l, [Val v; Val vpc] =>
match cmpu_for_btest bt with
- | (Some c, Int) => eval_branch_deps fn l vpc (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint (Int.repr 0)))
- | (Some c, Long) => eval_branch_deps fn l vpc (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong (Int64.repr 0)))
+ | (Some c, Int) => eval_branch_deps fn l vpc (Val_cmpu_bool c v (Vint (Int.repr 0)))
+ | (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0)))
| (None, _) => None
end
| OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz)))
@@ -503,7 +503,7 @@ Definition trans_control (ctl: control) : macro :=
| Pigoto r => [(#PC, Name (#r))]
| Pj_l l => [(#PC, Op (Control (Oj_l l)) (Name (#PC) @ Enil))]
| Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (Name (#r) @ Name (#PC) @ Enil))]
- | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Name pmem @ Enil))]
+ | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Enil))]
| Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
end.
@@ -844,34 +844,34 @@ Proof.
* intros rr; destruct rr; Simpl.
(* Pcbu *)
+ destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i.
- ++ unfold eval_branch in H0. destruct (Val.cmpu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b0.
+ ++ unfold eval_branch in H0. destruct (Val_cmpu_bool _ _) eqn:VALCMP; try discriminate. destruct b0.
+++ unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock b rs PC) eqn:NB; try discriminate.
inv H0. eexists; split; try split.
* simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl.
- rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0.
+ rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0.
unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
unfold goto_label_deps. rewrite LPOS. rewrite nextblock_pc in NB. rewrite NB. reflexivity.
* Simpl.
* intros rr; destruct rr; Simpl.
+++ inv H0. eexists; split; try split.
* simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl.
- rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0.
+ rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0.
unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
reflexivity.
* Simpl.
* intros rr; destruct rr; Simpl.
- ++ unfold eval_branch in H0. destruct (Val.cmplu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b0.
+ ++ unfold eval_branch in H0. destruct (Val_cmplu_bool _ _) eqn:VALCMP; try discriminate. destruct b0.
+++ unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock b rs PC) eqn:NB; try discriminate.
inv H0. eexists; split; try split.
* simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl.
- rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0.
+ rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0.
unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
unfold goto_label_deps. rewrite LPOS. rewrite nextblock_pc in NB. rewrite NB. reflexivity.
* Simpl.
* intros rr; destruct rr; Simpl.
+++ inv H0. eexists; split; try split.
* simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl.
- rewrite CFB. Simpl. rewrite H2. pose (H3 r). simpl in e0. rewrite e0.
+ rewrite CFB. Simpl. pose (H3 r). simpl in e0. rewrite e0.
unfold eval_branch_deps. unfold nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
reflexivity.
* Simpl.
@@ -1013,17 +1013,17 @@ Proof.
(* Pcbu *)
- simpl in *. destruct (cmpu_for_btest bt). destruct i.
+ pose (H3 PC); simpl in e; rewrite e in H1; clear e.
- destruct o; auto. rewrite H2 in H1.
+ destruct o; auto.
pose (H3 r); simpl in e; rewrite e in H1; clear e.
unfold eval_branch_deps in H1; unfold eval_branch.
- destruct (Val.cmpu_bool _ _ _ _); auto. destruct b; try discriminate.
+ destruct (Val_cmpu_bool _ _ _); auto. destruct b; try discriminate.
unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
destruct (rs PC); auto. discriminate.
+ pose (H3 PC); simpl in e; rewrite e in H1; clear e.
- destruct o; auto. rewrite H2 in H1.
+ destruct o; auto.
pose (H3 r); simpl in e; rewrite e in H1; clear e.
unfold eval_branch_deps in H1; unfold eval_branch.
- destruct (Val.cmplu_bool _ _ _); auto. destruct b; try discriminate.
+ destruct (Val_cmplu_bool _ _); auto. destruct b; try discriminate.
unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
destruct (rs PC); auto. discriminate.
Qed.
@@ -1123,17 +1123,17 @@ Proof.
(* Pcbu *)
- simpl in *. destruct (cmpu_for_btest bt). destruct i.
-- destruct o.
- + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps.
- pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpu_bool _ _ _); auto.
+ + unfold eval_branch in H0; unfold eval_branch_deps.
+ pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmpu_bool _ _); auto.
destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
- + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
+ + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
-- destruct o.
- + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps.
- pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmplu_bool _ _ _); auto.
+ + unfold eval_branch in H0; unfold eval_branch_deps.
+ pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmplu_bool _ _); auto.
destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
- + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
+ + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
Qed.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 1a55f58e..5486a497 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -743,7 +743,7 @@ Lemma transl_opt_compuimm_correct:
exists rs', exists insn,
exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
- /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs#r1 (Vint n) = Some b ->
+ /\ ( Val_cmpu_bool cmp rs#r1 (Vint n) = Some b ->
exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
@@ -819,7 +819,7 @@ Lemma transl_opt_compluimm_correct:
exists rs', exists insn,
exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
- /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 (Vlong n) = Some b ->
+ /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b ->
exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
@@ -1016,7 +1016,7 @@ Proof.
exists rs', i.
split.
* apply A.
- * split; auto. apply C. apply EVAL'.
+ * split; eauto. (* apply C. apply EVAL'. *)
+ assert (transl_opt_compluimm n c0 x lbl k = loadimm64 RTMP n ::g transl_compl c0 Unsigned x RTMP lbl k).
{ unfold transl_opt_compluimm.
destruct (Int64.eq n Int64.zero) eqn:EQN.
generated by cgit (git 2.34.1) at 2024-06-11 23:03:37 +0000