aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asmblockgen.v2
-rw-r--r--mppa_k1c/Asmblockgenproof1.v16
-rw-r--r--mppa_k1c/Op.v4
-rw-r--r--mppa_k1c/SelectLong.vp25
-rw-r--r--mppa_k1c/SelectLongproof.v160
-rw-r--r--mppa_k1c/ValueAOp.v12
6 files changed, 205 insertions, 14 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 6e025381..cf0b2a0a 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -741,7 +741,7 @@ Definition transl_op
do r0 <- ireg_of a0;
do r1 <- ireg_of a1;
do rS <- ireg_of aS;
- OK (Pcmove BTwnez r0 rS r1 ::i k)
+ OK (Pcmove BTdnez r0 rS r1 ::i k)
| _, _ =>
Error(msg "Asmgenblock.transl_op")
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index a1bd7124..16663522 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1568,6 +1568,16 @@ Proof.
destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence.
Qed.
+Lemma int64_eq_comm:
+ forall (x y: int64),
+ (Int64.eq x y) = (Int64.eq y x).
+Proof.
+ intros.
+ unfold Int64.eq.
+ unfold zeq.
+ destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence.
+Qed.
+
Lemma transl_op_correct:
forall op args res k (rs: regset) m v c,
transl_op op args res k = OK c ->
@@ -1674,13 +1684,13 @@ Opaque Int.eq.
+ eapply exec_straight_one.
simpl; reflexivity.
+ split.
- * unfold select.
+ * unfold selectl.
destruct (rs x1) eqn:eqX1; try constructor.
destruct (rs x) eqn:eqX; try constructor.
destruct (rs x0) eqn:eqX0; try constructor.
simpl.
- rewrite int_eq_comm.
- destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor.
+ rewrite int64_eq_comm.
+ destruct (Int64.eq i Int64.zero); simpl; rewrite Pregmap.gss; constructor.
* intros.
rewrite Pregmap.gso; congruence.
Qed.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 39a599d8..ec3f1077 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -271,12 +271,12 @@ Definition select (v0 : val) (v1 : val) (vselect : val) : val :=
Definition selectl (v0 : val) (v1 : val) (vselect : val) : val :=
match vselect with
- | Vint iselect =>
+ | Vlong iselect =>
match v0 with
| Vlong i0 =>
match v1 with
| Vlong i1 =>
- Vlong (if Int.cmp Ceq Int.zero iselect
+ Vlong (if Int64.cmp Ceq Int64.zero iselect
then i0
else i1)
| _ => Vundef
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 0c3618d7..26ae55f6 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -278,9 +278,34 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
| t1, Eop (Olongconst n2) Enil => orlimm n2 t1
| (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil)
| t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil)
+ | (Eop Oandl ((Eop Ocast32signed
+ ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0))
+ (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)),
+ (Eop Oandl ((Eop Ocast32signed
+ ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1))
+ (y1:::Enil)):::Enil)):::Enil)):::v1:::Enil)) =>
+ if same_expr_pure y0 y1
+ && Int64.eq zero0 Int64.zero
+ && Int64.eq zero1 Int64.zero
+ then Eop Oselectl (v0:::v1:::y0:::Enil)
+ else Eop Oorl (e1:::e2:::Enil)
+
| _, _ => Eop Oorl (e1:::e2:::Enil)
end.
+(*
+ | (Eop Oandl ((Eop Ocast32signed
+ ((Eop Oneg ((Eop (Ocmp (Ccompluimm Ceq zero0))
+ (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)),
+ (Eop Oandl ((Eop Ocast32signed
+ ((Eop Oneg ((Eop (Ocmp (Ccompluimm Cne zero1))
+ (y1:::Enil)):::Enil)):::Enil)):::v1:::Enil)) =>
+ if same_expr_pure y0 y1
+ && Int64.eq zero0 Int64.zero
+ && Int64.eq zero1 Int64.zero
+ then Eop Oselectl (v0:::v1:::y0:::Enil)
+ else Eop Oorl (e1:::e2:::Enil) *)
+
Nondetfunction xorlimm (n1: int64) (e2: expr) :=
if Int64.eq n1 Int64.zero then e2 else
match e2 with
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 79187338..09a7cfff 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -414,6 +414,16 @@ Proof.
- TrivialExists.
Qed.
+
+Lemma int64_eq_commut: forall x y : int64,
+ (Int64.eq x y) = (Int64.eq y x).
+Proof.
+ intros.
+ predSpec Int64.eq Int64.eq_spec x y;
+ predSpec Int64.eq Int64.eq_spec y x;
+ congruence.
+Qed.
+
Theorem eval_orl: binary_constructor_sound orl Val.orl.
Proof.
unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl.
@@ -423,6 +433,156 @@ Proof.
- InvEval. apply eval_orlimm; auto.
- (*orn*) InvEval. TrivialExists; simpl; congruence.
- (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence.
+ - (* selectl *)
+ destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists.
+ predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists.
+ predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; [ | TrivialExists].
+ inv H.
+ inv H0.
+ inv H6.
+ inv H3.
+ inv H2.
+ inv H7.
+ inv H4.
+ inv H3.
+ inv H6.
+ inv H4.
+ inv H3.
+ inv H14.
+ inv H13.
+ inv H6.
+ inv H4.
+ inv H13.
+ inv H14.
+ inv H9.
+ inv H11.
+ inv H13.
+ inv H3.
+ inv H6.
+ inv H7.
+ inv H3.
+ inv H14.
+ inv H17.
+ simpl in *.
+ inv H8.
+ inv H5.
+ inv H10.
+ inv H12.
+ inv H15.
+ inv H16.
+ inv H11.
+ inv H13.
+ unfold same_expr_pure in PURE.
+ destruct y0; try congruence.
+ destruct y1; try congruence.
+ destruct (ident_eq i i0); try congruence; clear PURE.
+ rewrite <- e0 in *; clear e0.
+ inv H6.
+ inv H7.
+ rename v10 into vtest.
+ replace v11 with vtest in * by congruence.
+ TrivialExists.
+ simpl.
+ f_equal.
+ unfold selectl.
+ destruct vtest; simpl; trivial.
+ rewrite Val.andl_commut.
+ destruct v4; simpl; trivial.
+ rewrite Val.andl_commut.
+ rewrite Val.orl_commut.
+ destruct v9; simpl; trivial.
+ rewrite int64_eq_commut.
+ destruct (Int64.eq i1 Int64.zero); simpl.
+
+ + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+ replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+ rewrite Int64.and_mone.
+ rewrite Int64.and_zero.
+ rewrite Int64.or_commut.
+ rewrite Int64.or_zero.
+ reflexivity.
+ + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+ replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+ rewrite Int64.and_mone.
+ rewrite Int64.and_zero.
+ rewrite Int64.or_zero.
+ reflexivity.
+ (*
+ - (* selectl unsigned *)
+ destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists.
+ predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists.
+ predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; [ | TrivialExists].
+ inv H.
+ inv H0.
+ inv H6.
+ inv H3.
+ inv H2.
+ inv H7.
+ inv H4.
+ inv H3.
+ inv H6.
+ inv H4.
+ inv H3.
+ inv H14.
+ inv H13.
+ inv H6.
+ inv H4.
+ inv H13.
+ inv H14.
+ inv H9.
+ inv H11.
+ inv H13.
+ inv H3.
+ inv H6.
+ inv H7.
+ inv H3.
+ inv H14.
+ inv H17.
+ simpl in *.
+ inv H8.
+ inv H5.
+ inv H10.
+ inv H12.
+ inv H15.
+ inv H16.
+ inv H11.
+ inv H13.
+ unfold same_expr_pure in PURE.
+ destruct y0; try congruence.
+ destruct y1; try congruence.
+ destruct (ident_eq i i0); try congruence; clear PURE.
+ rewrite <- e0 in *; clear e0.
+ inv H6.
+ inv H7.
+ rename v10 into vtest.
+ replace v11 with vtest in * by congruence.
+ TrivialExists.
+ simpl.
+ f_equal.
+ unfold selectl.
+ destruct vtest; simpl; trivial.
+ rewrite Val.andl_commut.
+ destruct v4; simpl; trivial.
+ rewrite Val.andl_commut.
+ rewrite Val.orl_commut.
+ destruct v9; simpl; trivial.
+ rewrite int64_eq_commut.
+ destruct (Int64.eq i1 Int64.zero); simpl.
+
+ + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+ replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+ rewrite Int64.and_mone.
+ rewrite Int64.and_zero.
+ rewrite Int64.or_commut.
+ rewrite Int64.or_zero.
+ reflexivity.
+ + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+ replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+ rewrite Int64.and_mone.
+ rewrite Int64.and_zero.
+ rewrite Int64.or_zero.
+ reflexivity.
+ + *)
- TrivialExists.
Qed.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index f181c0ea..a3843301 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -52,8 +52,8 @@ Definition select (v0 v1 vselect : aval) : aval :=
Definition selectl (v0 v1 vselect : aval) : aval :=
match vselect with
- | I iselect =>
- if Int.eq Int.zero iselect
+ | L iselect =>
+ if Int64.eq Int64.zero iselect
then binop_long (fun x0 x1 => x0) v0 v1
else binop_long (fun x0 x1 => x1) v0 v1
| _ => Vtop
@@ -272,12 +272,8 @@ Proof.
destruct a1; destruct a0; eauto; constructor.
(* selectl *)
- inv H2; simpl; try constructor.
- + destruct (Int.eq _ _); apply binop_long_sound; trivial.
- + destruct (Int.eq _ _);
- destruct a1; destruct a0; eauto; constructor.
- + destruct (Int.eq _ _);
- destruct a1; destruct a0; eauto; constructor.
- + destruct (Int.eq _ _);
+ + destruct (Int64.eq _ _); apply binop_long_sound; trivial.
+ + destruct (Int64.eq _ _);
destruct a1; destruct a0; eauto; constructor.
Qed.
generated by cgit (git 2.34.1) at 2024-07-14 12:58:42 +0000