Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit df9aab80 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

a more general way to manage special registers before introducing SP

parent 83b556a1
......@@ -205,20 +205,13 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
| Cge => (Pfles rd fs2 fs1, true)
end.
Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) :=
match optR0 with
| None => sem r1 r2 lbl
| Some true => sem X0 r1 lbl
| Some false => sem r1 X0 lbl
Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) :=
match optR with
| None => (r1, r2)
| Some X0_L => (X0, r1)
| Some X0_R => (r1, X0)
end.
Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) :=
match optR0 with
| None => sem r1 r2
| Some true => sem X0 r1
| Some false => sem r1 X0
end.
Definition get_opimmR0 (rd: ireg) (opi: opimm) :=
match opi with
| OPimmADD i => Paddiw rd X0 i
......@@ -281,54 +274,70 @@ Definition transl_cbranch
let (insn, normal) := transl_cond_single c X31 r1 r2 in
OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
| CEbeqw optR0, a1 :: a2 :: nil =>
| CEbeqw optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k)
| CEbnew optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbeqw r1' r2' lbl :: k)
| CEbnew optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k)
| CEbequw optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbnew r1' r2' lbl :: k)
| CEbequw optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k)
| CEbneuw optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbeqw r1' r2' lbl :: k)
| CEbneuw optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k)
| CEbltw optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbnew r1' r2' lbl :: k)
| CEbltw optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbltw r1 r2 lbl :: k)
| CEbltuw optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbltw r1' r2' lbl :: k)
| CEbltuw optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbltuw r1 r2 lbl :: k)
| CEbgew optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbltuw r1' r2' lbl :: k)
| CEbgew optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbgew r1 r2 lbl :: k)
| CEbgeuw optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbgew r1' r2' lbl :: k)
| CEbgeuw optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbgeuw r1 r2 lbl :: k)
| CEbeql optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbgeuw r1' r2' lbl :: k)
| CEbeql optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k)
| CEbnel optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbeql r1' r2' lbl :: k)
| CEbnel optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k)
| CEbequl optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbnel r1' r2' lbl :: k)
| CEbequl optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k)
| CEbneul optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbeql r1' r2' lbl :: k)
| CEbneul optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k)
| CEbltl optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbnel r1' r2' lbl :: k)
| CEbltl optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbltl r1 r2 lbl :: k)
| CEbltul optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbltl r1' r2' lbl :: k)
| CEbltul optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbltul r1 r2 lbl :: k)
| CEbgel optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbltul r1' r2' lbl :: k)
| CEbgel optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbgel r1 r2 lbl :: k)
| CEbgeul optR0, a1 :: a2 :: nil =>
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbgel r1' r2' lbl :: k)
| CEbgeul optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (apply_bin_r0_r0r0lbl optR0 Pbgeul r1 r2 lbl :: k)
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
OK (Pbgeul r1' r2' lbl :: k)
| _, _ =>
Error(msg "Asmgen.transl_cond_branch")
end.
......@@ -779,36 +788,42 @@ Definition transl_op
| OEimmR0 opi, nil =>
do rd <- ireg_of res;
OK (get_opimmR0 rd opi :: k)
| OEseqw optR0, a1 :: a2 :: nil =>
| OEseqw optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Pseqw rd) rs1 rs2 :: k)
| OEsnew optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Pseqw rd rs1' rs2' :: k)
| OEsnew optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k)
| OEsequw optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psnew rd rs1' rs2' :: k)
| OEsequw optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Pseqw rd) rs1 rs2 :: k)
| OEsneuw optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Pseqw rd rs1' rs2' :: k)
| OEsneuw optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k)
| OEsltw optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psnew rd rs1' rs2' :: k)
| OEsltw optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psltw rd) rs1 rs2 :: k)
| OEsltuw optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psltw rd rs1' rs2' :: k)
| OEsltuw optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psltuw rd) rs1 rs2 :: k)
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psltuw rd rs1' rs2' :: k)
| OEsltiw n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
......@@ -836,36 +851,42 @@ Definition transl_op
do rd <- ireg_of res;
do rs <- ireg_of a1;
OK (Poriw rd rs n :: k)
| OEseql optR0, a1 :: a2 :: nil =>
| OEseql optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Pseql rd) rs1 rs2 :: k)
| OEsnel optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Pseql rd rs1' rs2' :: k)
| OEsnel optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k)
| OEsequl optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psnel rd rs1' rs2' :: k)
| OEsequl optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Pseql rd) rs1 rs2 :: k)
| OEsneul optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Pseql rd rs1' rs2' :: k)
| OEsneul optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k)
| OEsltl optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psnel rd rs1' rs2' :: k)
| OEsltl optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psltl rd) rs1 rs2 :: k)
| OEsltul optR0, a1 :: a2 :: nil =>
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psltl rd rs1' rs2' :: k)
| OEsltul optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
do rs2 <- ireg_of a2;
OK (apply_bin_r0_r0r0 optR0 (Psltul rd) rs1 rs2 :: k)
let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in
OK (Psltul rd rs1' rs2' :: k)
| OEsltil n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
......
......@@ -212,22 +212,22 @@ Proof.
- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto.
destruct normal; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
Qed.
Remark transl_cond_op_label:
......@@ -309,18 +309,18 @@ Opaque Int.eq.
- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
- eapply transl_cond_op_label; eauto.
- destruct opi; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
Qed.
Remark indexed_memory_access_label:
......
......@@ -494,124 +494,128 @@ Proof.
split. rewrite V; destruct normal, b; reflexivity.
intros; Simpl.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *;
eexists; eexists; eauto; split; constructor; auto;
destruct (rs x) eqn:EQRS; simpl in *; try congruence;
inv EQ2; eexists; eexists; eauto; split; constructor; auto;
simpl in *.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: (Int.eq Int.zero i) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: (Int.eq i Int.zero) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
rewrite <- HB; destruct b; simpl; auto.
+ rewrite EQRS;
destruct (rs x0); try congruence.
assert (HB: (Int.eq i i0) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
rewrite <- HB; destruct b; simpl; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *;
eexists; eexists; eauto; split; constructor; auto;
destruct (rs x) eqn:EQRS; simpl in *; try congruence;
inv EQ2; eexists; eexists; eauto; split; constructor; auto;
simpl in *.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
rewrite <- HB; destruct b; simpl; auto.
+ rewrite EQRS;
destruct (rs x0); try congruence.
assert (HB: negb (Int.eq i i0) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero32, Op.zero32 in *;
rewrite <- HB; destruct b; simpl; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero32, Op.zero32 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero32, Op.zero32 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero32, Op.zero32 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero32, Op.zero32 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero32, Op.zero32 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
destruct (rs x) eqn:EQRS; simpl in *; try congruence;
eexists; eexists; eauto; split; constructor;
simpl in *; auto.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
rewrite <- HB; destruct b; simpl; auto.
+ rewrite EQRS;
destruct (rs x0); try congruence.
assert (HB: (Int64.eq i i0) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
rewrite <- HB; destruct b; simpl; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
destruct (rs x) eqn:EQRS; simpl in *; try congruence;
eexists; eexists; eauto; split; constructor;
simpl in *; auto.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
+ rewrite EQRS;
assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
+ destruct (rs x); simpl in *; try congruence.
rewrite <- HB; destruct b; simpl; auto.
+ rewrite EQRS;
destruct (rs x0); try congruence.
assert (HB: negb (Int64.eq i i0) = b) by congruence.
rewrite HB; destruct b; simpl; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
rewrite <- HB; destruct b; simpl; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
unfold zero64, Op.zero64 in *;
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
Qed.
......@@ -1273,7 +1277,7 @@ Opaque Int.eq.
try rewrite Int64.or_commut;
try rewrite Int.or_commut; auto.
1-12:
destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; inv EQ3;
econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl;
destruct (rs x0); auto;
......
......@@ -66,7 +66,7 @@ let find_or_addnmove op args rd succ map_consts not_final =
if not_final then node := !node - 1;
Sr (P.of_int r)
| None ->
if not (List.exists (fun a -> a = rd) args) && not_final then
if (not (List.exists (fun a -> a = rd) args)) && not_final then
Hashtbl.add map_consts sop (p2i rd);
Si (Iop (op, args, rd, succ))
......@@ -208,131 +208,132 @@ let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul
let is_inv_cmp = function Cle | Cgt -> true | _ -> false
let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None
let make_optR is_x0 is_inv =
if is_x0 then if is_inv then Some X0_L else Some X0_R else None
let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
| Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k
| Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k
| Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k
| Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k
| Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k
| Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k
| Ceq -> Icond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k
| Cne -> Icond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k
| Clt -> Icond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k
| Cle -> Icond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k
| Cgt -> Icond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k
| Cge -> Icond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k
let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with