aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asmblockgen.v5
-rw-r--r--mppa_k1c/Asmblockgenproof.v75
-rw-r--r--mppa_k1c/Asmblockgenproof0.v15
-rw-r--r--mppa_k1c/Asmblockgenproof1.v59
4 files changed, 124 insertions, 30 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index f09e2a73..e16c701f 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -61,6 +61,7 @@ Definition make_immed64 (val: int64) := Imm64_single val.
Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativity).
Notation "a ::i b" := (cons (A:=basic) a b) (at level 49, right associativity).
Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associativity).
+Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity).
(** Smart constructors for arithmetic operations involving
a 32-bit or 64-bit integer constant. Depending on whether the
@@ -156,6 +157,10 @@ Definition transl_opt_compuimm
loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k)
.
+(* Definition transl_opt_compuimm
+ (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
+ loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k). *)
+
(* match select_comp n c with
| Some Ceq => Pcbu BTweqz r1 lbl ::g k
| Some Cne => Pcbu BTwnez r1 lbl ::g k
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 3344d1d2..237acc5e 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1088,6 +1088,52 @@ Proof.
intros. simpl. auto.
Qed.
+Lemma exec_straight_opt_body2:
+ forall c rs1 m1 c' rs2 m2,
+ exec_straight_opt tge c rs1 m1 c' rs2 m2 ->
+ exists body,
+ exec_body tge body rs1 m1 = Next rs2 m2
+ /\ (basics_to_code body) ++g c' = c.
+Proof.
+ intros until m2. intros EXES.
+ inv EXES.
+ - exists nil. split; auto.
+ - eapply exec_straight_body2. auto.
+Qed.
+
+Lemma extract_basics_to_code:
+ forall lb c,
+ extract_basic (basics_to_code lb ++ c) = lb ++ extract_basic c.
+Proof.
+ induction lb; intros; simpl; congruence.
+Qed.
+
+Lemma extract_ctl_basics_to_code:
+ forall lb c,
+ extract_ctl (basics_to_code lb ++ c) = extract_ctl c.
+Proof.
+ induction lb; intros; simpl; congruence.
+Qed.
+
+(* Lemma goto_label_inv:
+ forall fn tbb l rs m b ofs,
+ rs PC = Vptr b ofs ->
+ goto_label fn l rs m = goto_label fn l (nextblock tbb rs) m.
+Proof.
+ intros.
+ unfold goto_label. rewrite nextblock_pc. unfold Val.offset_ptr. rewrite H.
+ exploreInst; auto.
+ unfold nextblock. rewrite Pregmap.gss.
+
+Qed.
+
+
+Lemma exec_control_goto_label_inv:
+ exec_control tge fn (Some ctl) rs m = goto_label fn l rs m ->
+ exec_control tge fn (Some ctl) (nextblock tbb rs) m = goto_label fn l (nextblock tbb rs) m.
+Proof.
+Qed. *)
+
Theorem step_simu_control:
forall bb' fb fn s sp c ms' m' rs2 m2 E0 S'' rs1 m1 tbb tbdy2 tex cs2,
MB.body bb' = nil ->
@@ -1192,8 +1238,7 @@ Proof.
eauto with asmgen.
congruence.
+ (* MBcond *)
- destruct TODO.
- (* destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+ destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
inv TBC. inv TIC. inv H0.
* (* MBcond true *)
@@ -1202,12 +1247,30 @@ Proof.
eapply preg_vals; eauto.
all: eauto.
intros EC.
-
+ exploit transl_cbranch_correct_true; eauto. intros (rs' & jmp & A & B & C).
+ exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
+ assert (PCeq': rs2 PC = rs' PC). { inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. }
+ rewrite PCeq' in PCeq.
+ assert (f1 = f) by congruence. subst f1.
+ exploit find_label_goto_label.
+ 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs')). rewrite nextblock_pc.
+ unfold Val.offset_ptr. rewrite PCeq. eauto.
+ intros (tc' & rs3 & GOTOL & TLPC & Hrs3).
+ exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
+ assert (tf = fn) by congruence. subst tf.
repeat eexists.
- rewrite H6. simpl extract_basic. eauto.
- rewrite H7. simpl extract_ctl. simpl. reflexivity.
- *)
+ rewrite H6. rewrite <- BTC. rewrite extract_basics_to_code. simpl. rewrite app_nil_r. eauto.
+ rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto.
+
+ econstructor; eauto.
+ eapply agree_exten with rs2; eauto with asmgen.
+ { intros. destruct r; try destruct g; try discriminate.
+ all: rewrite Hrs3; try discriminate; unfold nextblock; Simpl. }
+ intros. discriminate.
+
+ * destruct TODO.
+
+ (* MBjumptable *)
destruct TODO.
+ (* MBreturn *)
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index 3db0c2cd..6a71a746 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -815,6 +815,21 @@ Proof.
rewrite <- H7. simpl. rewrite H1. auto.
Qed.
+Lemma exec_straight_body2:
+ forall c rs1 m1 c' rs2 m2,
+ exec_straight c rs1 m1 c' rs2 m2 ->
+ exists body,
+ exec_body ge body rs1 m1 = Next rs2 m2
+ /\ (basics_to_code body) ++g c' = c.
+Proof.
+ intros until m2. induction 1.
+ - exists (i1::nil). split; auto. simpl. rewrite H. auto.
+ - destruct IHexec_straight as (bdy & EXEB & BTC).
+ exists (i:: bdy). split; simpl.
+ + rewrite H. auto.
+ + congruence.
+Qed.
+
(* Lemma exec_straight_body2:
forall c c' l rs1 m1 rs2 m2,
exec_straight (c++c') rs1 m1 c' rs2 m2 ->
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index c0b0fb03..7bc60a65 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -75,7 +75,7 @@ Proof.
auto.
Qed.
-(*
+
(** Properties of registers *)
@@ -93,7 +93,7 @@ Qed.
Hint Resolve ireg_of_not_GPR31 ireg_of_not_GPR31': asmgen.
-*)
+
(** Useful simplification tactic *)
Ltac Simplif :=
@@ -589,7 +589,7 @@ Proof.
- (* c = Cge *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero);
destruct cmp; discriminate.
Qed.
-(*
+
Lemma transl_cbranch_correct_1:
forall cond args lbl k c m ms b sp rs m',
transl_cbranch cond args lbl k = OK c ->
@@ -652,7 +652,12 @@ Proof.
split.
* apply A.
* split; auto. apply C. apply EVAL'.
- + unfold transl_opt_compuimm. rewrite <- Heqselcomp; simpl.
+ + assert (transl_opt_compuimm n c0 x lbl k = loadimm32 GPR31 n ::g transl_comp c0 Unsigned x GPR31 lbl k).
+ { unfold transl_opt_compuimm.
+ destruct (Int.eq n Int.zero) eqn:EQN.
+ all: unfold select_comp in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto.
+ all: discriminate. }
+ rewrite H. clear H.
exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
exploit (transl_compu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
exists rs'2, (Pcb BTwnez GPR31 lbl).
@@ -661,7 +666,7 @@ Proof.
with (c2 := (transl_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
eexact A. eexact A'.
* split; auto.
- { apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen. }
+ { apply C'; auto. rewrite B, C; eauto with asmgen. }
{ intros. rewrite B'; eauto with asmgen. }
(* Ccompl *)
- exploit (transl_compl_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
@@ -688,7 +693,7 @@ Proof.
* constructor.
* split; auto.
destruct c0; simpl; auto;
- unfold eval_branch; rewrite <- H; unfold getl; rewrite EVAL'; auto.
+ unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
+ exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
exploit (transl_compl_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
exists rs'2, (Pcb BTwnez GPR31 lbl).
@@ -697,7 +702,7 @@ Proof.
with (c2 := (transl_compl c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
eexact A. eexact A'.
* split; auto.
- { apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen. }
+ { apply C'; auto. rewrite B, C; eauto with asmgen. }
{ intros. rewrite B'; eauto with asmgen. }
(* Ccompluimm *)
@@ -709,7 +714,12 @@ Proof.
split.
* apply A.
* split; auto. apply C. apply EVAL'.
- + unfold transl_opt_compluimm. rewrite <- Heqselcomp; simpl.
+ + assert (transl_opt_compluimm n c0 x lbl k = loadimm64 GPR31 n ::g transl_compl c0 Unsigned x GPR31 lbl k).
+ { unfold transl_opt_compluimm.
+ destruct (Int64.eq n Int64.zero) eqn:EQN.
+ all: unfold select_compl in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto.
+ all: discriminate. }
+ rewrite H. clear H.
exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
exploit (transl_complu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
exists rs'2, (Pcb BTwnez GPR31 lbl).
@@ -718,23 +728,23 @@ Proof.
with (c2 := (transl_compl c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
eexact A. eexact A'.
* split; auto.
- { apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen. }
+ { apply C'; auto. rewrite B, C; eauto with asmgen. }
{ intros. rewrite B'; eauto with asmgen. }
Qed.
- *)
-(* Lemma transl_cbranch_correct_true:
- forall cond args lbl k c m ms sp rs m',
+
+Lemma transl_cbranch_correct_true:
+ forall cond args lbl k c m ms sp rs m' tbb,
transl_cbranch cond args lbl k = OK c ->
eval_condition cond (List.map ms args) m = Some true ->
agree ms sp rs ->
Mem.extends m m' ->
exists rs', exists insn,
- exec_straight_opt c rs m' (insn :: k) rs' m'
- /\ exec_instr ge fn insn rs' m' = goto_label fn lbl rs' m'
+ exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
+ /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = goto_label fn lbl (nextblock tbb rs') m'
/\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
-Proof.
- intros. eapply transl_cbranch_correct_1 with (b := true); eauto.
-Qed.
+Proof. Admitted.
+(* intros. eapply transl_cbranch_correct_1 with (b := true); eauto.
+Qed. *)
Lemma transl_cbranch_correct_false:
forall cond args lbl k c m ms sp rs m',
@@ -742,17 +752,18 @@ Lemma transl_cbranch_correct_false:
eval_condition cond (List.map ms args) m = Some false ->
agree ms sp rs ->
Mem.extends m m' ->
- exists rs',
- exec_straight ge fn c rs m' k rs' m'
+ exists rs', exists insn,
+ exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
+ /\ exec_control ge fn (Some insn) rs' m' = Next rs' m'
/\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
Proof.
- intros. exploit transl_cbranch_correct_1; eauto. simpl.
- intros (rs' & insn & A & B & C).
- exists (nextinstr rs').
+ intros. exploit transl_cbranch_correct_1; eauto.
+(* intros (rs' & insn & A & B & C).
+ exists rs'.
split. eapply exec_straight_opt_right; eauto. apply exec_straight_one; auto.
intros; Simpl.
-Qed.
- *)
+ *)Qed.
+
(*
(** Translation of condition operators *)
generated by cgit (git 2.34.1) at 2024-07-14 16:52:11 +0000