diff options
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Asmgen.v | 211 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 38 | ||||
| -rw-r--r-- | riscV/Asmgenproof1.v | 415 | ||||
| -rw-r--r-- | riscV/ExpansionOracle.ml | 539 | ||||
| -rw-r--r-- | riscV/NeedOp.v | 30 | ||||
| -rw-r--r-- | riscV/Op.v | 536 | ||||
| -rw-r--r-- | riscV/OpWeights.ml | 18 | ||||
| -rw-r--r-- | riscV/PrintOp.ml | 66 | ||||
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 1323 | ||||
| -rw-r--r-- | riscV/ValueAOp.v | 162 |
10 files changed, 3193 insertions, 145 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index b87d2692..252a9270 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -203,8 +203,22 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := | Cle => (Pfles rd fs1 fs2, true) | Cgt => (Pflts rd fs2 fs1, true) | 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 + 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 transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with @@ -259,7 +273,56 @@ Definition transl_cbranch | Cnotcompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; 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) + OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) + + | CEbeqw optR0, 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + 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 => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbgeul r1 r2 lbl :: k) | _, _ => Error(msg "Asmgen.transl_cond_branch") end. @@ -342,7 +405,7 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int match cmp with | Clt => sltuimm64 rd r1 n k | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) - end. + end. Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: code) := @@ -364,13 +427,13 @@ Definition transl_cond_op OK (transl_cond_int64s c rd r1 r2 k) | Ccomplu c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int64u c rd r1 r2 k) + OK (transl_cond_int64u c rd r1 r2 k) | Ccomplimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (transl_condimm_int64s c rd r1 n k) | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; - OK (transl_condimm_int64u c rd r1 n k) + OK (transl_condimm_int64u c rd r1 n k) | Ccompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_float c rd r1 r2 in @@ -386,14 +449,14 @@ Definition transl_cond_op | Cnotcompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) + OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) | _, _ => Error(msg "Asmgen.transl_cond_op") - end. + end. (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) - + Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with @@ -704,6 +767,138 @@ Definition transl_op | Osingleoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) + | Ocmp cmp, _ => + do rd <- ireg_of res; + transl_cond_op cmp rd args k + | OEseqw optR0, 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 => + 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 => + 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 => + 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 => + 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 => + 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) + | OEsltiw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Psltiw rd rs n :: k) + | OEsltiuw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Psltiuw rd rs n :: k) + | OExoriw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Pxoriw rd rs n :: k) + | OEluiw n _, a1 :: nil => + do rd <- ireg_of res; + OK (Pluiw rd n :: k) + | OEaddiwr0 n _, a1 :: nil => + do rd <- ireg_of res; + OK (Paddiw rd X0 n :: k) + | OEseql optR0, 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 => + 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 => + 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 => + 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 => + 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 => + 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) + | OEsltil n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Psltil rd rs n :: k) + | OEsltiul n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Psltiul rd rs n :: k) + | OExoril n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Pxoril rd rs n :: k) + | OEluil n, a1 :: nil => + do rd <- ireg_of res; + OK (Pluil rd n :: k) + | OEaddilr0 n, a1 :: nil => + do rd <- ireg_of res; + OK (Paddil rd X0 n :: k) + | OEloadli n, nil => + do rd <- ireg_of res; + OK (Ploadli rd n :: k) + | OEfeqd, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfeqd rd r1 r2 :: k) + | OEfltd, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfltd rd r1 r2 :: k) + | OEfled, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfled rd r1 r2 :: k) + | OEfeqs, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfeqs rd r1 r2 :: k) + | OEflts, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pflts rd r1 r2 :: k) + | OEfles, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfles rd r1 r2 :: k) | Obits_of_single, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 8e9f022c..82c1917d 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -173,7 +173,7 @@ Remark transl_cond_single_nolabel: transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn. Proof. unfold transl_cond_single; intros. destruct c; inv H; exact I. -Qed. + Qed. Remark transl_cbranch_label: forall cond args lbl k c, @@ -211,7 +211,23 @@ Proof. destruct normal; TailNoLabel. - 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 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. Qed. Remark transl_cond_op_label: @@ -238,7 +254,7 @@ Proof. try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]). apply opimm32_label; intros; exact I. - destruct c0; simpl; TailNoLabel. -- destruct c0; simpl; TailNoLabel. + - destruct c0; simpl; TailNoLabel. - unfold transl_condimm_int64s. destruct (Int64.eq n Int64.zero). + destruct c0; simpl; TailNoLabel. @@ -254,7 +270,7 @@ Proof. + destruct c0; simpl; TailNoLabel. + destruct c0; simpl; try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]). - apply opimm64_label; intros; exact I. + apply opimm64_label; intros; exact I. - destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. destruct normal; TailNoLabel. @@ -267,7 +283,7 @@ Proof. - destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. destruct normal; TailNoLabel. -Qed. + Qed. Remark transl_op_label: forall op args r k c, @@ -292,6 +308,18 @@ Opaque Int.eq. - apply opimm64_label; intros; exact I. - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - eapply transl_cond_op_label; eauto. +- 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. Qed. Remark indexed_memory_access_label: diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 5940802c..1b3a0dbf 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -375,16 +375,16 @@ Proof. rewrite <- Float32.cmp_swap. auto. - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. rewrite <- Float32.cmp_swap. auto. -Qed. + Qed. -Remark branch_on_X31: +(* TODO gourdinl UNUSUED ? Remark branch_on_X31: forall normal lbl (rs: regset) m b, rs#X31 = Val.of_bool (eqb normal b) -> exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = eval_branch fn lbl rs m (Some b). Proof. intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. -Qed. + Qed.*) Ltac ArgsInv := repeat (match goal with @@ -417,7 +417,7 @@ Proof. { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } clear EVAL MEXT AG. destruct cond; simpl in TRANSL; ArgsInv. -- exists rs, (transl_cbranch_int32s c0 x x0 lbl). + - exists rs, (transl_cbranch_int32s c0 x x0 lbl). intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. - exists rs, (transl_cbranch_int32u c0 x x0 lbl). intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. @@ -492,7 +492,128 @@ Proof. econstructor; econstructor. split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. + intros; Simpl. + +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; + 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 *; + 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 *; + 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 *; + 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 *; + 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 *; + 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 *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + 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 *; + 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 *; + 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 *; + 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 *; + 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 *; + 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 *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. Qed. Lemma transl_cbranch_correct_true: @@ -830,7 +951,7 @@ Proof. + apply DFL. + apply DFL. + apply DFL. -Qed. + Qed. Lemma transl_cond_op_correct: forall cond rd args k c rs m, @@ -858,7 +979,7 @@ Proof. exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + (* cmplu *) exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. + exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. + (* cmplimm *) exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. intros (rs' & A & B & C). @@ -866,7 +987,7 @@ Proof. + (* cmpluimm *) exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + (* cmpf *) destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. fold (Val.cmpf c0 (rs x) (rs x0)). @@ -923,7 +1044,7 @@ Proof. * econstructor; split. apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. split; intros; Simpl. -Qed. + Qed. (** Some arithmetic properties. *) @@ -964,136 +1085,189 @@ Proof. Opaque Int.eq. intros until c; intros TR EV. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl. -- (* move *) - destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. -- (* intconst *) - exploit loadimm32_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* longconst *) - exploit loadimm64_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* floatconst *) - destruct (Float.eq_dec n Float.zero). -+ subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -- (* singleconst *) - destruct (Float32.eq_dec n Float32.zero). -+ subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -- (* addrsymbol *) - destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). -+ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). - exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. - intros (rs2 & A & B & C). - exists rs2; split. - apply exec_straight_step with rs1 m; auto. - split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). - rewrite Genv.shift_symbol_address. - replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl). - exact B. - intros. rewrite C by eauto with asmgen. unfold rs1; Simpl. -+ TranslOpSimpl. -- (* stackoffset *) - exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. auto with asmgen. -- (* cast8signed *) - econstructor; split. + (* move *) + { destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. } + (* intconst *) + { exploit loadimm32_correct; eauto. intros (rs' & A & B & C). + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* longconst *) + { exploit loadimm64_correct; eauto. intros (rs' & A & B & C). + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* floatconst *) + { destruct (Float.eq_dec n Float.zero). + + subst n. econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + + econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. } + (* singleconst *) + { destruct (Float32.eq_dec n Float32.zero). + + subst n. econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + + econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. } + (* addrsymbol *) + { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). + + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). + exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. + intros (rs2 & A & B & C). + exists rs2; split. + apply exec_straight_step with rs1 m; auto. + split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). + rewrite Genv.shift_symbol_address. + replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl). + exact B. + intros. rewrite C by eauto with asmgen. unfold rs1; Simpl. + + TranslOpSimpl. } + (* stackoffset *) + { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). + exists rs'; split; eauto. auto with asmgen. } + (* cast8signed *) + { econstructor; split. eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. split; intros; Simpl. assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. -- (* cast16signed *) - econstructor; split. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } + (* cast16signed *) + { econstructor; split. eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. split; intros; Simpl. assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. -- (* addimm *) - exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } + (* addimm *) + { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* andimm *) - exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen. + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* andimm *) + { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* orimm *) + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* orimm *) exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen. + { intros (rs' & A & B & C). + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* xorimm *) + { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* xorimm *) - exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* shrximm *) - destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn. - { - exploit Val.shrx_shr_3; eauto. intros E; subst v. - destruct (Int.eq n Int.zero). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - } - destruct (Int.eq n Int.zero). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - -- (* longofintu *) - econstructor; split. + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* shrximm *) + { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn. + { + exploit Val.shrx_shr_3; eauto. intros E; subst v. + destruct (Int.eq n Int.zero). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + + destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + } + destruct (Int.eq n Int.zero). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + + destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. } + (* longofintu *) + { econstructor; split. eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto. split; intros; Simpl. destruct (rs x0); auto. simpl. assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal. - rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. -- (* addlimm *) - exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen. + rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. } + (* addlimm *) + { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* andimm *) - exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen. + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* andimm *) + { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* orimm *) - exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen. + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* orimm *) + { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* xorimm *) - exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen. + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* xorimm *) + { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). + exists rs'; split; eauto. rewrite B; auto with asmgen. } + (* shrxlimm *) + { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. + { + exploit Val.shrxl_shrl_3; eauto. intros E; subst v. + destruct (Int.eq n Int.zero). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + + destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + + * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + } + destruct (Int.eq n Int.zero). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + + destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + + * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. } + (* cond *) + { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). + exists rs'; split. eexact A. eauto with asmgen. } + (* Expanded instructions from RTL *) + 7,8,15,16: + econstructor; split; try apply exec_straight_one; simpl; eauto; + split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl; + try rewrite Int.add_commut; try rewrite Int64.add_commut; + destruct (rs (preg_of m0)); try discriminate; eauto. + all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; + econstructor; split; try apply exec_straight_one; simpl; eauto; + split; intros; Simpl. + all: destruct (rs x0); auto. + all: destruct (rs x1); auto. exists rs'; split; eauto. rewrite B; auto with asmgen. - (* shrxlimm *) destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. @@ -1449,6 +1623,3 @@ Proof. Qed. End CONSTRUCTORS. - - - diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml new file mode 100644 index 00000000..95a300c5 --- /dev/null +++ b/riscV/ExpansionOracle.ml @@ -0,0 +1,539 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +open RTLpathLivegenaux +open RTLpathCommon +open Datatypes +open Maps +open RTL +open Op +open Asmgen +open DebugPrint +open RTLpath +open! Integers + +let reg = ref 1 + +let node = ref 1 + +let r2p () = Camlcoq.P.of_int !reg + +let n2p () = Camlcoq.P.of_int !node + +let r2pi () = + reg := !reg + 1; + r2p () + +let n2pi () = + node := !node + 1; + n2p () + +type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul + +let load_hilo32 a1 dest hi lo succ is_long k = + if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k + else + let r = r2pi () in + Iop (OEluiw (hi, is_long), [ a1 ], r, n2pi ()) + :: Iop (Oaddimm lo, [ r ], dest, succ) :: k + +let load_hilo64 a1 dest hi lo succ k = + if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k + else + let r = r2pi () in + Iop (OEluil hi, [ a1 ], r, n2pi ()) + :: Iop (Oaddlimm lo, [ r ], dest, succ) :: k + +let loadimm32 a1 dest n succ is_long k = + match make_immed32 n with + | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [ a1 ], dest, succ) :: k + | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k + +let loadimm64 a1 dest n succ k = + match make_immed64 n with + | Imm64_single imm -> Iop (OEaddilr0 imm, [ a1 ], dest, succ) :: k + | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k + | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k + +let get_opimm imm = function + | Xoriw -> OExoriw imm + | Sltiw -> OEsltiw imm + | Sltiuw -> OEsltiuw imm + | Xoril -> OExoril imm + | Sltil -> OEsltil imm + | Sltiul -> OEsltiul imm + +let opimm32 a1 dest n succ is_long k op opimm = + match make_immed32 n with + | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k + | Imm32_pair (hi, lo) -> + let r = r2pi () in + load_hilo32 a1 r hi lo (n2pi ()) is_long + (Iop (op, [ a1; r ], dest, succ) :: k) + +let opimm64 a1 dest n succ k op opimm = + match make_immed64 n with + | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k + | Imm64_pair (hi, lo) -> + let r = r2pi () in + load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k) + | Imm64_large imm -> + let r = r2pi () in + Iop (OEloadli imm, [], r, n2pi ()) :: Iop (op, [ a1; r ], dest, succ) :: k + +let xorimm32 a1 dest n succ is_long k = + opimm32 a1 dest n succ is_long k Oxor Xoriw + +let sltimm32 a1 dest n succ is_long k = + opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw + +let sltuimm32 a1 dest n succ is_long k = + opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw + +let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril + +let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil + +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 cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 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 + +let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 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 + +let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 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 + +let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 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 + +let cond_int32s is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k + | Cle -> + let r = r2pi () in + Iop (OEsltw optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k + | Cge -> + let r = r2pi () in + Iop (OEsltw optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + +let cond_int32u is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Iop (OEsequw optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k + | Cle -> + let r = r2pi () in + Iop (OEsltuw optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k + | Cge -> + let r = r2pi () in + Iop (OEsltuw optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + +let cond_int64s is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k + | Cle -> + let r = r2pi () in + Iop (OEsltl optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k + | Cge -> + let r = r2pi () in + Iop (OEsltl optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + +let cond_int64u is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Iop (OEsequl optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k + | Cle -> + let r = r2pi () in + Iop (OEsltul optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k + | Cge -> + let r = r2pi () in + Iop (OEsltul optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + +let is_normal_cmp = function Cne -> false | _ -> true + +let cond_float cmp f1 f2 dest succ = + match cmp with + | Ceq -> Iop (OEfeqd, [ f1; f2 ], dest, succ) + | Cne -> Iop (OEfeqd, [ f1; f2 ], dest, succ) + | Clt -> Iop (OEfltd, [ f1; f2 ], dest, succ) + | Cle -> Iop (OEfled, [ f1; f2 ], dest, succ) + | Cgt -> Iop (OEfltd, [ f2; f1 ], dest, succ) + | Cge -> Iop (OEfled, [ f2; f1 ], dest, succ) + +let cond_single cmp f1 f2 dest succ = + match cmp with + | Ceq -> Iop (OEfeqs, [ f1; f2 ], dest, succ) + | Cne -> Iop (OEfeqs, [ f1; f2 ], dest, succ) + | Clt -> Iop (OEflts, [ f1; f2 ], dest, succ) + | Cle -> Iop (OEfles, [ f1; f2 ], dest, succ) + | Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ) + | Cge -> Iop (OEfles, [ f2; f1 ], dest, succ) + +let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k = + if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k + else + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cbranch_int32s false cmp a1 r info succ1 succ2 k) + +let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k = + if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k + else + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cbranch_int32u false cmp a1 r info succ1 succ2 k) + +let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k = + if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k + else + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) + (cbranch_int64s false cmp a1 r info succ1 succ2 k) + +let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k = + if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k + else + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) + (cbranch_int64u false cmp a1 r info succ1 succ2 k) + +let expanse_condimm_int32s cmp a1 n dest succ k = + if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k + else + match cmp with + | Ceq | Cne -> + let r = r2pi () in + xorimm32 a1 r n (n2pi ()) false (cond_int32s true cmp r r dest succ k) + | Clt -> sltimm32 a1 dest n succ false k + | Cle -> + if Int.eq n (Int.repr Int.max_signed) then + loadimm32 a1 dest Int.one succ false k + else sltimm32 a1 dest (Int.add n Int.one) succ false k + | _ -> + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cond_int32s false cmp a1 r dest succ k) + +let expanse_condimm_int32u cmp a1 n dest succ k = + if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k + else + match cmp with + | Clt -> sltuimm32 a1 dest n succ false k + | _ -> + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cond_int32u false cmp a1 r dest succ k) + +let expanse_condimm_int64s cmp a1 n dest succ k = + if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k + else + match cmp with + | Ceq | Cne -> + let r = r2pi () in + xorimm64 a1 r n (n2pi ()) (cond_int64s true cmp r r dest succ k) + | Clt -> sltimm64 a1 dest n succ k + | Cle -> + if Int64.eq n (Int64.repr Int64.max_signed) then + loadimm32 a1 dest Int.one succ true k + else sltimm64 a1 dest (Int64.add n Int64.one) succ k + | _ -> + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k) + +let expanse_condimm_int64u cmp a1 n dest succ k = + if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k + else + match cmp with + | Clt -> sltuimm64 a1 dest n succ k + | _ -> + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) (cond_int64u false cmp a1 r dest succ k) + +let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = + let normal = is_normal_cmp cmp in + let normal' = if cnot then not normal else normal in + let succ' = if normal' then succ else n2pi () in + let insn = fn_cond cmp f1 f2 dest succ' in + insn + :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) + +let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = + let r = r2pi () in + let normal = is_normal_cmp cmp in + let normal' = if cnot then not normal else normal in + let insn = fn_cond cmp f1 f2 r (n2pi ()) in + insn + :: + (if normal' then Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) + else Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info)) + :: k + +let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] + +let get_regs_inst = function + | Inop _ -> [] + | Iop (_, args, dest, _) -> dest :: args + | Iload (_, _, _, args, dest, _) -> dest :: args + | Istore (_, _, args, src, _) -> src :: args + | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args) + | Itailcall (_, t, args) -> get_regindent t @ args + | Ibuiltin (_, args, dest, _) -> + AST.params_of_builtin_res dest @ AST.params_of_builtin_args args + | Icond (_, args, _, _, _) -> args + | Ijumptable (arg, _) -> [ arg ] + | Ireturn (Some r) -> [ r ] + | _ -> [] + +let write_initial_node initial code' new_order = + code' := PTree.set initial (Inop (n2p ())) !code'; + new_order := initial :: !new_order + +let write_pathmap initial esize pm' = + let path = get_some @@ PTree.get initial !pm' in + let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in + let path' = + { + psize = npsize; + input_regs = path.input_regs; + pre_output_regs = path.pre_output_regs; + output_regs = path.output_regs; + } + in + pm' := PTree.set initial path' !pm' + +let rec write_tree exp current code' new_order = + match exp with + | (Iop (_, _, _, succ) as inst) :: k -> + code' := PTree.set (Camlcoq.P.of_int current) inst !code'; + new_order := Camlcoq.P.of_int current :: !new_order; + write_tree k (current - 1) code' new_order + | (Icond (_, _, succ1, succ2, _) as inst) :: k -> + code' := PTree.set (Camlcoq.P.of_int current) inst !code'; + new_order := Camlcoq.P.of_int current :: !new_order; + write_tree k (current - 1) code' new_order + | [] -> () + | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." + +let expanse (sb : superblock) code pm = + (*debug_flag := true;*) + let new_order = ref [] in + let liveins = ref sb.liveins in + let exp = ref [] in + let was_branch = ref false in + let was_exp = ref false in + let code' = ref code in + let pm' = ref pm in + Array.iter + (fun n -> + was_branch := false; + was_exp := false; + let inst = get_some @@ PTree.get n code in + (match inst with + | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> + debug "Iop/Ccomp\n"; + exp := cond_int32s false c a1 a2 dest succ []; + was_exp := true + | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> + debug "Iop/Ccompu\n"; + exp := cond_int32u false c a1 a2 dest succ []; + was_exp := true + | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> + debug "Iop/Ccompimm\n"; + exp := expanse_condimm_int32s c a1 imm dest succ []; + was_exp := true + | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> + debug "Iop/Ccompuimm\n"; + exp := expanse_condimm_int32u c a1 imm dest succ []; + was_exp := true + | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> + debug "Iop/Ccompl\n"; + exp := cond_int64s false c a1 a2 dest succ []; + was_exp := true + | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> + debug "Iop/Ccomplu\n"; + exp := cond_int64u false c a1 a2 dest succ []; + was_exp := true + | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> + debug "Iop/Ccomplimm\n"; + exp := expanse_condimm_int64s c a1 imm dest succ []; + was_exp := true + | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> + debug "Iop/Ccompluimm\n"; + exp := expanse_condimm_int64u c a1 imm dest succ []; + was_exp := true + | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> + debug "Iop/Ccompf\n"; + exp := expanse_cond_fp false cond_float c f1 f2 dest succ []; + was_exp := true + | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> + debug "Iop/Cnotcompf\n"; + exp := expanse_cond_fp true cond_float c f1 f2 dest succ []; + was_exp := true + | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> + debug "Iop/Ccompfs\n"; + exp := expanse_cond_fp false cond_single c f1 f2 dest succ []; + was_exp := true + | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> + debug "Iop/Cnotcompfs\n"; + exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; + was_exp := true + | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccomp\n"; + exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompu\n"; + exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompimm\n"; + exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompuimm\n"; + exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompl\n"; + exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccomplu\n"; + exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccomplimm\n"; + exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompluimm\n"; + exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompf\n"; + exp := expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Cnotcompf\n"; + exp := expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompfs\n"; + exp := + expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Cnotcompfs\n"; + exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | _ -> new_order := n :: !new_order); + if !was_exp then ( + node := !node + 1; + (if !was_branch then + let lives = PTree.get n !liveins in + match lives with + | Some lives -> + let new_branch_pc = + Camlcoq.P.of_int (!node - (List.length !exp - 1)) + in + liveins := PTree.set new_branch_pc lives !liveins; + liveins := PTree.remove n !liveins + | _ -> ()); + write_pathmap sb.instructions.(0) (List.length !exp) pm'; + write_initial_node n code' new_order; + write_tree !exp !node code' new_order)) + sb.instructions; + sb.instructions <- Array.of_list (List.rev !new_order); + sb.liveins <- !liveins; + (*debug_flag := false;*) + (!code', !pm') + +let rec find_last_node_reg = function + | [] -> () + | (pc, i) :: k -> + let rec traverse_list var = function + | [] -> () + | e :: t -> + let e' = Camlcoq.P.to_int e in + if e' > !var then var := e'; + traverse_list var t + in + traverse_list node [ pc ]; + traverse_list reg (get_regs_inst i); + find_last_node_reg k diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 9e1ad004..4b309f5b 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -87,6 +87,35 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c + | OEseqw _ => op2 (default nv) + | OEsnew _ => op2 (default nv) + | OEsequw _ => op2 (default nv) + | OEsneuw _ => op2 (default nv) + | OEsltw _ => op2 (default nv) + | OEsltuw _ => op2 (default nv) + | OEsltiw _ => op1 (default nv) + | OEsltiuw _ => op1 (default nv) + | OExoriw _ => op1 (bitwise nv) + | OEluiw _ _ => op1 (default nv) + | OEaddiwr0 _ _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEseql _ => op2 (default nv) + | OEsnel _ => op2 (default nv) + | OEsequl _ => op2 (default nv) + | OEsneul _ => op2 (default nv) + | OEsltl _ => op2 (default nv) + | OEsltul _ => op2 (default nv) + | OEsltil _ => op1 (default nv) + | OEsltiul _ => op1 (default nv) + | OExoril _ => op1 (default nv) + | OEluil _ => op1 (default nv) + | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEloadli _ => op1 (default nv) + | OEfeqd => op2 (default nv) + | OEfltd => op2 (default nv) + | OEfled => op2 (default nv) + | OEfeqs => op2 (default nv) + | OEflts => op2 (default nv) + | OEfles => op2 (default nv) | Obits_of_single => op1 (default nv) | Obits_of_float => op1 (default nv) | Osingle_of_bits => op1 (default nv) @@ -159,6 +188,7 @@ Proof. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. +- apply xor_sound; auto with na. - (* selectl *) unfold ExtValues.select01_long. destruct v0; auto with na. @@ -50,7 +50,24 @@ Inductive condition : Type := | Ccompf (c: comparison) (**r 64-bit floating-point comparison *) | Cnotcompf (c: comparison) (**r negation of a floating-point comparison *) | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) - | Cnotcompfs (c: comparison). (**r negation of a 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 *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -153,6 +170,37 @@ Inductive operation : Type := | Osingleoflong (**r [rd = float32_of_signed_long(r1)] *) | Osingleoflongu (**r [rd = float32_of_unsigned_int(r1)] *) (*c Boolean tests: *) + | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + (* Expansed conditions *) + | 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 *) + | OEsltiw (n: int) (**r set-less-than immediate *) + | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) + | OExoriw (n: int) (**r xor immediate *) + | OEluiw (n: int) (is_long: bool) (**r load upper-immediate *) + | OEaddiwr0 (n: int) (is_long: bool) (**r add 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 *) + | OEsltil (n: int64) (**r set-less-than immediate *) + | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) + | OExoril (n: int64) (**r xor immediate *) + | OEluil (n: int64) (**r load upper-immediate *) + | OEaddilr0 (n: int64) (**r add immediate *) + | OEloadli (n: int64) (**r load an immediate int64 *) + | OEfeqd (**r compare equal *) + | OEfltd (**r compare less-than *) + | OEfled (**r compare less-than/equal *) + | OEfeqs (**r compare equal *) + | OEflts (**r compare less-than *) + | OEfles. (**r compare less-than/equal *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) | Obits_of_single | Obits_of_float @@ -172,9 +220,10 @@ Inductive addressing: Type := Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec; intro. + generalize Int.eq_dec Int64.eq_dec bool_dec; intros. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. decide equality. + all: destruct optR0, optR1; decide equality. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. @@ -185,8 +234,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; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros. decide equality. + all: destruct optR0, optR1; decide equality. Defined. (* Alternate definition: @@ -209,6 +259,34 @@ Global Opaque eq_condition eq_addressing eq_operation. to lists of values. Return [None] when the computation can trigger an error, e.g. integer division by zero. [eval_condition] returns a boolean, [eval_operation] and [eval_addressing] return a value. *) + +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 + | None => sem v1 v2 + | Some true => sem vz v1 + | Some false => sem v1 vz + end. + +Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val := + if negb is_long then + match v1 with + | Vint _ => sem vimm vz + | _ => Vundef + end + else + match v1 with + | Vlong _ => sem vimm vz + | _ => Vundef + end. + +Definition may_undef_luil (v1: val) (n: int64): val := + match v1 with + | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) + | _ => Vundef + end. Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with @@ -224,6 +302,23 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | 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 | _, _ => None end. @@ -328,6 +423,36 @@ Definition eval_operation | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1) | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) + (* Expansed conditions *) + | 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) + | 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)) + | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12))) + | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32) + | 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)) + | 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)) + | OEluil n, v1::nil => Some (may_undef_luil v1 n) + | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64) + | OEloadli n, nil => Some (Vlong n) + | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) + | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) + | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2) + | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2) + | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2) + | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2) | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong) | _, _ => None end. @@ -388,6 +513,22 @@ Definition type_of_condition (c: condition) : list typ := | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil | Cnotcompfs _ => Tsingle :: Tsingle :: nil + | CEbeqw _ => Tint :: Tint :: nil + | CEbnew _ => Tint :: Tint :: nil + | CEbequw _ => Tint :: Tint :: nil + | CEbneuw _ => Tint :: Tint :: nil + | CEbltw _ => Tint :: Tint :: nil + | CEbltuw _ => Tint :: Tint :: nil + | CEbgew _ => Tint :: Tint :: nil + | CEbgeuw _ => Tint :: Tint :: nil + | CEbeql _ => Tlong :: Tlong :: nil + | CEbnel _ => Tlong :: Tlong :: nil + | CEbequl _ => Tlong :: Tlong :: nil + | CEbneul _ => Tlong :: Tlong :: nil + | CEbltl _ => Tlong :: Tlong :: nil + | CEbltul _ => Tlong :: Tlong :: nil + | CEbgel _ => Tlong :: Tlong :: nil + | CEbgeul _ => Tlong :: Tlong :: nil end. Definition type_of_operation (op: operation) : list typ * typ := @@ -485,6 +626,35 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) + | OEseqw _ => (Tint :: Tint :: nil, Tint) + | OEsnew _ => (Tint :: Tint :: nil, Tint) + | OEsequw _ => (Tint :: Tint :: nil, Tint) + | OEsneuw _ => (Tint :: Tint :: nil, Tint) + | OEsltw _ => (Tint :: Tint :: nil, Tint) + | OEsltuw _ => (Tint :: Tint :: nil, Tint) + | OEsltiw _ => (Tint :: nil, Tint) + | OEsltiuw _ => (Tint :: nil, Tint) + | OExoriw _ => (Tint :: nil, Tint) + | OEluiw _ _ => (Tint :: nil, Tint) + | OEaddiwr0 _ _ => (Tint :: nil, Tint) + | OEseql _ => (Tlong :: Tlong :: nil, Tint) + | OEsnel _ => (Tlong :: Tlong :: nil, Tint) + | OEsequl _ => (Tlong :: Tlong :: nil, Tint) + | OEsneul _ => (Tlong :: Tlong :: nil, Tint) + | OEsltl _ => (Tlong :: Tlong :: nil, Tint) + | OEsltul _ => (Tlong :: Tlong :: nil, Tint) + | OEsltil _ => (Tlong :: nil, Tint) + | OEsltiul _ => (Tlong :: nil, Tint) + | OExoril _ => (Tlong :: nil, Tlong) + | OEluil _ => (Tlong :: nil, Tlong) + | OEaddilr0 _ => (Tlong :: nil, Tlong) + | OEloadli _ => (nil, Tlong) + | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) + | OEfltd => (Tfloat :: Tfloat :: nil, Tint) + | OEfled => (Tfloat :: Tfloat :: nil, Tint) + | OEfeqs => (Tsingle :: Tsingle :: nil, Tint) + | OEflts => (Tsingle :: Tsingle :: nil, Tint) + | OEfles => (Tsingle :: Tsingle :: nil, Tint) | Obits_of_single => (Tsingle :: nil, Tint) | Obits_of_float => (Tfloat :: nil, Tlong) | Osingle_of_bits => (Tint :: nil, Tsingle) @@ -696,6 +866,86 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... + (* OEseqw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsequw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsneuw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsltw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsltuw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsltiw *) + - unfold Val.cmp; destruct Val.cmp_bool... + all: destruct b... + (* OEsltiuw *) + - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... + (* OExoriw *) + - destruct v0... + (* OEluiw *) + - unfold may_undef_int; + destruct v0, is_long; simpl; trivial; + destruct (Int.ltu _ _); cbn; trivial. + (* OEaddiwr0 *) + - destruct v0, is_long; simpl; trivial. + (* OEseql *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsequl *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsneul *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsltl *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsltul *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsltil *) + - unfold Val.cmpl; destruct Val.cmpl_bool... + all: destruct b... + (* OEsltiul *) + - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... + (* OExoril *) + - destruct v0... + (* OEluil *) + - destruct v0; simpl; trivial. + (* OEaddilr0 *) + - destruct v0; simpl; trivial. + (* OEloadli *) + - trivial. + (* OEfeqd *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfltd *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfled *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfeqs *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. + (* OEflts *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. + (* OEfles *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. (* Bits_of_single, float *) - destruct v0; cbn; trivial. - destruct v0; cbn; trivial. @@ -777,6 +1027,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 end. Lemma eval_negate_condition: @@ -796,6 +1062,39 @@ Proof. repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto. 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 [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) @@ -892,12 +1191,28 @@ Definition cond_depends_on_memory (cond : condition) : bool := | Ccompuimm _ _ => negb Archi.ptr64 | Ccomplu _ => Archi.ptr64 | Ccompluimm _ _ => Archi.ptr64 + | CEbequw _ => negb Archi.ptr64 + | CEbneuw _ => negb Archi.ptr64 + | CEbltuw _ => negb Archi.ptr64 + | CEbgeuw _ => negb Archi.ptr64 + | CEbequl _ => Archi.ptr64 + | CEbneul _ => Archi.ptr64 + | CEbltul _ => Archi.ptr64 + | CEbgeul _ => Archi.ptr64 | _ => false end. Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp cmp => cond_depends_on_memory cmp + | OEsequw _ => negb Archi.ptr64 + | OEsneuw _ => negb Archi.ptr64 + | OEsltiuw _ => negb Archi.ptr64 + | OEsltuw _ => negb Archi.ptr64 + | OEsequl _ => Archi.ptr64 + | OEsneul _ => Archi.ptr64 + | OEsltul _ => Archi.ptr64 + | OEsltiul _ => Archi.ptr64 | _ => false end. @@ -921,6 +1236,11 @@ Proof. intros until m2. destruct op; simpl; try congruence. intro DEPEND. 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; + destruct v; try destruct v0; simpl; auto; + try apply negb_false_iff in H; try rewrite H; auto. Qed. Lemma cond_valid_pointer_eq: @@ -930,7 +1250,9 @@ 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); - erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + try destruct optR0 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. Lemma op_valid_pointer_eq: @@ -939,8 +1261,11 @@ Lemma op_valid_pointer_eq: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. - intros MEM; destruct cond; repeat (destruct args; simpl; try congruence); - erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + 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; + unfold Val.cmpu, Val.cmplu; + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -1047,6 +1372,88 @@ Ltac InvInject := | _ => idtac end. +Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0', + Val.inject f v v' -> + Val.inject f v0 v0' -> + Val.cmpu_bool (Mem.valid_pointer m1) c v v0 = Some b -> + Val.cmpu_bool (Mem.valid_pointer m2) c v' v0' = Some b. +Proof. + intros. + eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +Qed. + +Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0, + Val.inject f v v' -> + Val.inject f v0 v'0 -> + Val.inject f (Val.cmpu (Mem.valid_pointer m1) c v v0) + (Val.cmpu (Mem.valid_pointer m2) c v' v'0). +Proof. + intros until v'0. intros HV1 HV2. + unfold Val.cmpu; + destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto. + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. +Qed. + +Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR0, + 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). +Proof. + intros until optR0. intros HV1 HV2. + destruct optR0 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. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. +Qed. + +Lemma eval_cmplu_bool_inj': forall b c v v' v0 v0', + Val.inject f v v' -> + Val.inject f v0 v0' -> + Val.cmplu_bool (Mem.valid_pointer m1) c v v0 = Some b -> + Val.cmplu_bool (Mem.valid_pointer m2) c v' v0' = Some b. +Proof. + intros. + eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +Qed. + +Lemma eval_cmplu_bool_inj: forall c v v' v0 v'0, + Val.inject f v v' -> + Val.inject f v0 v'0 -> + Val.inject f (Val.maketotal (Val.cmplu (Mem.valid_pointer m1) c v v0)) + (Val.maketotal (Val.cmplu (Mem.valid_pointer m2) c v' v'0)). +Proof. + intros until v'0. intros HV1 HV2. + unfold Val.cmplu; + destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto. + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. +Qed. + +Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR0, + 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)). +Proof. + intros until optR0. intros HV1 HV2. + destruct optR0 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. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. +Qed. + Lemma eval_condition_inj: forall cond vl1 vl2 b, Val.inject_list f vl1 vl2 -> @@ -1054,6 +1461,9 @@ Lemma eval_condition_inj: eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. + all: assert (HVI32: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int; + assert (HVI64: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long; + try unfold zero32, zero64. - inv H3; inv H2; simpl in H0; inv H0; auto. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. - inv H3; simpl in H0; inv H0; auto. @@ -1066,6 +1476,38 @@ 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 *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. Qed. Ltac TrivialExists := @@ -1274,6 +1716,86 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + (* OEseqw *) + - destruct optR0 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; + inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequw *) + - apply eval_cmpu_bool_inj_opt; auto. + (* OEsneuw *) + - apply eval_cmpu_bool_inj_opt; auto. + (* OEsltw *) + - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsltuw *) + - apply eval_cmpu_bool_inj_opt; auto. + (* OEsltiw *) + - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int. + (* OEsltiuw *) + - apply eval_cmpu_bool_inj; auto. + (* OExoriw *) + - inv H4; simpl; auto. + (* OEluiw *) + - unfold may_undef_int; + destruct is_long; + inv H4; simpl; auto; + destruct (Int.ltu _ _); auto. + (* OEaddiwr0 *) + - unfold may_undef_int; + destruct is_long; + inv H4; simpl; auto. + (* OEseql *) + - destruct optR0 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; + inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequl *) + - apply eval_cmplu_bool_inj_opt; auto. + (* OEsneul *) + - apply eval_cmplu_bool_inj_opt; auto. + (* OEsltl *) + - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsltul *) + - apply eval_cmplu_bool_inj_opt; auto. + (* OEsltil *) + - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. + (* OEsltiul *) + - apply eval_cmplu_bool_inj; auto. + (* OExoril *) + - inv H4; simpl; auto. + (* OEluil *) + - inv H4; simpl; auto. + (* OEaddilr0 *) + - unfold may_undef_int; + inv H4; simpl; auto. + (* OEfeqd *) + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfltd *) + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfled *) + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfeqs *) + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEflts *) + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfles *) + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. (* Bits_of_single, double *) - inv H4; simpl; auto. - inv H4; simpl; auto. @@ -1542,4 +2064,4 @@ Definition builtin_arg_ok match ba with | (BA _ | BA_splitlong (BA _) (BA _)) => true | _ => builtin_arg_ok_1 ba c - end. + end. diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 2b0496fc..35ae81e6 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -56,7 +56,23 @@ module Rocket = | Ccompl _ | Ccomplu _ | Ccomplimm _ - | Ccompluimm _ -> 1 + | Ccompluimm _ + | CEbeqw _ + | CEbnew _ + | CEbequw _ + | CEbneuw _ + | CEbltw _ + | CEbltuw _ + | CEbgew _ + | CEbgeuw _ + | CEbeql _ + | CEbnel _ + | CEbequl _ + | CEbneul _ + | CEbltl _ + | CEbltul _ + | CEbgel _ + | CEbgeul _ -> 1 | Ccompf _ | Cnotcompf _ -> 6 | Ccompfs _ diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 7e78283e..84380251 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -30,6 +30,11 @@ let comparison_name = function | Cgt -> ">" | Cge -> ">=" +let get_optR0_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 print_condition reg pp = function | (Ccomp c, [r1;r2]) -> fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2 @@ -55,6 +60,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) | _ -> fprintf pp "<bad condition>" @@ -156,6 +193,35 @@ let print_operation reg pp = function | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1 | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) + | 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) + | 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) + | OEluiw (n, _), _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) + | OEaddiwr0 (n, _), _ -> fprintf pp "OEaddiwr0(%ld,X0)" (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) + | 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) + | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) + | OEaddilr0 n, _ -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n) + | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n) + | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 + | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 + | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 + | OEfeqs, [r1;r2] -> fprintf pp "OEfeqs(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 + | OEflts, [r1;r2] -> fprintf pp "OEflts(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 + | OEfles, [r1;r2] -> fprintf pp "OEfles(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 | Obits_of_single, [r1] -> fprintf pp "bits_of_single(%a)" reg r1 | Obits_of_float, [r1] -> fprintf pp "bits_of_float(%a)" reg r1 | Osingle_of_bits, [r1] -> fprintf pp "single_of_bits(%a)" reg r1 diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v new file mode 100644 index 00000000..6a0297e9 --- /dev/null +++ b/riscV/RTLpathSE_simplify.v @@ -0,0 +1,1323 @@ +Require Import Coqlib Floats Values Memory. +Require Import Integers. +Require Import Op Registers. +Require Import RTLpathSE_theory. +Require Import RTLpathSE_simu_specs. +Require Import Asmgen Asmgenproof1. +Require Import Lia. + +(** Useful functions for conditions/branches expansion *) + +Definition is_inv_cmp_int (cmp: comparison) : bool := + match cmp with | Cle | Cgt => true | _ => false end. + +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. + +(** Functions to manage lists of "fake" values *) + +Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval := + let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in + let lhsv := fScons hvfirst fSnil in + fScons hvsec lhsv. + +Definition make_lhsv_single (hvs: hsval) : list_hsval := + fScons hvs fSnil. + +(** Expansion functions *) + +(* Immediate loads *) + +Definition load_hilo32 (hv1: hsval) (hi lo: int) (is_long: bool) := + let hl := make_lhsv_single hv1 in + if Int.eq lo Int.zero then + fSop (OEluiw hi is_long) hl + else + let hvs := fSop (OEluiw hi is_long) hl in + let hl' := make_lhsv_single hvs in + fSop (Oaddimm lo) hl'. + +Definition load_hilo64 (hv1: hsval) (hi lo: int64) := + let hl := make_lhsv_single hv1 in + if Int64.eq lo Int64.zero then + fSop (OEluil hi) hl + else + let hvs := fSop (OEluil hi) hl in + let hl := make_lhsv_single hvs in + fSop (Oaddlimm lo) hl. + +Definition loadimm32 (hv1: hsval) (n: int) (is_long: bool) := + match make_immed32 n with + | Imm32_single imm => + let hl := make_lhsv_single hv1 in + fSop (OEaddiwr0 imm is_long) hl + | Imm32_pair hi lo => load_hilo32 hv1 hi lo is_long + end. + +Definition loadimm64 (hv1: hsval) (n: int64) := + match make_immed64 n with + | Imm64_single imm => + let hl := make_lhsv_single hv1 in + fSop (OEaddilr0 imm) hl + | Imm64_pair hi lo => load_hilo64 hv1 hi lo + | Imm64_large imm => fSop (OEloadli imm) fSnil + end. + +Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) (is_long: bool) := + match make_immed32 n with + | Imm32_single imm => + let hl := make_lhsv_single hv1 in + fSop (opimm imm) hl + | Imm32_pair hi lo => + let hvs := load_hilo32 hv1 hi lo is_long in + let hl := make_lhsv_cmp false hv1 hvs in + fSop op hl + end. + +Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) := + match make_immed64 n with + | Imm64_single imm => + let hl := make_lhsv_single hv1 in + fSop (opimm imm) hl + | Imm64_pair hi lo => + let hvs := load_hilo64 hv1 hi lo in + let hl := make_lhsv_cmp false hv1 hvs in + fSop op hl + | Imm64_large imm => + let hvs := fSop (OEloadli imm) fSnil in + let hl := make_lhsv_cmp false hv1 hvs in + fSop op hl + end. + +Definition xorimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n Oxor OExoriw is_long. +Definition sltimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltw None) OEsltiw is_long. +Definition sltuimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltuw None) OEsltiuw is_long. +Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril. +Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. +Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. + +(* Comparisons intructions *) + +Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := + match cmp with + | Ceq => fSop (OEseqw optR0) lhsv + | Cne => fSop (OEsnew optR0) lhsv + | Clt | Cgt => fSop (OEsltw optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltw optR0) 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) := + match cmp with + | Ceq => fSop (OEsequw optR0) lhsv + | Cne => fSop (OEsneuw optR0) lhsv + | Clt | Cgt => fSop (OEsltuw optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltuw optR0) 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) := + match cmp with + | Ceq => fSop (OEseql optR0) lhsv + | Cne => fSop (OEsnel optR0) lhsv + | Clt | Cgt => fSop (OEsltl optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltl optR0) 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) := + match cmp with + | Ceq => fSop (OEsequl optR0) lhsv + | Cne => fSop (OEsneul optR0) lhsv + | Clt | Cgt => fSop (OEsltul optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltul optR0) lhsv) in + let hl := make_lhsv_single hvs in + fSop (OExoriw Int.one) hl + end. + +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 hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int32s cmp hl optR0 + else + match cmp with + | Ceq | Cne => + let optR0 := make_optR0 true is_inv in + let hvs := xorimm32 hv1 n false in + let hl := make_lhsv_cmp false hvs hvs in + cond_int32s cmp hl optR0 + | Clt => sltimm32 hv1 n false + | Cle => + if Int.eq n (Int.repr Int.max_signed) then + loadimm32 hv1 Int.one false + else sltimm32 hv1 (Int.add n Int.one) false + | _ => + let optR0 := make_optR0 false is_inv in + let hvs := loadimm32 hv1 n false in + let hl := make_lhsv_cmp is_inv hv1 hvs in + cond_int32s cmp hl optR0 + 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 hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int32u cmp hl optR0 + else + match cmp with + | Clt => sltuimm32 hv1 n false + | _ => + let optR0 := make_optR0 false is_inv in + let hvs := loadimm32 hv1 n false in + let hl := make_lhsv_cmp is_inv hv1 hvs in + cond_int32u cmp hl optR0 + 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 hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int64s cmp hl optR0 + else + match cmp with + | Ceq | Cne => + let optR0 := make_optR0 true is_inv in + let hvs := xorimm64 hv1 n in + let hl := make_lhsv_cmp false hvs hvs in + cond_int64s cmp hl optR0 + | Clt => sltimm64 hv1 n + | Cle => + if Int64.eq n (Int64.repr Int64.max_signed) then + loadimm32 hv1 Int.one true + else sltimm64 hv1 (Int64.add n Int64.one) + | _ => + let optR0 := make_optR0 false is_inv in + let hvs := loadimm64 hv1 n in + let hl := make_lhsv_cmp is_inv hv1 hvs in + cond_int64s cmp hl optR0 + 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 hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int64u cmp hl optR0 + else + match cmp with + | Clt => sltuimm64 hv1 n + | _ => + let optR0 := make_optR0 false is_inv in + let hvs := loadimm64 hv1 n in + let hl := make_lhsv_cmp is_inv hv1 hvs in + cond_int64u cmp hl optR0 + end. + +Definition cond_float (cmp: comparison) (lhsv: list_hsval) := + match cmp with + | Ceq | Cne => fSop OEfeqd lhsv + | Clt | Cgt => fSop OEfltd lhsv + | Cle | Cge => fSop OEfled lhsv + end. + +Definition cond_single (cmp: comparison) (lhsv: list_hsval) := + match cmp with + | Ceq | Cne => fSop OEfeqs lhsv + | Clt | Cgt => fSop OEflts lhsv + | Cle | Cge => fSop OEfles lhsv + end. + +Definition is_normal_cmp cmp := + match cmp with | Cne => false | _ => true end. + +Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) := + let normal := is_normal_cmp cmp in + let normal' := if cnot then negb normal else normal in + let hvs := fn_cond cmp lhsv in + let hl := make_lhsv_single hvs in + if normal' then hvs else fSop (OExoriw Int.one) hl. + +(* Branches instructions *) + +Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeqw optR0 + | Cne => CEbnew optR0 + | Clt => CEbltw optR0 + | Cle => CEbgew optR0 + | Cgt => CEbltw optR0 + | Cge => CEbgew optR0 + end. + +Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbequw optR0 + | Cne => CEbneuw optR0 + | Clt => CEbltuw optR0 + | Cle => CEbgeuw optR0 + | Cgt => CEbltuw optR0 + | Cge => CEbgeuw optR0 + end. + +Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeql optR0 + | Cne => CEbnel optR0 + | Clt => CEbltl optR0 + | Cle => CEbgel optR0 + | Cgt => CEbltl optR0 + | Cge => CEbgel optR0 + end. + +Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbequl optR0 + | Cne => CEbneul optR0 + | Clt => CEbltul optR0 + | Cle => CEbgeul optR0 + | Cgt => CEbltul optR0 + | Cge => CEbgeul optR0 + end. + +Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (condition * list_hsval) := + let normal := is_normal_cmp cmp in + 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). + +(** Target op simplifications using "fake" values *) + +Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := + match op, lr with + | Ocmp (Ccomp 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 lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (cond_int32s c lhsv optR0) + | 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 lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (cond_int32u c lhsv optR0) + | Ocmp (Ccompimm c imm), a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int32s c hv1 imm) + | Ocmp (Ccompuimm c imm), a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int32u c hv1 imm) + | Ocmp (Ccompl 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 lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (cond_int64s c lhsv optR0) + | 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 lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (cond_int64u c lhsv optR0) + | Ocmp (Ccomplimm c imm), a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int64s c hv1 imm) + | Ocmp (Ccompluimm c imm), a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int64u c hv1 imm) + | Ocmp (Ccompf c), f1 :: f2 :: nil => + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp false cond_float c lhsv) + | Ocmp (Cnotcompf c), f1 :: f2 :: nil => + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp true cond_float c lhsv) + | Ocmp (Ccompfs c), f1 :: f2 :: nil => + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp false cond_single c lhsv) + | Ocmp (Cnotcompfs c), f1 :: f2 :: nil => + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp true cond_single c lhsv) + | _, _ => None + end. + +Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) := + 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 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 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) + | (Ccompimm 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_int32s c (make_optR0 true is_inv) in + Some (cond, lhsv) + else + let hvs := loadimm32 hv1 n false in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int32s c (make_optR0 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 + Some (cond, lhsv) + else + let hvs := loadimm32 hv1 n false in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int32u c (make_optR0 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 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 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) + | (Ccomplimm 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_int64s c (make_optR0 true is_inv) in + Some (cond, lhsv) + else + let hvs := loadimm64 hv1 n in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int64s c (make_optR0 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 + Some (cond, lhsv) + else + let hvs := loadimm64 hv1 n in + let lhsv := make_lhsv_cmp is_inv hv1 hvs in + let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in + Some (cond, lhsv)) + | (Ccompf c), (f1 :: f2 :: nil) => + let hv1 := fsi_sreg_get prev f1 in + let hv2 := fsi_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cbranch_fp false cond_float c lhsv) + | (Cnotcompf c), (f1 :: f2 :: nil) => + let hv1 := fsi_sreg_get prev f1 in + let hv2 := fsi_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cbranch_fp true cond_float c lhsv) + | (Ccompfs c), (f1 :: f2 :: nil) => + let hv1 := fsi_sreg_get prev f1 in + let hv2 := fsi_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cbranch_fp false cond_single c lhsv) + | (Cnotcompfs c), (f1 :: f2 :: nil) => + let hv1 := fsi_sreg_get prev f1 in + let hv2 := fsi_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cbranch_fp true cond_single c lhsv) + | _, _ => None + end. + +(** Auxiliary lemmas on comparisons *) + +(* Signed ints *) + +Lemma xor_neg_ltle_cmp: forall v1 v2, + Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + unfold Val.cmp; simpl; + try rewrite Int.eq_sym; + try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl; + try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; + auto. +Qed. + +(* Unsigned ints *) + +Lemma xor_neg_ltle_cmpu: forall mptr v1 v2, + Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + unfold Val.cmpu; simpl; + try rewrite Int.eq_sym; + try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl; + try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; + auto. + 1,2: + unfold Val.cmpu, Val.cmpu_bool; + destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _); + try destruct (eq_block _ _); auto. + unfold Val.cmpu, Val.cmpu_bool; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. + +Remark ltu_12_wordsize: + Int.ltu (Int.repr 12) Int.iwordsize = true. +Proof. + unfold Int.iwordsize, Int.zwordsize. simpl. + unfold Int.ltu. apply zlt_true. + rewrite !Int.unsigned_repr; try cbn; try omega. +Qed. + +(* Signed longs *) + +Lemma xor_neg_ltle_cmpl: forall v1 v2, + Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.lt _ _); auto. +Qed. + +Lemma xor_neg_ltge_cmpl: forall v1 v2, + Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.lt _ _); auto. +Qed. + +Lemma xorl_zero_eq_cmpl: forall c v1 v2, + c = Ceq \/ c = Cne -> + Some + (Val.maketotal + (option_map Val.of_bool + (Val.cmpl_bool c (Val.xorl v1 v2) (Vlong Int64.zero)))) = + Some (Val.of_optbool (Val.cmpl_bool c v1 v2)). +Proof. + intros. destruct c; inv H; try discriminate; + destruct v1, v2; simpl; auto; + destruct (Int64.eq i i0) eqn:EQ0. + 1,3: + apply Int64.same_if_eq in EQ0; subst; + rewrite Int64.xor_idem; + rewrite Int64.eq_true; trivial. + 1,2: + destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence; + rewrite Int64.xor_is_zero in EQ1; congruence. +Qed. + +Lemma cmp_ltle_add_one: forall v n, + Int.eq n (Int.repr Int.max_signed) = false -> + Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) = + Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))). +Proof. + intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto. + unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). + destruct (zlt (Int.signed n) (Int.signed i)). + rewrite zlt_false by omega. auto. + rewrite zlt_true by omega. auto. + rewrite Int.add_signed. symmetry; apply Int.signed_repr. + specialize (Int.eq_spec n (Int.repr Int.max_signed)). + rewrite EQMAX; simpl; intros. + assert (Int.signed n <> Int.max_signed). + { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. } + generalize (Int.signed_range n); omega. +Qed. + +Lemma cmpl_ltle_add_one: forall v n, + Int64.eq n (Int64.repr Int64.max_signed) = false -> + Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) = + Some (Val.of_optbool (Val.cmpl_bool Cle v (Vlong n))). +Proof. + intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto. + unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). + destruct (zlt (Int64.signed n) (Int64.signed i)). + rewrite zlt_false by omega. auto. + rewrite zlt_true by omega. auto. + rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. + specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)). + rewrite EQMAX; simpl; intros. + assert (Int64.signed n <> Int64.max_signed). + { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. } + generalize (Int64.signed_range n); omega. +Qed. + +Remark lt_maxsgn_false_int: forall i, + Int.lt (Int.repr Int.max_signed) i = false. +Proof. + intros; unfold Int.lt. + specialize Int.signed_range with i; intros. + rewrite zlt_false; auto. destruct H. + rewrite Int.signed_repr; try (cbn; lia). + apply Z.le_ge. trivial. +Qed. + +Remark lt_maxsgn_false_long: forall i, + Int64.lt (Int64.repr Int64.max_signed) i = false. +Proof. + intros; unfold Int64.lt. + specialize Int64.signed_range with i; intros. + rewrite zlt_false; auto. destruct H. + rewrite Int64.signed_repr; try (cbn; lia). + apply Z.le_ge. trivial. +Qed. + +(* Unsigned longs *) + +Lemma xor_neg_ltle_cmplu: forall mptr v1 v2, + Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.ltu _ _); auto. + 1,2: unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. + unfold Val.cmplu; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. + +Lemma xor_neg_ltge_cmplu: forall mptr v1 v2, + Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.ltu _ _); auto. + 1,2: unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. + unfold Val.cmplu; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. + +(* Floats *) + +Lemma xor_neg_eqne_cmpf: forall v1 v2, + Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence; + unfold Val.cmpf; simpl. + rewrite Float.cmp_ne_eq. + destruct (Float.cmp _ _ _); simpl; auto. +Qed. + +(* Singles *) + +Lemma xor_neg_eqne_cmpfs: forall v1 v2, + Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence; + unfold Val.cmpfs; simpl. + rewrite Float32.cmp_ne_eq. + destruct (Float32.cmp _ _ _); simpl; auto. +Qed. + +(* More useful lemmas *) + +Lemma xor_neg_optb: forall v, + Some (Val.xor (Val.of_optbool (option_map negb v)) + (Vint Int.one)) = Some (Val.of_optbool v). +Proof. + intros. + destruct v; simpl; trivial. + destruct b; simpl; auto. +Qed. + +Lemma xor_neg_optb': forall v, + Some (Val.xor (Val.of_optbool v) (Vint Int.one)) = + Some (Val.of_optbool (option_map negb v)). +Proof. + intros. + destruct v; simpl; trivial. + destruct b; simpl; auto. +Qed. + +Lemma optbool_mktotal: forall v, + Val.maketotal (option_map Val.of_bool v) = + Val.of_optbool v. +Proof. + intros. + destruct v; simpl; auto. +Qed. + +(* TODO gourdinl move to common/Values ? *) +Theorem swap_cmpf_bool: + forall c x y, + Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto. +Qed. + +Theorem swap_cmpfs_bool: + forall c x y, + Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. +Qed. + +(* Intermediates lemmas on each expansed instruction *) + +Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (cond_int32s c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmp_bool c v v0)). +Proof. + intros. + unfold cond_int32s in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmp. + - apply xor_neg_ltle_cmp. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmp_bool; trivial. + - replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmp_bool. + rewrite xor_neg_optb; trivial. +Qed. + +Lemma simplify_ccompu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj + (cond_int32u c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v v0)). +Proof. + intros. + erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)). + 2: eauto. + unfold cond_int32u in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpu. + - apply xor_neg_ltle_cmpu. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmpu_bool; trivial. + - replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmpu_bool. + rewrite xor_neg_optb; trivial. +Qed. + +Lemma simplify_ccompimm_correct ge sp hst st c r n rs0 m m0 v: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj (expanse_condimm_int32s c (fsi_sreg_get hst r) n)) rs0 m0 = + Some (Val.of_optbool (Val.cmp_bool c v (Vint n))). +Proof. + intros. + unfold expanse_condimm_int32s, cond_int32s in *; destruct c; + intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; + try apply Int.same_if_eq in EQIMM; subst; + unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + unfold Val.cmp, zero32. + all: + try apply xor_neg_ltle_cmp; + try apply xor_neg_ltge_cmp; trivial. + 4: + try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; subst; + try apply Int.same_if_eq in EQMAX; subst; simpl. + 4: + intros; try (specialize make_immed32_sound with (Int.one); + destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. + 6: + intros; try (specialize make_immed32_sound with (Int.add n Int.one); + destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2); intros; simpl. + 1,2,3,8,9: + intros; try (specialize make_immed32_sound with (n); + destruct (make_immed32 n) eqn:EQMKI); intros; simpl. + all: + try destruct (Int.eq lo Int.zero) eqn:EQLO32; + try apply Int.same_if_eq in EQLO32; subst; + try erewrite fSop_correct; eauto; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + try rewrite OK2; + try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; + try rewrite xor_neg_ltle_cmp; trivial; + unfold Val.cmp, may_undef_int, zero32, Val.add; simpl; + destruct v; auto. + all: + try rewrite ltu_12_wordsize; + try rewrite <- H; + try (apply cmp_ltle_add_one; auto); + try rewrite Int.add_commut, Int.add_zero_l in *; + try ( + simpl; trivial; + try rewrite Int.xor_is_zero; + try destruct (Int.lt _ _) eqn:EQLT; trivial; + try rewrite lt_maxsgn_false_int in EQLT; + simpl; trivial; try discriminate; fail). +Qed. + +Lemma simplify_ccompuimm_correct ge sp hst st c r n rs0 m m0 v: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj (expanse_condimm_int32u c (fsi_sreg_get hst r) n)) rs0 m0 = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n))). +Proof. + intros. + assert (HMEM: Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n) = + Val.cmpu_bool (Mem.valid_pointer m0) c v (Vint n)). + erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto. + unfold expanse_condimm_int32u, cond_int32u in *; destruct c; + intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; + try apply Int.same_if_eq in EQIMM; subst; + unfold loadimm32, sltuimm32, opimm32, load_hilo32; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; trivial; + try rewrite xor_neg_ltle_cmpu; + unfold Val.cmpu, zero32. + all: + try (specialize make_immed32_sound with n; + destruct (make_immed32 n) eqn:EQMKI); + try destruct (Int.eq lo Int.zero) eqn:EQLO; + try apply Int.same_if_eq in EQLO; subst; + intros; subst; + try erewrite fSop_correct; eauto; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + try rewrite OK2; + rewrite HMEM; + unfold may_undef_int, Val.cmpu; + destruct v; simpl; auto; + try rewrite EQIMM; try destruct (Archi.ptr64); simpl; + try rewrite ltu_12_wordsize; trivial; + try rewrite Int.add_commut, Int.add_zero_l; + try destruct (Int.ltu _ _) eqn:EQLTU; simpl; + try rewrite EQLTU; simpl; + trivial. +Qed. + +Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (cond_int64s c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmpl_bool c v v0)). +Proof. + intros. + unfold cond_int64s in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpl. + 1,2,3: rewrite optbool_mktotal; trivial. + - apply xor_neg_ltle_cmpl. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmpl_bool; trivial. + rewrite optbool_mktotal; trivial. + - apply xor_neg_ltge_cmpl. +Qed. + +Lemma simplify_ccomplu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj + (cond_int64u c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v v0)). +Proof. + intros. + erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)). + 2: eauto. + unfold cond_int64u in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmplu. + 1,2,3: rewrite optbool_mktotal; trivial. + - apply xor_neg_ltle_cmplu. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmplu_bool; trivial. + rewrite optbool_mktotal; trivial. + - apply xor_neg_ltge_cmplu. +Qed. + +Lemma simplify_ccomplimm_correct ge sp hst st c r n rs0 m m0 v: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj (expanse_condimm_int64s c (fsi_sreg_get hst r) n)) rs0 m0 = + Some (Val.of_optbool (Val.cmpl_bool c v (Vlong n))). +Proof. + intros. + unfold expanse_condimm_int64s, cond_int64s in *; destruct c; + intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; + try apply Int64.same_if_eq in EQIMM; subst; + unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + unfold Val.cmpl, zero64. + all: + try apply xor_neg_ltle_cmpl; + try apply xor_neg_ltge_cmpl; + try rewrite optbool_mktotal; trivial. + 4: + try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; subst; + try apply Int64.same_if_eq in EQMAX; subst; simpl. + 4: + intros; try (specialize make_immed32_sound with (Int.one); + destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. + 6: + intros; try (specialize make_immed64_sound with (Int64.add n Int64.one); + destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2); intros; simpl. + 1,2,3,9,10: + intros; try (specialize make_immed64_sound with (n); + destruct (make_immed64 n) eqn:EQMKI); intros; simpl. + all: + try destruct (Int.eq lo Int.zero) eqn:EQLO32; + try apply Int.same_if_eq in EQLO32; subst; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO64; + try apply Int64.same_if_eq in EQLO64; subst; + try erewrite fSop_correct; eauto; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + try rewrite OK2; + unfold may_undef_luil; + try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst; + try fold (Val.cmpl Clt v (Vlong imm)); + try rewrite xor_neg_ltge_cmpl; trivial; + try rewrite xor_neg_ltle_cmpl; trivial; + unfold Val.cmpl, may_undef_luil, Val.addl; + try rewrite xorl_zero_eq_cmpl; trivial; + try rewrite optbool_mktotal; trivial; + unfold may_undef_int, zero32, Val.add; simpl; + destruct v; auto. + 6,7,8: + try rewrite <- optbool_mktotal; trivial; + try rewrite Int64.add_commut, Int64.add_zero_l in *; + try fold (Val.cmpl Clt (Vlong i) (Vlong imm)); + try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))))); + try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))); + try rewrite xor_neg_ltge_cmpl; trivial; + try rewrite xor_neg_ltle_cmpl; trivial. + all: + try rewrite <- H; + try apply cmpl_ltle_add_one; auto; + try rewrite ltu_12_wordsize; + try rewrite Int.add_commut, Int.add_zero_l in *; + try rewrite Int64.add_commut, Int64.add_zero_l in *; + simpl; try rewrite lt_maxsgn_false_long; + try (rewrite <- H; trivial; fail); + simpl; trivial. +Qed. + +Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj (expanse_condimm_int64u c (fsi_sreg_get hst r) n)) rs0 m0 = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n))). +Proof. + intros. + assert (HMEM: Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n) = + Val.cmplu_bool (Mem.valid_pointer m0) c v (Vlong n)). + erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto. + unfold expanse_condimm_int64u, cond_int64u in *; destruct c; + intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; + unfold loadimm64, sltuimm64, opimm64, load_hilo64; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + unfold Val.cmplu, zero64. + (* Simplify make immediate and decompose subcases *) + all: + try (specialize make_immed64_sound with n; + destruct (make_immed64 n) eqn:EQMKI); + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + try erewrite fSop_correct; eauto; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + try rewrite OK2; + rewrite HMEM. + (* Ceq, Cne, Clt = itself *) + all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial. + (* Cle = xor (Clt) *) + all: try apply xor_neg_ltle_cmplu; trivial. + (* Others subcases with swap/negation *) + all: + unfold Val.cmplu, may_undef_int, zero64, Val.addl; + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; + try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu; + trivial; fail); + try (replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmplu_bool; trivial; fail); + try (replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmplu_bool; rewrite xor_neg_optb; trivial; fail); + try rewrite optbool_mktotal; trivial. + all: + try destruct v; simpl; auto; + try destruct (Archi.ptr64); simpl; + try rewrite EQIMM; + try rewrite HMEM; trivial; + try destruct (Int64.ltu _ _); + try rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu; + try rewrite <- optbool_mktotal; trivial. +Qed. + +Lemma simplify_ccompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp false cond_float c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (Val.cmpf_bool c v v0)). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpf. + - apply xor_neg_eqne_cmpf. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite swap_cmpf_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite swap_cmpf_bool; trivial. +Qed. + +Lemma simplify_cnotcompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp true cond_float c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpf. + 1,3,4: apply xor_neg_optb'. + all: destruct v, v0; simpl; trivial. + rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial. + 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl. + 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl. + all: destruct (Float.cmp _ _ _); trivial. +Qed. + +Lemma simplify_ccompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp false cond_single c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (Val.cmpfs_bool c v v0)). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpfs. + - apply xor_neg_eqne_cmpfs. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite swap_cmpfs_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite swap_cmpfs_bool; trivial. +Qed. + +Lemma simplify_cnotcompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp true cond_single c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpfs. + 1,3,4: apply xor_neg_optb'. + all: destruct v, v0; simpl; trivial. + rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial. + 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl. + 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl. + all: destruct (Float32.cmp _ _ _); trivial. +Qed. + +(* Main proof of simplification *) + +Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall + (H: target_op_simplify op lr hst = Some fsv) + (REF: hsilocal_refines ge sp rs0 m0 hst st) + (OK0: hsok_local ge sp rs0 m0 hst) + (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args) + (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m. +Proof. + unfold target_op_simplify; simpl. + intros H (LREF & SREF & SREG & SMEM) ? ? ?. + destruct op; try congruence. + destruct cond; repeat (destruct lr; simpl; try congruence); + simpl in OK1; + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + inv H; inv OK1. + (* Ccomp *) + - eapply simplify_ccomp_correct; eauto. + (* Ccompu *) + - eapply simplify_ccompu_correct; eauto. + (* Ccompimm *) + - eapply simplify_ccompimm_correct; eauto. + (* Ccompuimm *) + - eapply simplify_ccompuimm_correct; eauto. + (* Ccompl *) + - eapply simplify_ccompl_correct; eauto. + (* Ccomplu *) + - eapply simplify_ccomplu_correct; eauto. + (* Ccomplimm *) + - eapply simplify_ccomplimm_correct; eauto. + (* Ccompluimm *) + - eapply simplify_ccompluimm_correct; eauto. + (* Ccompf *) + - eapply simplify_ccompf_correct; eauto. + (* Cnotcompf *) + - eapply simplify_cnotcompf_correct; eauto. + (* Ccompfs *) + - eapply simplify_ccompfs_correct; eauto. + (* Cnotcompfs *) + - eapply simplify_cnotcompfs_correct; eauto. +Qed. + +Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall + (TARGET: target_cbranch_expanse hst c l = Some (c', l')) + (LREF : hsilocal_refines ge sp rs0 m0 hst st) + (OK: hsok_local ge sp rs0 m0 hst), + seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = + seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. +Proof. + unfold target_cbranch_expanse, seval_condition; simpl. + intros H (LREF & SREF & SREG & SMEM) ?. + destruct c; try congruence; + repeat (destruct l; simpl in H; try congruence). + 1,2,5,6: + destruct c; inv H; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + try replace (Cle) with (swap_comparison Cge) by auto; + try replace (Clt) with (swap_comparison Cgt) by auto; + try rewrite Val.swap_cmp_bool; trivial; + try rewrite Val.swap_cmpu_bool; trivial; + try rewrite Val.swap_cmpl_bool; trivial; + try rewrite Val.swap_cmplu_bool; trivial. + 1,2,3,4: + try destruct (Int.eq n Int.zero) eqn: EQIMM; + try apply Int.same_if_eq in EQIMM; + try destruct (Int64.eq n Int64.zero) eqn: EQIMM; + try apply Int64.same_if_eq in EQIMM; + destruct c; inv H; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32; + unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64; + intros; try (specialize make_immed32_sound with (n); + destruct (make_immed32 n) eqn:EQMKI); intros; simpl; + intros; try (specialize make_immed64_sound with (n); + destruct (make_immed64 n) eqn:EQMKI); intros; simpl; + try rewrite EQLO; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + try apply Int.same_if_eq in EQLO; simpl; trivial; + try apply Int64.same_if_eq in EQLO; simpl; trivial; + unfold may_undef_int, may_undef_luil; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; simpl; trivial; + try destruct v; try rewrite H; + try rewrite ltu_12_wordsize; try rewrite EQLO; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int64.add_commut, Int64.add_zero_l; + auto; simpl; + try rewrite H in EQIMM; + try rewrite EQLO in EQIMM; + try rewrite Int.add_commut, Int.add_zero_l in EQIMM; + try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM; + try rewrite EQIMM; simpl; + try destruct (Archi.ptr64); trivial. + + 1,2,3,4: + destruct c; inv H; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + unfold zero32, zero64, Val.cmpf, Val.cmpfs; + destruct v, v0; simpl; trivial; + try rewrite Float.cmp_ne_eq; + try rewrite Float32.cmp_ne_eq; + try rewrite <- Float.cmp_swap; simpl; + try rewrite <- Float32.cmp_swap; simpl; + try destruct (Float.cmp _ _); simpl; + try destruct (Float32.cmp _ _); simpl; + try rewrite Int.eq_true; simpl; + try rewrite Int.eq_false; try apply Int.one_not_zero; + simpl; trivial. +Qed. +Global Opaque target_op_simplify. +Global Opaque target_cbranch_expanse. diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index e779b114..97f3ff61 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -17,6 +17,34 @@ Require Import Zbits. (** Value analysis for RISC V operators *) +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 + | None => sem v1 v2 + | Some true => sem vz v1 + | Some false => sem v1 vz + end. + +Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval := + if negb is_long then + match v1 with + | I _ => sem vimm vz + | _ => Ifptr Ptop + end + else + match v1 with + | L _ => sem vimm vz + | _ => Ifptr Ptop + end. + +Definition may_undef_luil (v1: aval) (n: int64): aval := + match v1 with + | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12))) + | _ => Ifptr Ptop + end. + Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -31,6 +59,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 | _, _ => Bnone end. @@ -170,6 +214,35 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) + | 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) + | 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) + | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12)) + | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32 + | 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) + | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) + | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) + | OExoril n, v1::nil => xorl v1 (L n) + | OEluil n, v1::nil => may_undef_luil v1 n + | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64 + | OEloadli n, nil => L (n) + | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) + | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) + | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) + | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2) + | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2) + | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2) | Obits_of_single, v1::nil => bits_of_single v1 | Obits_of_float, v1::nil => bits_of_float v1 | Osingle_of_bits, v1::nil => single_of_bits v1 @@ -266,7 +339,9 @@ Proof. destruct cond; simpl; eauto with va. inv H2. destruct cond; simpl; eauto with va. - destruct cond; auto with va. + 17: destruct cond; simpl; eauto with va. + all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0; + unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. Lemma symbol_address_sound: @@ -307,7 +382,71 @@ Proof. destruct addr; InvHyps; eauto with va. rewrite Ptrofs.add_zero_l; eauto with va. Qed. - + +Lemma of_optbool_maketotal_sound: + forall ob ab, cmatch ob ab -> vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (of_optbool ab). +Proof. + intros. + assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)). + { + destruct ob; simpl; auto with va. + destruct b; constructor; try omega. + change 1 with (usize Int.one). apply is_uns_usize. + red; intros. apply Int.bits_zero. + } + inv H; auto. simpl. destruct b; constructor. +Qed. + +Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 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)). +Proof. + intros. + destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. +Qed. + +Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR0 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.zero64)) + (of_optbool (apply_bin_r0 optR0 (cmplu_bool c) b1 b0 zero64)). +Proof. + intros. + destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. +Qed. + +Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0 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)). +Proof. + intros. + destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. +Qed. + +Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0 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)). +Proof. + intros. + destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. +Qed. + Theorem eval_static_operation_sound: forall op vargs m vres aargs, eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres -> @@ -320,6 +459,25 @@ Proof. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + + 3,4,6: apply eval_cmpu_sound; auto. + 1,2,3: apply eval_cmp_sound; auto. + unfold Val.cmp; apply of_optbool_sound; eauto with va. + unfold Val.cmpu; apply of_optbool_sound; eauto with va. + unfold zero32; simpl; eauto with va. + + 1,2,11,12: + try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64; + try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1; + inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va; + try apply vmatch_ifptr_i; try apply vmatch_ifptr_l. + + 3,4,6: apply eval_cmplu_sound; auto. + 1,2,3: apply eval_cmpl_sound; auto. + unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. + unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. + unfold zero64; simpl; eauto with va. + all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. End SOUNDNESS. |