diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-30 12:48:51 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-30 12:48:51 +0200 |
| commit | df9aab806ae8d20393b56e4175e210ed6cff1ef1 (patch) | |
| tree | 96adb17a591e6c9b72c5b856deeff369a3a7dbb9 /riscV | |
| parent | 83b556a101b7ed490acf9e127c5b4b9db40e1019 (diff) | |
| download | compcert-kvx-df9aab806ae8d20393b56e4175e210ed6cff1ef1.tar.gz compcert-kvx-df9aab806ae8d20393b56e4175e210ed6cff1ef1.zip | |
a more general way to manage special registers before introducing SP
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Asmgen.v | 157 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 56 | ||||
| -rw-r--r-- | riscV/Asmgenproof1.v | 142 | ||||
| -rw-r--r-- | riscV/ExpansionOracle.ml | 121 | ||||
| -rw-r--r-- | riscV/Op.v | 296 | ||||
| -rw-r--r-- | riscV/PrintOp.ml | 98 | ||||
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 185 | ||||
| -rw-r--r-- | riscV/ValueAOp.v | 98 |
8 files changed, 593 insertions, 560 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 54c7a7c0..88d4f73f 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -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; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 9a458b77..101bfa9c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -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: diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 6e5cc531..1e17c4e2 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -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; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index c03e0d03..16f1ee4b 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -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 - | Ceq -> Icond (CEbequw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbneuw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k let cbranch_int64s 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 (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k let cbranch_int64u 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 (CEbequl optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbneul optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ map_consts = - 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 -> [ Iop (OEseqw optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsnew optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltw optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEseqw optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnew optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltw optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltw optR0 in + let op = OEsltw optR in let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltw optR0, [ a2; a1 ], dest, succ) ] + | Cgt -> [ Iop (OEsltw optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltw optR0 in + let op = OEsltw optR in let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ map_consts = - 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 -> [ Iop (OEsequw optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEsequw optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneuw optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltuw optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltuw optR0 in + let op = OEsltuw optR in let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) ] + | Cgt -> [ Iop (OEsltuw optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltuw optR0 in + let op = OEsltuw optR in let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ map_consts = - 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 -> [ Iop (OEseql optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsnel optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltl optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEseql optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnel optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltl optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltl optR0 in + let op = OEsltl optR in let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltl optR0, [ a2; a1 ], dest, succ) ] + | Cgt -> [ Iop (OEsltl optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltl optR0 in + let op = OEsltl optR in let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ map_consts = - 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 -> [ Iop (OEsequl optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsneul optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltul optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEsequl optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneul optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltul optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltul optR0 in + let op = OEsltul optR in let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltul optR0, [ a2; a1 ], dest, succ) ] + | Cgt -> [ Iop (OEsltul optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltul optR0 in + let op = OEsltul optR in let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in @@ -481,8 +482,8 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts = let insn = List.hd (fn_cond cmp f1 f2 r (n2pi ()) map_consts) in insn :: - (if normal' then [ Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) ] - else [ Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info) ]) + (if normal' then [ Icond (CEbnew (Some X0_R), [ r; r ], succ1, succ2, info) ] + else [ Icond (CEbeqw (Some X0_R), [ r; r ], succ1, succ2, info) ]) let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -38,6 +38,11 @@ Set Implicit Arguments. (** Conditions (boolean-valued operators). *) +(* Type to modelize the use of a special register in arith operations *) +Inductive oreg: Type := + | X0_L: oreg + | X0_R: oreg. + Inductive condition : Type := | Ccomp (c: comparison) (**r signed integer comparison *) | Ccompu (c: comparison) (**r unsigned integer comparison *) @@ -52,22 +57,22 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) (* Expansed branches *) - | CEbeqw (optR0: option bool) (**r branch-if-equal signed *) - | CEbnew (optR0: option bool) (**r branch-if-not-equal signed *) - | CEbequw (optR0: option bool) (**r branch-if-equal unsigned *) - | CEbneuw (optR0: option bool) (**r branch-if-not-equal unsigned *) - | CEbltw (optR0: option bool) (**r branch-if-less signed *) - | CEbltuw (optR0: option bool) (**r branch-if-less unsigned *) - | CEbgew (optR0: option bool) (**r branch-if-greater-or-equal signed *) - | CEbgeuw (optR0: option bool) (**r branch-if-greater-or-equal unsigned *) - | CEbeql (optR0: option bool) (**r branch-if-equal signed *) - | CEbnel (optR0: option bool) (**r branch-if-not-equal signed *) - | CEbequl (optR0: option bool) (**r branch-if-equal unsigned *) - | CEbneul (optR0: option bool) (**r branch-if-not-equal unsigned *) - | CEbltl (optR0: option bool) (**r branch-if-less signed *) - | CEbltul (optR0: option bool) (**r branch-if-less unsigned *) - | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) - | CEbgeul (optR0: option bool). (**r branch-if-greater-or-equal unsigned *) + | CEbeqw (optR: option oreg) (**r branch-if-equal signed *) + | CEbnew (optR: option oreg) (**r branch-if-not-equal signed *) + | CEbequw (optR: option oreg) (**r branch-if-equal unsigned *) + | CEbneuw (optR: option oreg) (**r branch-if-not-equal unsigned *) + | CEbltw (optR: option oreg) (**r branch-if-less signed *) + | CEbltuw (optR: option oreg) (**r branch-if-less unsigned *) + | CEbgew (optR: option oreg) (**r branch-if-greater-or-equal signed *) + | CEbgeuw (optR: option oreg) (**r branch-if-greater-or-equal unsigned *) + | CEbeql (optR: option oreg) (**r branch-if-equal signed *) + | CEbnel (optR: option oreg) (**r branch-if-not-equal signed *) + | CEbequl (optR: option oreg) (**r branch-if-equal unsigned *) + | CEbneul (optR: option oreg) (**r branch-if-not-equal unsigned *) + | CEbltl (optR: option oreg) (**r branch-if-less signed *) + | CEbltul (optR: option oreg) (**r branch-if-less unsigned *) + | CEbgel (optR: option oreg) (**r branch-if-greater-or-equal signed *) + | CEbgeul (optR: option oreg). (**r branch-if-greater-or-equal unsigned *) (* This type will define the eval function of a OEmayundef operation. *) Inductive mayundef: Type := @@ -76,7 +81,7 @@ Inductive mayundef: Type := | MUshrx: int -> mayundef | MUshrxl: int -> mayundef. -(* This allow to have a single RTL constructor to perform an arith operation between an immediate and X0 *) +(* Type for allowing a single RTL constructor to perform an arith operation between an immediate and X0 *) Inductive opimm: Type := | OPimmADD: int -> opimm | OPimmADDL: int64 -> opimm. @@ -185,12 +190,12 @@ Inductive operation : Type := | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) | OEimmR0 (opi: opimm) - | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) - | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) - | OEsequw (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) - | OEsneuw (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) - | OEsltw (optR0: option bool) (**r set-less-than *) - | OEsltuw (optR0: option bool) (**r set-less-than unsigned *) + | OEseqw (optR: option oreg) (**r [rd <- rs1 == rs2] signed *) + | OEsnew (optR: option oreg) (**r [rd <- rs1 != rs2] signed *) + | OEsequw (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneuw (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *) + | OEsltw (optR: option oreg) (**r set-less-than *) + | OEsltuw (optR: option oreg) (**r set-less-than unsigned *) | OEsltiw (n: int) (**r set-less-than immediate *) | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) | OEaddiw (n: int) (**r add immediate *) @@ -198,12 +203,12 @@ Inductive operation : Type := | OEoriw (n: int) (**r or immediate *) | OExoriw (n: int) (**r xor immediate *) | OEluiw (n: int) (**r load upper-immediate *) - | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) - | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) - | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) - | OEsneul (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) - | OEsltl (optR0: option bool) (**r set-less-than *) - | OEsltul (optR0: option bool) (**r set-less-than unsigned *) + | OEseql (optR: option oreg) (**r [rd <- rs1 == rs2] signed *) + | OEsnel (optR: option oreg) (**r [rd <- rs1 != rs2] signed *) + | OEsequl (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneul (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *) + | OEsltl (optR: option oreg) (**r set-less-than *) + | OEsltul (optR: option oreg) (**r set-less-than unsigned *) | OEsltil (n: int64) (**r set-less-than immediate *) | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) | OEaddil (n: int64) (**r add immediate *) @@ -235,12 +240,15 @@ Inductive addressing: Type := (** Comparison functions (used in modules [CSE] and [Allocation]). *) +Definition oreg_eq: forall (x y: oreg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec bool_dec; intros. + generalize Int.eq_dec Int64.eq_dec bool_dec oreg_eq; intros. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. decide equality. - all: destruct optR0, optR1; decide equality. + all: destruct optR, optR0; decide equality. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. @@ -251,9 +259,9 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec Val.eq; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec Val.eq oreg_eq; intros. decide equality. - all: try destruct optR0, optR1; try decide equality. + all: try destruct optR, optR0; try decide equality. Defined. (* Alternate definition: @@ -273,11 +281,11 @@ Global Opaque eq_condition eq_addressing eq_operation. Definition zero32 := (Vint Int.zero). Definition zero64 := (Vlong Int64.zero). -Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 vz: val): B := - match optR0 with +Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz: val): B := + match optR with | None => sem v1 v2 - | Some true => sem vz v1 - | Some false => sem v1 vz + | Some X0_L => sem vz v1 + | Some X0_R => sem v1 vz end. Definition eval_may_undef (mu: mayundef) (v1 v2: val): val := @@ -332,22 +340,22 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) (* Expansed branches *) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cne) v1 v2 zero32 - | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 - | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 - | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 - | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 - | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 - | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 - | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 | _, _ => None end. @@ -454,12 +462,12 @@ Definition eval_operation | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) (* Expansed conditions *) | OEimmR0 opi, nil => Some (eval_opimmR0 opi) - | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Cne) v1 v2 zero32) - | OEsequw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) - | OEsneuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) - | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32) - | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) + | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n)) | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) @@ -467,12 +475,12 @@ Definition eval_operation | OEaddiw n, v1::nil => Some (Val.add (Vint n) v1) | OEandiw n, v1::nil => Some (Val.and (Vint n) v1) | OEoriw n, v1::nil => Some (Val.or (Vint n) v1) - | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) - | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64)) - | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) - | OEsneul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) - | OEsltl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Clt) v1 v2 zero64)) - | OEsltul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) + | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64)) + | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64)) + | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) + | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) + | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64)) + | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n))) | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) @@ -924,22 +932,22 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEimmR0 *) - destruct opi; unfold eval_opimmR0; simpl; auto. (* OEseqw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... (* OEsnew *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... (* OEsequw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + - destruct optR as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsneuw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + - destruct optR as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsltw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... (* OEsltuw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + - destruct optR as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsltiw *) - unfold Val.cmp; destruct Val.cmp_bool... @@ -957,22 +965,22 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEluiw *) - destruct (Int.ltu _ _); cbn; trivial. (* OEseql *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + - destruct optR as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... (* OEsnel *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + - destruct optR as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... (* OEsequl *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + - destruct optR as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsneul *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + - destruct optR as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsltl *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + - destruct optR as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... (* OEsltul *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + - destruct optR as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsltil *) - unfold Val.cmpl; destruct Val.cmpl_bool... @@ -1092,22 +1100,22 @@ Definition negate_condition (cond: condition): condition := | Cnotcompf c => Ccompf c | Ccompfs c => Cnotcompfs c | Cnotcompfs c => Ccompfs c - | CEbeqw optR0 => CEbnew optR0 - | CEbnew optR0 => CEbeqw optR0 - | CEbequw optR0 => CEbneuw optR0 - | CEbneuw optR0 => CEbequw optR0 - | CEbltw optR0 => CEbgew optR0 - | CEbltuw optR0 => CEbgeuw optR0 - | CEbgew optR0 => CEbltw optR0 - | CEbgeuw optR0 => CEbltuw optR0 - | CEbeql optR0 => CEbnel optR0 - | CEbnel optR0 => CEbeql optR0 - | CEbequl optR0 => CEbneul optR0 - | CEbneul optR0 => CEbequl optR0 - | CEbltl optR0 => CEbgel optR0 - | CEbltul optR0 => CEbgeul optR0 - | CEbgel optR0 => CEbltl optR0 - | CEbgeul optR0 => CEbltul optR0 + | CEbeqw optR => CEbnew optR + | CEbnew optR => CEbeqw optR + | CEbequw optR => CEbneuw optR + | CEbneuw optR => CEbequw optR + | CEbltw optR => CEbgew optR + | CEbltuw optR => CEbgeuw optR + | CEbgew optR => CEbltw optR + | CEbgeuw optR => CEbltuw optR + | CEbeql optR => CEbnel optR + | CEbnel optR => CEbeql optR + | CEbequl optR => CEbneul optR + | CEbneul optR => CEbequl optR + | CEbltl optR => CEbgel optR + | CEbltul optR => CEbgeul optR + | CEbgel optR => CEbltl optR + | CEbgeul optR => CEbltul optR end. Lemma eval_negate_condition: @@ -1128,37 +1136,37 @@ Proof. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. Qed. @@ -1303,7 +1311,7 @@ Proof. f_equal. f_equal. apply cond_depends_on_memory_correct; trivial. all: intros; repeat (destruct args; auto); unfold Val.cmpu, Val.cmpu_bool, Val.cmplu, Val.cmplu_bool; - try destruct optR0 as [[]|]; simpl; + try destruct optR as [[]|]; simpl; destruct v; try destruct v0; simpl; auto; try apply negb_false_iff in H; try rewrite H; auto. Qed. @@ -1315,7 +1323,7 @@ Lemma cond_valid_pointer_eq: Proof. intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence. all: repeat (destruct args; simpl; try congruence); - try destruct optR0 as [[]|]; simpl; + try destruct optR as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; try erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. @@ -1328,7 +1336,7 @@ Proof. intros until m2. destruct op; simpl; try congruence. intro MEM; erewrite cond_valid_pointer_eq; eauto. all: intros MEM; repeat (destruct args; simpl; try congruence); - try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; + try destruct optR as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; unfold Val.cmpu, Val.cmplu; erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. @@ -1460,14 +1468,14 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. -Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR0, +Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32) - (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32). + Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32) + (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32). Proof. - intros until optR0. intros HV1 HV2. - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmpu; + intros until optR. intros HV1 HV2. + destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu; destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto; assert (HVI: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int. + exploit eval_cmpu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo. @@ -1501,14 +1509,14 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. -Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR0, +Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64)) - (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)). + Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64)) + (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)). Proof. - intros until optR0. intros HV1 HV2. - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmplu; + intros until optR. intros HV1 HV2. + destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu; destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto; assert (HVI: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long. + exploit eval_cmplu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo. @@ -1541,37 +1549,37 @@ Proof. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. Qed. @@ -1784,11 +1792,11 @@ Proof. (* OEimmR0 *) - destruct opi; unfold eval_opimmR0; simpl; auto. (* OEseqw *) - - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsnew *) - - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsequw *) @@ -1796,7 +1804,7 @@ Proof. (* OEsneuw *) - apply eval_cmpu_bool_inj_opt; auto. (* OEsltw *) - - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsltuw *) @@ -1818,11 +1826,11 @@ Proof. (* OEluiw *) - destruct (Int.ltu _ _); auto. (* OEseql *) - - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsnel *) - - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsequl *) @@ -1830,7 +1838,7 @@ Proof. (* OEsneul *) - apply eval_cmplu_bool_inj_opt; auto. (* OEsltl *) - - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsltul *) diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 9b3e8835..e18d31f6 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -40,14 +40,10 @@ let get_immR0 pp = function | OPimmADD i -> fprintf pp "OPimmADD(%ld)" (camlint_of_coqint i) | OPimmADDL i -> fprintf pp "OPimmADDL(%ld)" (camlint_of_coqint i) -let get_optR0_s c reg pp r1 r2 = function +let get_optR_s c reg pp r1 r2 = function | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2 - | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1 - | Some false -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c) - -let get_optR0_s_int reg pp r1 n = function - | None -> fprintf pp "(%a, %ld)" reg r1 n - | Some _ -> fprintf pp "(X0, %ld)" n + | Some X0_L -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1 + | Some X0_R -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c) let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> @@ -74,38 +70,38 @@ let print_condition reg pp = function fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 | (Cnotcompfs c, [r1;r2]) -> fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 - | (CEbeqw optR0, [r1;r2]) -> - fprintf pp "CEbeqw"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | (CEbnew optR0, [r1;r2]) -> - fprintf pp "CEbnew"; (get_optR0_s Cne reg pp r1 r2 optR0) - | (CEbequw optR0, [r1;r2]) -> - fprintf pp "CEbequw"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | (CEbneuw optR0, [r1;r2]) -> - fprintf pp "CEbneuw"; (get_optR0_s Cne reg pp r1 r2 optR0) - | (CEbltw optR0, [r1;r2]) -> - fprintf pp "CEbltw"; (get_optR0_s Clt reg pp r1 r2 optR0) - | (CEbltuw optR0, [r1;r2]) -> - fprintf pp "CEbltuw"; (get_optR0_s Clt reg pp r1 r2 optR0) - | (CEbgew optR0, [r1;r2]) -> - fprintf pp "CEbgew"; (get_optR0_s Cge reg pp r1 r2 optR0) - | (CEbgeuw optR0, [r1;r2]) -> - fprintf pp "CEbgeuw"; (get_optR0_s Cge reg pp r1 r2 optR0) - | (CEbeql optR0, [r1;r2]) -> - fprintf pp "CEbeql"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | (CEbnel optR0, [r1;r2]) -> - fprintf pp "CEbnel"; (get_optR0_s Cne reg pp r1 r2 optR0) - | (CEbequl optR0, [r1;r2]) -> - fprintf pp "CEbequl"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | (CEbneul optR0, [r1;r2]) -> - fprintf pp "CEbneul"; (get_optR0_s Cne reg pp r1 r2 optR0) - | (CEbltl optR0, [r1;r2]) -> - fprintf pp "CEbltl"; (get_optR0_s Clt reg pp r1 r2 optR0) - | (CEbltul optR0, [r1;r2]) -> - fprintf pp "CEbltul"; (get_optR0_s Clt reg pp r1 r2 optR0) - | (CEbgel optR0, [r1;r2]) -> - fprintf pp "CEbgel"; (get_optR0_s Cge reg pp r1 r2 optR0) - | (CEbgeul optR0, [r1;r2]) -> - fprintf pp "CEbgeul"; (get_optR0_s Cge reg pp r1 r2 optR0) + | (CEbeqw optR, [r1;r2]) -> + fprintf pp "CEbeqw"; (get_optR_s Ceq reg pp r1 r2 optR) + | (CEbnew optR, [r1;r2]) -> + fprintf pp "CEbnew"; (get_optR_s Cne reg pp r1 r2 optR) + | (CEbequw optR, [r1;r2]) -> + fprintf pp "CEbequw"; (get_optR_s Ceq reg pp r1 r2 optR) + | (CEbneuw optR, [r1;r2]) -> + fprintf pp "CEbneuw"; (get_optR_s Cne reg pp r1 r2 optR) + | (CEbltw optR, [r1;r2]) -> + fprintf pp "CEbltw"; (get_optR_s Clt reg pp r1 r2 optR) + | (CEbltuw optR, [r1;r2]) -> + fprintf pp "CEbltuw"; (get_optR_s Clt reg pp r1 r2 optR) + | (CEbgew optR, [r1;r2]) -> + fprintf pp "CEbgew"; (get_optR_s Cge reg pp r1 r2 optR) + | (CEbgeuw optR, [r1;r2]) -> + fprintf pp "CEbgeuw"; (get_optR_s Cge reg pp r1 r2 optR) + | (CEbeql optR, [r1;r2]) -> + fprintf pp "CEbeql"; (get_optR_s Ceq reg pp r1 r2 optR) + | (CEbnel optR, [r1;r2]) -> + fprintf pp "CEbnel"; (get_optR_s Cne reg pp r1 r2 optR) + | (CEbequl optR, [r1;r2]) -> + fprintf pp "CEbequl"; (get_optR_s Ceq reg pp r1 r2 optR) + | (CEbneul optR, [r1;r2]) -> + fprintf pp "CEbneul"; (get_optR_s Cne reg pp r1 r2 optR) + | (CEbltl optR, [r1;r2]) -> + fprintf pp "CEbltl"; (get_optR_s Clt reg pp r1 r2 optR) + | (CEbltul optR, [r1;r2]) -> + fprintf pp "CEbltul"; (get_optR_s Clt reg pp r1 r2 optR) + | (CEbgel optR, [r1;r2]) -> + fprintf pp "CEbgel"; (get_optR_s Cge reg pp r1 r2 optR) + | (CEbgeul optR, [r1;r2]) -> + fprintf pp "CEbgeul"; (get_optR_s Cge reg pp r1 r2 optR) | _ -> fprintf pp "<bad condition>" @@ -208,12 +204,12 @@ let print_operation reg pp = function | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) | OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi - | OEseqw optR0, [r1;r2] -> fprintf pp "OEseqw"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | OEsnew optR0, [r1;r2] -> fprintf pp "OEsnew"; (get_optR0_s Cne reg pp r1 r2 optR0) - | OEsequw optR0, [r1;r2] -> fprintf pp "OEsequw"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | OEsneuw optR0, [r1;r2] -> fprintf pp "OEsneuw"; (get_optR0_s Cne reg pp r1 r2 optR0) - | OEsltw optR0, [r1;r2] -> fprintf pp "OEsltw"; (get_optR0_s Clt reg pp r1 r2 optR0) - | OEsltuw optR0, [r1;r2] -> fprintf pp "OEsltuw"; (get_optR0_s Clt reg pp r1 r2 optR0) + | OEseqw optR, [r1;r2] -> fprintf pp "OEseqw"; (get_optR_s Ceq reg pp r1 r2 optR) + | OEsnew optR, [r1;r2] -> fprintf pp "OEsnew"; (get_optR_s Cne reg pp r1 r2 optR) + | OEsequw optR, [r1;r2] -> fprintf pp "OEsequw"; (get_optR_s Ceq reg pp r1 r2 optR) + | OEsneuw optR, [r1;r2] -> fprintf pp "OEsneuw"; (get_optR_s Cne reg pp r1 r2 optR) + | OEsltw optR, [r1;r2] -> fprintf pp "OEsltw"; (get_optR_s Clt reg pp r1 r2 optR) + | OEsltuw optR, [r1;r2] -> fprintf pp "OEsltuw"; (get_optR_s Clt reg pp r1 r2 optR) | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n) @@ -221,12 +217,12 @@ let print_operation reg pp = function | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (camlint_of_coqint n) - | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0) - | OEsequl optR0, [r1;r2] -> fprintf pp "OEsequl"; (get_optR0_s Ceq reg pp r1 r2 optR0) - | OEsneul optR0, [r1;r2] -> fprintf pp "OEsneul"; (get_optR0_s Cne reg pp r1 r2 optR0) - | OEsltl optR0, [r1;r2] -> fprintf pp "OEsltl"; (get_optR0_s Clt reg pp r1 r2 optR0) - | OEsltul optR0, [r1;r2] -> fprintf pp "OEsltul"; (get_optR0_s Clt reg pp r1 r2 optR0) + | OEseql optR, [r1;r2] -> fprintf pp "OEseql"; (get_optR_s Ceq reg pp r1 r2 optR) + | OEsnel optR, [r1;r2] -> fprintf pp "OEsnel"; (get_optR_s Cne reg pp r1 r2 optR) + | OEsequl optR, [r1;r2] -> fprintf pp "OEsequl"; (get_optR_s Ceq reg pp r1 r2 optR) + | OEsneul optR, [r1;r2] -> fprintf pp "OEsneul"; (get_optR_s Cne reg pp r1 r2 optR) + | OEsltl optR, [r1;r2] -> fprintf pp "OEsltl"; (get_optR_s Clt reg pp r1 r2 optR) + | OEsltul optR, [r1;r2] -> fprintf pp "OEsltul"; (get_optR_s Clt reg pp r1 r2 optR) | OEsltil n, [r1] -> fprintf pp "OEsltil(%a,%ld)" reg r1 (camlint_of_coqint n) | OEsltiul n, [r1] -> fprintf pp "OEsltiul(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n) diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 08c1a6a0..5b44caba 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -14,8 +14,11 @@ Definition is_inv_cmp_int (cmp: comparison) : bool := Definition is_inv_cmp_float (cmp: comparison) : bool := match cmp with | Cge | Cgt => true | _ => false end. -Definition make_optR0 (is_x0 is_inv: bool) : option bool := - if is_x0 then Some is_inv else None. +Definition make_optR (is_x0 is_inv: bool) : option oreg := + if is_x0 then + (if is_inv then Some (X0_L) + else Some (X0_R)) + else None. (** Functions to manage lists of "fake" values *) @@ -103,46 +106,46 @@ Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEs (* Comparisons intructions *) -Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := +Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) := match cmp with - | Ceq => fSop (OEseqw optR0) lhsv - | Cne => fSop (OEsnew optR0) lhsv - | Clt | Cgt => fSop (OEsltw optR0) lhsv + | Ceq => fSop (OEseqw optR) lhsv + | Cne => fSop (OEsnew optR) lhsv + | Clt | Cgt => fSop (OEsltw optR) lhsv | Cle | Cge => - let hvs := (fSop (OEsltw optR0) lhsv) in + let hvs := (fSop (OEsltw optR) lhsv) in let hl := make_lhsv_single hvs in fSop (OExoriw Int.one) hl end. -Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := +Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) := match cmp with - | Ceq => fSop (OEsequw optR0) lhsv - | Cne => fSop (OEsneuw optR0) lhsv - | Clt | Cgt => fSop (OEsltuw optR0) lhsv + | Ceq => fSop (OEsequw optR) lhsv + | Cne => fSop (OEsneuw optR) lhsv + | Clt | Cgt => fSop (OEsltuw optR) lhsv | Cle | Cge => - let hvs := (fSop (OEsltuw optR0) lhsv) in + let hvs := (fSop (OEsltuw optR) lhsv) in let hl := make_lhsv_single hvs in fSop (OExoriw Int.one) hl end. -Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := +Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) := match cmp with - | Ceq => fSop (OEseql optR0) lhsv - | Cne => fSop (OEsnel optR0) lhsv - | Clt | Cgt => fSop (OEsltl optR0) lhsv + | Ceq => fSop (OEseql optR) lhsv + | Cne => fSop (OEsnel optR) lhsv + | Clt | Cgt => fSop (OEsltl optR) lhsv | Cle | Cge => - let hvs := (fSop (OEsltl optR0) lhsv) in + let hvs := (fSop (OEsltl optR) lhsv) in let hl := make_lhsv_single hvs in fSop (OExoriw Int.one) hl end. -Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := +Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) := match cmp with - | Ceq => fSop (OEsequl optR0) lhsv - | Cne => fSop (OEsneul optR0) lhsv - | Clt | Cgt => fSop (OEsltul optR0) lhsv + | Ceq => fSop (OEsequl optR) lhsv + | Cne => fSop (OEsneul optR) lhsv + | Clt | Cgt => fSop (OEsltul optR) lhsv | Cle | Cge => - let hvs := (fSop (OEsltul optR0) lhsv) in + let hvs := (fSop (OEsltul optR) lhsv) in let hl := make_lhsv_single hvs in fSop (OExoriw Int.one) hl end. @@ -150,16 +153,16 @@ Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) := let is_inv := is_inv_cmp_int cmp in if Int.eq n Int.zero then - let optR0 := make_optR0 true is_inv in + let optR := make_optR true is_inv in let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int32s cmp hl optR0 + cond_int32s cmp hl optR else match cmp with | Ceq | Cne => - let optR0 := make_optR0 true is_inv in + let optR := make_optR true is_inv in let hvs := xorimm32 hv1 n in let hl := make_lhsv_cmp false hvs hvs in - cond_int32s cmp hl optR0 + cond_int32s cmp hl optR | Clt => sltimm32 hv1 n | Cle => if Int.eq n (Int.repr Int.max_signed) then @@ -168,41 +171,41 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) := fSop (OEmayundef MUint) hl else sltimm32 hv1 (Int.add n Int.one) | _ => - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let hvs := loadimm32 n in let hl := make_lhsv_cmp is_inv hv1 hvs in - cond_int32s cmp hl optR0 + cond_int32s cmp hl optR end. Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) := let is_inv := is_inv_cmp_int cmp in if Int.eq n Int.zero then - let optR0 := make_optR0 true is_inv in + let optR := make_optR true is_inv in let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int32u cmp hl optR0 + cond_int32u cmp hl optR else match cmp with | Clt => sltuimm32 hv1 n | _ => - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let hvs := loadimm32 n in let hl := make_lhsv_cmp is_inv hv1 hvs in - cond_int32u cmp hl optR0 + cond_int32u cmp hl optR end. Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := let is_inv := is_inv_cmp_int cmp in if Int64.eq n Int64.zero then - let optR0 := make_optR0 true is_inv in + let optR := make_optR true is_inv in let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int64s cmp hl optR0 + cond_int64s cmp hl optR else match cmp with | Ceq | Cne => - let optR0 := make_optR0 true is_inv in + let optR := make_optR true is_inv in let hvs := xorimm64 hv1 n in let hl := make_lhsv_cmp false hvs hvs in - cond_int64s cmp hl optR0 + cond_int64s cmp hl optR | Clt => sltimm64 hv1 n | Cle => if Int64.eq n (Int64.repr Int64.max_signed) then @@ -211,26 +214,26 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := fSop (OEmayundef MUlong) hl else sltimm64 hv1 (Int64.add n Int64.one) | _ => - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let hvs := loadimm64 n in let hl := make_lhsv_cmp is_inv hv1 hvs in - cond_int64s cmp hl optR0 + cond_int64s cmp hl optR end. Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) := let is_inv := is_inv_cmp_int cmp in if Int64.eq n Int64.zero then - let optR0 := make_optR0 true is_inv in + let optR := make_optR true is_inv in let hl := make_lhsv_cmp is_inv hv1 hv1 in - cond_int64u cmp hl optR0 + cond_int64u cmp hl optR else match cmp with | Clt => sltuimm64 hv1 n | _ => - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let hvs := loadimm64 n in let hl := make_lhsv_cmp is_inv hv1 hvs in - cond_int64u cmp hl optR0 + cond_int64u cmp hl optR end. Definition cond_float (cmp: comparison) (lhsv: list_hsval) := @@ -259,44 +262,44 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) := (* Branches instructions *) -Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) := +Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) := match cmp with - | Ceq => CEbeqw optR0 - | Cne => CEbnew optR0 - | Clt => CEbltw optR0 - | Cle => CEbgew optR0 - | Cgt => CEbltw optR0 - | Cge => CEbgew optR0 + | Ceq => CEbeqw optR + | Cne => CEbnew optR + | Clt => CEbltw optR + | Cle => CEbgew optR + | Cgt => CEbltw optR + | Cge => CEbgew optR end. -Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) := +Definition transl_cbranch_int32u (cmp: comparison) (optR: option oreg) := match cmp with - | Ceq => CEbequw optR0 - | Cne => CEbneuw optR0 - | Clt => CEbltuw optR0 - | Cle => CEbgeuw optR0 - | Cgt => CEbltuw optR0 - | Cge => CEbgeuw optR0 + | Ceq => CEbequw optR + | Cne => CEbneuw optR + | Clt => CEbltuw optR + | Cle => CEbgeuw optR + | Cgt => CEbltuw optR + | Cge => CEbgeuw optR end. -Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) := +Definition transl_cbranch_int64s (cmp: comparison) (optR: option oreg) := match cmp with - | Ceq => CEbeql optR0 - | Cne => CEbnel optR0 - | Clt => CEbltl optR0 - | Cle => CEbgel optR0 - | Cgt => CEbltl optR0 - | Cge => CEbgel optR0 + | Ceq => CEbeql optR + | Cne => CEbnel optR + | Clt => CEbltl optR + | Cle => CEbgel optR + | Cgt => CEbltl optR + | Cge => CEbgel optR end. -Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := +Definition transl_cbranch_int64u (cmp: comparison) (optR: option oreg) := match cmp with - | Ceq => CEbequl optR0 - | Cne => CEbneul optR0 - | Clt => CEbltul optR0 - | Cle => CEbgeul optR0 - | Cgt => CEbltul optR0 - | Cge => CEbgeul optR0 + | Ceq => CEbequl optR + | Cne => CEbneul optR + | Clt => CEbltul optR + | Cle => CEbgeul optR + | Cgt => CEbltul optR + | Cge => CEbgeul optR end. Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (condition * list_hsval) := @@ -304,7 +307,7 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con let normal' := if cnot then negb normal else normal in let hvs := fn_cond cmp lhsv in let hl := make_lhsv_cmp false hvs hvs in - if normal' then ((CEbnew (Some false)), hl) else ((CEbeqw (Some false)), hl). + if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl). (** Add pointer expansion *) @@ -325,16 +328,16 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let hv1 := fsi_sreg_get hst a1 in let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (cond_int32s c lhsv optR0) + Some (cond_int32s c lhsv optR) | Ocmp (Ccompu c), a1 :: a2 :: nil => let hv1 := fsi_sreg_get hst a1 in let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (cond_int32u c lhsv optR0) + Some (cond_int32u c lhsv optR) | Ocmp (Ccompimm c imm), a1 :: nil => let hv1 := fsi_sreg_get hst a1 in Some (expanse_condimm_int32s c hv1 imm) @@ -345,16 +348,16 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let hv1 := fsi_sreg_get hst a1 in let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (cond_int64s c lhsv optR0) + Some (cond_int64s c lhsv optR) | Ocmp (Ccomplu c), a1 :: a2 :: nil => let hv1 := fsi_sreg_get hst a1 in let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in + let optR := make_optR false is_inv in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in - Some (cond_int64u c lhsv optR0) + Some (cond_int64u c lhsv optR) | Ocmp (Ccomplimm c imm), a1 :: nil => let hv1 := fsi_sreg_get hst a1 in Some (expanse_condimm_int64s c hv1 imm) @@ -497,14 +500,14 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args match cond, args with | (Ccomp c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in - let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in + let cond := transl_cbranch_int32s c (make_optR false is_inv) in let hv1 := fsi_sreg_get prev a1 in let hv2 := fsi_sreg_get prev a2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in Some (cond, lhsv) | (Ccompu c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in - let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in + let cond := transl_cbranch_int32u c (make_optR false is_inv) in let hv1 := fsi_sreg_get prev a1 in let hv2 := fsi_sreg_get prev a2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in @@ -514,35 +517,35 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let hv1 := fsi_sreg_get prev a1 in (if Int.eq n Int.zero then let lhsv := make_lhsv_cmp is_inv hv1 hv1 in - let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in + let cond := transl_cbranch_int32s c (make_optR true is_inv) in Some (cond, lhsv) else let hvs := loadimm32 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in - let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in + let cond := transl_cbranch_int32s c (make_optR false is_inv) in Some (cond, lhsv)) | (Ccompuimm c n), (a1 :: nil) => let is_inv := is_inv_cmp_int c in let hv1 := fsi_sreg_get prev a1 in (if Int.eq n Int.zero then let lhsv := make_lhsv_cmp is_inv hv1 hv1 in - let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in + let cond := transl_cbranch_int32u c (make_optR true is_inv) in Some (cond, lhsv) else let hvs := loadimm32 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in - let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in + let cond := transl_cbranch_int32u c (make_optR false is_inv) in Some (cond, lhsv)) | (Ccompl c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in - let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in + let cond := transl_cbranch_int64s c (make_optR false is_inv) in let hv1 := fsi_sreg_get prev a1 in let hv2 := fsi_sreg_get prev a2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in Some (cond, lhsv) | (Ccomplu c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in - let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in + let cond := transl_cbranch_int64u c (make_optR false is_inv) in let hv1 := fsi_sreg_get prev a1 in let hv2 := fsi_sreg_get prev a2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in @@ -552,24 +555,24 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let hv1 := fsi_sreg_get prev a1 in (if Int64.eq n Int64.zero then let lhsv := make_lhsv_cmp is_inv hv1 hv1 in - let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in + let cond := transl_cbranch_int64s c (make_optR true is_inv) in Some (cond, lhsv) else let hvs := loadimm64 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in - let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in + let cond := transl_cbranch_int64s c (make_optR false is_inv) in Some (cond, lhsv)) | (Ccompluimm c n), (a1 :: nil) => let is_inv := is_inv_cmp_int c in let hv1 := fsi_sreg_get prev a1 in (if Int64.eq n Int64.zero then let lhsv := make_lhsv_cmp is_inv hv1 hv1 in - let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in + let cond := transl_cbranch_int64u c (make_optR true is_inv) in Some (cond, lhsv) else let hvs := loadimm64 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in - let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in + let cond := transl_cbranch_int64u c (make_optR false is_inv) in Some (cond, lhsv)) | (Ccompf c), (f1 :: f2 :: nil) => let hv1 := fsi_sreg_get prev f1 in diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index b64040e1..e48c4a5b 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -20,11 +20,11 @@ Require Import Zbits. Definition zero32 := (I Int.zero). Definition zero64 := (L Int64.zero). -Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := - match optR0 with +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := + match optR with | None => sem v1 v2 - | Some true => sem vz v1 - | Some false => sem v1 vz + | Some X0_L => sem vz v1 + | Some X0_R => sem v1 vz end. Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := @@ -71,22 +71,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32 - | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32 - | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 - | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32 - | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64 - | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 - | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64 - | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 | _, _ => Bnone end. @@ -227,12 +227,12 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) | OEimmR0 opi, nil => eval_opimmR0 opi - | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32) - | OEsequw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) - | OEsneuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32) - | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32) - | OEsltuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32) + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) @@ -240,12 +240,12 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEaddiw n, v1::nil => add (I n) v1 | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 - | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) - | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) - | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) - | OEsneul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64) - | OEsltl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64) - | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64) + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OEandil n, v1::nil => andl (L n) v1 @@ -358,7 +358,7 @@ Proof. inv H2. destruct cond; simpl; eauto with va. 17: destruct cond; simpl; eauto with va. - all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0; + all: destruct optR as [[]|]; unfold apply_bin_oreg, Op.apply_bin_oreg; unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. @@ -415,53 +415,53 @@ Proof. inv H; auto. simpl. destruct b; constructor. Qed. -Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m, +Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmpu_bool c) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR0 m, +Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc (Val.maketotal - (Op.apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) c) a1 a0 + (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmplu_bool c) b1 b0 zero64)). + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. -Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0 cmp, +Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp cmp) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmp_bool cmp) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0 cmp, +Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl cmp) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmpl_bool cmp) b1 b0 zero64)). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. |