diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 34 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 49 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 233 | ||||
-rw-r--r-- | mppa_k1c/Machregs.v | 2 | ||||
-rw-r--r-- | mppa_k1c/NeedOp.v | 205 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 206 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 11 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 26 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 104 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 35 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 90 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 85 |
15 files changed, 1004 insertions, 86 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 115c8d6d..b323a67c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -214,6 +214,8 @@ Inductive instruction : Type := | Pandnil (rd rs: ireg) (imm: int64) (**r andn long *)
| Pornil (rd rs: ireg) (imm: int64) (**r orn long *)
| Pmaddil (rd rs: ireg) (imm: int64) (**r multiply add imm long *)
+ | Pcmove (bt: btest) (rcond rd rs : ireg) (** conditional move *)
+ | Pcmoveu (bt: btest) (rcond rd rs : ireg) (** conditional move, unsigned semantics *)
.
(** Correspondance between Asmblock and Asm *)
@@ -361,6 +363,8 @@ Definition basic_to_instruction (b: basic) := (** ARRR *)
| PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
| PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
+ | PArithARRR (Asmblock.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
+ | PArithARRR (Asmblock.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
(** ARRI32 *)
| PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index e612576f..339b44c6 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -417,6 +417,8 @@ Inductive arith_name_rri64 : Type := Inductive arith_name_arrr : Type := | Pmaddw (**r multiply add word *) | Pmaddl (**r multiply add long *) + | Pcmove (bt: btest) (**r conditional move *) + | Pcmoveu (bt: btest) (**r conditional move, test on unsigned semantics *) . Inductive arith_name_arri32 : Type := @@ -1212,6 +1214,38 @@ Definition arith_eval_arrr n v1 v2 v3 := match n with | Pmaddw => Val.add v1 (Val.mul v2 v3) | Pmaddl => Val.addl v1 (Val.mull v2 v3) + | Pcmove bt => + match cmp_for_btest bt with + | (Some c, Int) => + match Val.cmp_bool c v2 (Vint Int.zero) with + | None => Vundef + | Some true => v3 + | Some false => v1 + end + | (Some c, Long) => + match Val.cmpl_bool c v2 (Vlong Int64.zero) with + | None => Vundef + | Some true => v3 + | Some false => v1 + end + | (None, _) => Vundef + end + | Pcmoveu bt => + match cmpu_for_btest bt with + | (Some c, Int) => + match Val_cmpu_bool c v2 (Vint Int.zero) with + | None => Vundef + | Some true => v3 + | Some false => v1 + end + | (Some c, Long) => + match Val_cmplu_bool c v2 (Vlong Int64.zero) with + | None => Vundef + | Some true => v3 + | Some false => v1 + end + | (None, _) => Vundef + end end. Definition arith_eval_arri32 n v1 v2 v3 := diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 92630772..96547342 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1445,6 +1445,8 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring := match n with | Pmaddw => "Pmaddw" | Pmaddl => "Pmaddl" + | Pcmove _ => "Pcmove" + | Pcmoveu _ => "Pcmoveu" end. Definition string_of_name_arri32 (n: arith_name_arri32): pstring := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 3260312d..b3478a9a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -367,6 +367,28 @@ Definition transl_cond_op Error(msg "Asmblockgen.transl_cond_op") end. +(* CoMPare Unsigned Words to Zero *) +Definition btest_for_cmpuwz (c: comparison) := + match c with + | Cne => OK BTwnez + | Ceq => OK BTweqz + | Clt => Error (msg "btest_for_compuwz: Clt") + | Cge => Error (msg "btest_for_compuwz: Cge") + | Cle => Error (msg "btest_for_compuwz: Cle") + | Cgt => Error (msg "btest_for_compuwz: Cgt") + end. + +(* CoMPare Unsigned Words to Zero *) +Definition btest_for_cmpudz (c: comparison) := + match c with + | Cne => OK BTdnez + | Ceq => OK BTdeqz + | Clt => Error (msg "btest_for_compudz: Clt") + | Cge => Error (msg "btest_for_compudz: Cge") + | Cle => Error (msg "btest_for_compudz: Cle") + | Cgt => Error (msg "btest_for_compudz: Cgt") + end. + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -729,6 +751,33 @@ Definition transl_op do rd <- ireg_of res; transl_cond_op cmp rd args k + | Oselect cond, a0 :: a1 :: aS :: nil + | Oselectl cond, a0 :: a1 :: aS :: nil => + assertion (mreg_eq a0 res); + do r0 <- ireg_of a0; + do r1 <- ireg_of a1; + do rS <- ireg_of aS; + (match cond with + | Ccomp0 cmp => + OK (Pcmove (btest_for_cmpswz cmp) r0 rS r1 ::i k) + | Ccompu0 cmp => + do bt <- btest_for_cmpuwz cmp; + OK (Pcmoveu bt r0 rS r1 ::i k) + | Ccompl0 cmp => + OK (Pcmove (btest_for_cmpsdz cmp) r0 rS r1 ::i k) + | Ccomplu0 cmp => + do bt <- btest_for_cmpudz cmp; + OK (Pcmoveu bt r0 rS r1 ::i k) + end) + + | Oselectf, a0 :: a1 :: aS :: nil + | Oselectfs, a0 :: a1 :: aS :: nil => + assertion (mreg_eq a0 res); + do r0 <- ireg_of a0; + do r1 <- ireg_of a1; + do rS <- ireg_of aS; + OK (Pcmove BTwnez r0 rS r1 ::i k) + | _, _ => Error(msg "Asmgenblock.transl_op") end. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 5ccea246..874e40a8 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1530,6 +1530,26 @@ Ltac TranslOpSimpl := [ apply exec_straight_one; reflexivity | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ]. +Lemma int_eq_comm: + forall (x y: int), + (Int.eq x y) = (Int.eq y x). +Proof. + intros. + unfold Int.eq. + unfold zeq. + destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. +Qed. + +Lemma int64_eq_comm: + forall (x y: int64), + (Int64.eq x y) = (Int64.eq y x). +Proof. + intros. + unfold Int64.eq. + unfold zeq. + destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. +Qed. + Lemma transl_op_correct: forall op args res k (rs: regset) m v c, transl_op op args res k = OK c -> @@ -1617,69 +1637,156 @@ Opaque Int.eq. - (* Ocmp *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. -(* -- (* 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. -- (* stackoffset *) - exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). - exists rs'; split; eauto. auto with asmgen. -- (* 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. - intros (rs' & A & B & C). - 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. - - - -- (* 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. - 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. - 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. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. -*) +- (* Oselect *) + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); + econstructor; split; + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmplu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + +- (* Oselect *) + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); + econstructor; split; + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmplu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + +- (* Oselectf *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold eval_selectf. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. +- (* Oselectfs *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold eval_selectfs. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. Qed. (** Memory accesses *) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 60142797..ddf730a9 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -209,7 +209,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ => true + | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf | Oselectfs => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 2577370c..a276cda1 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -117,6 +117,7 @@ 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 + | Oselect _ | Oselectl _ | Oselectf | Oselectfs => op3 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -145,19 +146,75 @@ Section SOUNDNESS. Variable ge: genv. Variable sp: block. -Variables m m': mem. -Hypothesis PERM: forall b ofs k p, Mem.perm m b ofs k p -> Mem.perm m' b ofs k p. +Variables m1 m2: mem. +Hypothesis PERM: forall b ofs k p, Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p. Lemma needs_of_condition_sound: forall cond args b args', - eval_condition cond args m = Some b -> + eval_condition cond args m1 = Some b -> vagree_list args args' (needs_of_condition cond) -> - eval_condition cond args' m' = Some b. + eval_condition cond args' m2 = Some b. Proof. intros. unfold needs_of_condition in H0. eapply default_needs_of_condition_sound; eauto. Qed. +Let valid_pointer_inj: + forall b1 ofs b2 delta, + inject_id b1 = Some(b2, delta) -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. +Proof. + unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero. + rewrite Mem.valid_pointer_nonempty_perm in *. eauto. +Qed. + +Let weak_valid_pointer_inj: + forall b1 ofs b2 delta, + inject_id b1 = Some(b2, delta) -> + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. +Proof. + unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero. + rewrite Mem.weak_valid_pointer_spec in *. + rewrite ! Mem.valid_pointer_nonempty_perm in *. + destruct H0; [left|right]; eauto. +Qed. + +Let weak_valid_pointer_no_overflow: + forall b1 ofs b2 delta, + inject_id b1 = Some(b2, delta) -> + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. +Proof. + unfold inject_id; intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. +Qed. + +Let valid_different_pointers_inj: + forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, + b1 <> b2 -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> + inject_id b1 = Some (b1', delta1) -> + inject_id b2 = Some (b2', delta2) -> + b1' <> b2' \/ + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). +Proof. + unfold inject_id; intros. left; congruence. +Qed. + +Lemma needs_of_condition0_sound: + forall cond arg1 b arg2, + eval_condition0 cond arg1 m1 = Some b -> + vagree arg1 arg2 All -> + eval_condition0 cond arg2 m2 = Some b. +Proof. + intros until arg2. + intros Hcond Hagree. + apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); simpl; auto. + apply val_inject_lessdef. apply lessdef_vagree. assumption. +Qed. + Lemma addl_sound: forall v1 w1 v2 w2 x, vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> @@ -185,6 +242,132 @@ Proof. inv H. inv H0. trivial. Qed. + +Lemma select_sound: + forall cond v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_select cond v0 v1 v2 m1) (eval_select cond w0 w1 w2 m2) x. +Proof. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_select_to2. + rewrite eval_select_to2. + unfold eval_select2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + apply iagree_refl. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + apply iagree_refl. + - rewrite eval_select_to2. + rewrite eval_select_to2. + unfold eval_select2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. +Qed. + +Lemma selectl_sound: + forall cond v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_selectl cond v0 v1 v2 m1) (eval_selectl cond w0 w1 w2 m2) x. +Proof. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_selectl_to2. + rewrite eval_selectl_to2. + unfold eval_selectl2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + - rewrite eval_selectl_to2. + rewrite eval_selectl_to2. + unfold eval_selectl2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. +Qed. + +Lemma selectf_sound: + forall v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_selectf v0 v1 v2) (eval_selectf w0 w1 w2) x. +Proof. + unfold default; intros. + destruct x; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. +Qed. + +Lemma selectfs_sound: + forall v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_selectfs v0 v1 v2) (eval_selectfs w0 w1 w2) x. +Proof. + unfold default; intros. + destruct x; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. +Qed. Remark default_idem: forall nv, default (default nv) = default nv. Proof. @@ -193,11 +376,11 @@ Qed. Lemma needs_of_operation_sound: forall op args v nv args', - eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v -> vagree_list args args' (needs_of_operation op nv) -> nv <> Nothing -> exists v', - eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v' + eval_operation ge (Vptr sp Ptrofs.zero) op args' m2 = Some v' /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); @@ -238,12 +421,20 @@ Proof. apply mull_sound; trivial. rewrite default_idem; trivial. rewrite default_idem; trivial. + (* select *) +- apply select_sound; trivial. + (* selectl *) +- apply selectl_sound; trivial. + (* selectf *) +- apply selectf_sound; trivial. + (* selectfs *) +- apply selectfs_sound; trivial. Qed. Lemma operation_is_redundant_sound: forall op nv arg1 args v arg1' args', operation_is_redundant op nv = true -> - eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m1 = Some v -> vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index d533a504..045946fd 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -51,6 +51,18 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) +Inductive condition0 : Type := + | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *) + | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *) + | Ccompl0 (c: comparison) (**r signed 64-bit integer comparison with 0 *) + | Ccomplu0 (c: comparison). (**r unsigned 64-bit integer comparison with 0 *) + +Definition arg_type_of_condition0 (cond: condition0) := + match cond with + | Ccomp0 _ | Ccompu0 _ => Tint + | Ccompl0 _ | Ccomplu0 _ => Tlong + end. + (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -181,7 +193,11 @@ 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. *) + | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + | Oselect (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) + | Oselectl (cond: condition0)(**r [rd = if cond r3 then r2 else r1] *) + | Oselectf (**r [rd = if r3 then r2 else r1] *) + | Oselectfs. (**r [rd = if r3 then r2 else r1] *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -201,6 +217,13 @@ Proof. decide equality. Defined. +Definition eq_condition0 (x y: condition0) : {x=y} + {x<>y}. +Proof. + generalize Int.eq_dec Int64.eq_dec; intro. + assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + decide equality. +Defined. + Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. generalize ident_eq Ptrofs.eq_dec; intros. @@ -209,7 +232,7 @@ 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 eq_condition0; intros. decide equality. Defined. @@ -233,7 +256,7 @@ 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 eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2 @@ -250,6 +273,90 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) | _, _ => None end. + +Definition eval_condition0 (cond: condition0) (v1: val) (m: mem): option bool := + match cond with + | Ccomp0 c => Val.cmp_bool c v1 (Vint Int.zero) + | Ccompu0 c => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint Int.zero) + | Ccompl0 c => Val.cmpl_bool c v1 (Vlong Int64.zero) + | Ccomplu0 c => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong Int64.zero) + end. + +Definition eval_select (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match v0, v1, (eval_condition0 cond vselect m) with + | Vint i0, Vint i1, Some bval => Vint (if bval then i1 else i0) + | _,_,_ => Vundef + end. + +Definition eval_select2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match (eval_condition0 cond vselect m), v0, v1 with + | Some bval, Vint i0, Vint i1 => Vint (if bval then i1 else i0) + | _,_,_ => Vundef + end. + +Lemma eval_select_to2: forall cond v0 v1 vselect m, + (eval_select cond v0 v1 vselect m) = + (eval_select2 cond v0 v1 vselect m). +Proof. + intros. + unfold eval_select2. + destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity. +Qed. + +Definition eval_selectl (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match v0, v1, (eval_condition0 cond vselect m) with + | Vlong i0, Vlong i1, Some bval => Vlong (if bval then i1 else i0) + | _,_,_ => Vundef + end. + +Definition eval_selectl2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match (eval_condition0 cond vselect m), v0, v1 with + | Some bval, Vlong i0, Vlong i1 => Vlong (if bval then i1 else i0) + | _,_,_ => Vundef + end. + +Lemma eval_selectl_to2: forall cond v0 v1 vselect m, + (eval_selectl cond v0 v1 vselect m) = + (eval_selectl2 cond v0 v1 vselect m). +Proof. + intros. + unfold eval_selectl2. + destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity. +Qed. + +Definition eval_selectf (v0 : val) (v1 : val) (vselect : val) : val := + match vselect with + | Vint iselect => + match v0 with + | Vfloat i0 => + match v1 with + | Vfloat i1 => + Vfloat (if Int.cmp Ceq Int.zero iselect + then i0 + else i1) + | _ => Vundef + end + | _ => Vundef + end + | _ => Vundef + end. + +Definition eval_selectfs (v0 : val) (v1 : val) (vselect : val) : val := + match vselect with + | Vint iselect => + match v0 with + | Vsingle i0 => + match v1 with + | Vsingle i1 => + Vsingle (if Int.cmp Ceq Int.zero iselect + then i0 + else i1) + | _ => Vundef + end + | _ => Vundef + end + | _ => Vundef + end. Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) @@ -379,6 +486,10 @@ Definition eval_operation | Osingleoflong, v1::nil => Val.singleoflong v1 | Osingleoflongu, v1::nil => Val.singleoflongu v1 | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) + | (Oselect cond), v0::v1::vselect::nil => Some (eval_select cond v0 v1 vselect m) + | (Oselectl cond), v0::v1::vselect::nil => Some (eval_selectl cond v0 v1 vselect m) + | Oselectf, v0::v1::vselect::nil => Some (eval_selectf v0 v1 vselect) + | Oselectfs, v0::v1::vselect::nil => Some (eval_selectfs v0 v1 vselect) | _, _ => None end. @@ -567,6 +678,11 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) + + | Oselect cond => (Tint :: Tint :: (arg_type_of_condition0 cond) :: nil, Tint) + | Oselectl cond => (Tlong :: Tlong :: (arg_type_of_condition0 cond) :: nil, Tlong) + | Oselectf => (Tfloat :: Tfloat :: Tint :: nil, Tfloat) + | Oselectfs => (Tsingle :: Tsingle :: Tint :: nil, Tsingle) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -802,6 +918,29 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; simpl in H0; inv H0... (* cmp *) - destruct (eval_condition cond vl m)... destruct b... + (* select *) + - destruct v0; destruct v1; simpl in *; try discriminate; trivial. + destruct cond; destruct v2; simpl in *; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. + (* selectl *) + - destruct v0; destruct v1; simpl in *; try discriminate; trivial. + destruct cond; destruct v2; simpl in *; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. + + destruct Archi.ptr64; simpl; trivial. + destruct (_ && _); simpl; trivial. + destruct (Val.cmp_different_blocks _); simpl; trivial. + + (* selectf *) + - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. + (* selectfs *) + - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. Qed. End SOUNDNESS. @@ -962,6 +1101,13 @@ Definition op_depends_on_memory (op: operation) : bool := | Ocmp (Ccompuimm _ _) => negb Archi.ptr64 | Ocmp (Ccomplu _) => Archi.ptr64 | Ocmp (Ccompluimm _ _) => Archi.ptr64 + + | Oselect (Ccompu0 _) => negb Archi.ptr64 + | Oselect (Ccomplu0 _) => Archi.ptr64 + + | Oselectl (Ccompu0 _) => negb Archi.ptr64 + | Oselectl (Ccomplu0 _) => Archi.ptr64 + | _ => false end. @@ -970,9 +1116,10 @@ Lemma op_depends_on_memory_correct: op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. + intros until m2. destruct op; simpl; try congruence; + destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF; - unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. + unfold eval_select, eval_selectl, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -1100,6 +1247,19 @@ Proof. - inv H3; inv H2; simpl in H0; inv H0; auto. Qed. +Lemma eval_condition0_inj: + forall cond v1 v2 b, + Val.inject f v1 v2 -> + eval_condition0 cond v1 m1 = Some b -> + eval_condition0 cond v2 m2 = Some b. +Proof. + intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. + - inv H; simpl in *; congruence. + - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. + - inv H; simpl in *; congruence. + - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +Qed. + Ltac TrivialExists := match goal with | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => @@ -1328,6 +1488,42 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + (* select *) + - unfold eval_select. + inv H4; trivial. + inv H2; trivial. + inv H3; trivial; + try (destruct cond; simpl; trivial; fail). + destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial. + eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b). + * eapply eval_condition0_inj. + eapply Val.inject_ptr. + eassumption. + reflexivity. + assumption. + * rewrite Hcond'. constructor. + (* selectl *) + - unfold eval_selectl. + inv H4; trivial. + inv H2; trivial. + inv H3; trivial; + try (destruct cond; simpl; trivial; fail). + destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial. + eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b). + * eapply eval_condition0_inj. + eapply Val.inject_ptr. + eassumption. + reflexivity. + assumption. + * rewrite Hcond'. constructor. + (* selectf *) + - inv H3; simpl; try constructor. + inv H4; simpl; try constructor. + inv H2; simpl; constructor. + (* selectfs *) + - inv H3; simpl; try constructor. + inv H4; simpl; try constructor. + inv H2; simpl; constructor. Qed. Lemma eval_addressing_inj: diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index f7a35443..c4d8cd8d 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -128,6 +128,8 @@ let arith_rri64_str = function let arith_arrr_str = function | Pmaddw -> "Pmaddw" | Pmaddl -> "Pmaddl" + | Pcmove _ -> "Pcmove" + | Pcmoveu _ -> "Pcmoveu" let arith_ri32_str = "Pmake" @@ -420,7 +422,7 @@ type real_instruction = | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd - | Maddw | Maddd + | Maddw | Maddd | Cmoved | Make | Nop | Sxwd | Zxwd (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld @@ -487,7 +489,8 @@ let ab_inst_to_real = function | "Pfixedudrzz" -> Fixedudz | "Pfixeddrzz_i32" -> Fixeddz | "Pfixedudrzz_i32" -> Fixedudz - + | "Pcmove" | "Pcmoveu" -> Cmoved + | "Plb" -> Lbs | "Plbu" -> Lbz | "Plh" -> Lhs @@ -536,7 +539,7 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> alu_tiny_x | _ -> raise InvalidEncoding) | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord - | Nxord | Andnd | Ornd -> + | Nxord | Andnd | Ornd | Cmoved -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) @@ -589,7 +592,7 @@ let real_inst_to_latency = function | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw | Nandd | Nord | Nxord | Ornd | Andnd | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make - | Sxwd | Zxwd | Fcompw | Fcompd + | Sxwd | Zxwd | Fcompw | Fcompd | Cmoved -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 31112dca..f8f5bf3b 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -258,9 +258,17 @@ Nondetfunction andl (e1: expr) (e2: expr) := | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2 | t1, Eop (Olongconst n2) Enil => andlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) - | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) | _, _ => Eop Oandl (e1:::e2:::Enil) end. +(* + | (Eop Ocast32signed + ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1)) + (y1:::Enil)):::Enil)):::Enil)), v1 => + if Int64.eq zero1 Int64.zero + then Eop Oselectl ((Eop (Olongconst Int64.zero) Enil):::v1:::y1:::Enil) + else Eop Oandl (e1:::e2:::Enil) +*) Nondetfunction orlimm (n1: int64) (e2: expr) := if Int64.eq n1 Int64.zero then e2 else @@ -277,9 +285,23 @@ Nondetfunction orl (e1: expr) (e2: expr) := | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2 | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) - | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) | _, _ => Eop Oorl (e1:::e2:::Enil) end. + + (* + | (Eop Oandl ((Eop Ocast32signed + ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0)) + (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)), + (Eop Oandl ((Eop Ocast32signed + ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1)) + (y1:::Enil)):::Enil)):::Enil)):::v1:::Enil)) => + if same_expr_pure y0 y1 + && Int64.eq zero0 Int64.zero + && Int64.eq zero1 Int64.zero + then Eop Oselectl (v0:::v1:::y0:::Enil) + else Eop Oorl (e1:::e2:::Enil) + *) Nondetfunction xorlimm (n1: int64) (e2: expr) := if Int64.eq n1 Int64.zero then e2 else diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 51b989d6..e18de2ee 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -390,6 +390,15 @@ Proof. - TrivialExists. Qed. +Lemma int64_eq_commut: forall x y : int64, + (Int64.eq x y) = (Int64.eq y x). +Proof. + intros. + predSpec Int64.eq Int64.eq_spec x y; + predSpec Int64.eq Int64.eq_spec y x; + congruence. +Qed. + Theorem eval_andl: binary_constructor_sound andl Val.andl. Proof. unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl. @@ -398,6 +407,25 @@ Proof. - InvEval. apply eval_andlimm; auto. - (*andn*) InvEval. TrivialExists. simpl. congruence. - (*andn reverse*) InvEval. rewrite Val.andl_commut. TrivialExists; simpl. congruence. + (* +- (* selectl *) + InvEval. + predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; TrivialExists. + + constructor. econstructor; constructor. + constructor; try constructor; try constructor; try eassumption. + + simpl in *. f_equal. inv H6. + unfold selectl. + simpl. + destruct v3; simpl; trivial. + rewrite int64_eq_commut. + destruct (Int64.eq i Int64.zero); simpl. + * replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve. + destruct y; simpl; trivial. + * replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve. + destruct y; simpl; trivial. + rewrite Int64.and_commut. rewrite Int64.and_mone. reflexivity. + + constructor. econstructor. constructor. econstructor. constructor. econstructor. constructor. eassumption. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. eassumption. constructor. + + simpl in *. congruence. *) - TrivialExists. Qed. @@ -414,6 +442,7 @@ Proof. - TrivialExists. Qed. + Theorem eval_orl: binary_constructor_sound orl Val.orl. Proof. unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl. @@ -423,6 +452,81 @@ Proof. - InvEval. apply eval_orlimm; auto. - (*orn*) InvEval. TrivialExists; simpl; congruence. - (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence. + (* + - (* selectl *) + destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists. + predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists. + predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; [ | TrivialExists]. + inv H. + inv H0. + inv H6. + inv H3. + inv H2. + inv H7. + inv H4. + inv H3. + inv H6. + inv H4. + inv H3. + inv H14. + inv H13. + inv H6. + inv H4. + inv H13. + inv H14. + inv H9. + inv H11. + inv H13. + inv H3. + inv H6. + inv H7. + inv H3. + inv H14. + inv H17. + simpl in *. + inv H8. + inv H5. + inv H10. + inv H12. + inv H15. + inv H16. + inv H11. + inv H13. + unfold same_expr_pure in PURE. + destruct y0; try congruence. + destruct y1; try congruence. + destruct (ident_eq i i0); try congruence; clear PURE. + rewrite <- e0 in *; clear e0. + inv H6. + inv H7. + rename v10 into vtest. + replace v11 with vtest in * by congruence. + TrivialExists. + simpl. + f_equal. + unfold selectl. + destruct vtest; simpl; trivial. + rewrite Val.andl_commut. + destruct v4; simpl; trivial. + rewrite Val.andl_commut. + rewrite Val.orl_commut. + destruct v9; simpl; trivial. + rewrite int64_eq_commut. + destruct (Int64.eq i1 Int64.zero); simpl. + + + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve. + replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve. + rewrite Int64.and_mone. + rewrite Int64.and_zero. + rewrite Int64.or_commut. + rewrite Int64.or_zero. + reflexivity. + + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve. + replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve. + rewrite Int64.and_mone. + rewrite Int64.and_zero. + rewrite Int64.or_zero. + reflexivity. *) - TrivialExists. Qed. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index d82fe238..eeb3ffae 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -61,6 +61,21 @@ Section SELECT. Context {hf: helper_functions}. +(** Ternary operator *) +Definition select_base o0 o1 oselect := + Eop (Oselect (Ccomp0 Cne)) + (o0:::o1:::oselect:::Enil). + +Definition select o0 o1 oselect := + select_base o0 o1 oselect. + +Definition selectl_base o0 o1 oselect := + Eop (Oselectl (Ccomp0 Cne)) + (o0:::o1:::oselect:::Enil). + +Definition selectl o0 o1 oselect := + selectl_base o0 o1 oselect. + (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := @@ -275,7 +290,25 @@ Nondetfunction or (e1: expr) (e2: expr) := then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil) | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) - | t1, (Eop Onot (t2:::Enil)) => Eop Oorn (t2:::t1:::Enil) + | t1, (Eop Onot (t2:::Enil)) => Eop Oorn (t2:::t1:::Enil) + | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompimm Ceq zero0)) + (y0:::Enil)):::Enil)):::v0:::Enil)), + (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompimm Cne zero1)) + (y1:::Enil)):::Enil)):::v1:::Enil)) => + if same_expr_pure y0 y1 + && Int.eq zero0 Int.zero + && Int.eq zero1 Int.zero + then select_base v0 v1 y0 + else Eop Oor (e1:::e2:::Enil) + | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0)) + (y0:::Enil)):::Enil)):::v0:::Enil)), + (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Cne zero1)) + (y1:::Enil)):::Enil)):::v1:::Enil)) => + if same_expr_pure y0 y1 + && Int.eq zero0 Int.zero + && Int.eq zero1 Int.zero + then select_base v0 v1 y0 + else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index d426e4f1..4af5ccfa 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -92,7 +92,7 @@ Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. - + (* Helper lemmas - from SplitLongproof.v *) Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. @@ -162,7 +162,7 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v. - + Theorem eval_addrsymbol: forall le id ofs, exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v. @@ -526,6 +526,15 @@ Proof. discriminate. Qed. +Lemma int_eq_commut: forall x y : int, + (Int.eq x y) = (Int.eq y x). +Proof. + intros. + predSpec Int.eq Int.eq_spec x y; + predSpec Int.eq Int.eq_spec y x; + congruence. +Qed. + Theorem eval_or: binary_constructor_sound or Val.or. Proof. unfold or; red; intros. @@ -553,6 +562,83 @@ Proof. exists (Val.ror v1 (Vint n2)); split. EvalOp. rewrite Val.or_commut. apply ROR; auto. - (*orn*) TrivialExists; simpl; congruence. - (*orn reversed*) rewrite Val.or_commut. TrivialExists; simpl; congruence. + - (* select *) + destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try exact DEFAULT. + predSpec Int.eq Int.eq_spec zero0 Int.zero; simpl; try exact DEFAULT. + predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. + TrivialExists. + simpl in *. + unfold eval_select. + f_equal. + inv H6. + inv H7. + inv H9. + inv H11. + unfold same_expr_pure in PURE. + destruct y0; try congruence. + destruct y1; try congruence. + destruct (ident_eq i i0); try congruence. + rewrite <- e0 in *. clear e0. clear PURE. + inv H2. inv H5. + replace v8 with v4 in * by congruence. + rename v4 into vselect. + destruct vselect; simpl; trivial; + destruct v5; simpl; trivial; destruct v9; simpl; trivial; + destruct (Int.eq i1 Int.zero); simpl; trivial. + + rewrite Int.neg_zero. + rewrite Int.and_commut. + rewrite Int.and_mone. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.or_zero. + reflexivity. + + rewrite Int.neg_zero. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.and_commut. + rewrite Int.and_mone. + rewrite Int.or_commut. + rewrite Int.or_zero. + reflexivity. + - (* select unsigned *) + destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try exact DEFAULT. + predSpec Int.eq Int.eq_spec zero0 Int.zero; simpl; try exact DEFAULT. + predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. + TrivialExists. + simpl in *. + unfold eval_select. + f_equal. + inv H6. + inv H7. + inv H9. + inv H11. + unfold same_expr_pure in PURE. + destruct y0; try congruence. + destruct y1; try congruence. + destruct (ident_eq i i0); try congruence. + rewrite <- e0 in *. clear e0. clear PURE. + inv H2. inv H5. + replace v8 with v4 in * by congruence. + rename v4 into vselect. + destruct vselect; simpl; trivial; + destruct v5; simpl; trivial; + destruct v9; simpl; trivial; + destruct (Int.eq i1 Int.zero); simpl; trivial. + + rewrite Int.neg_zero. + rewrite Int.and_commut. + rewrite Int.and_mone. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.or_zero. + reflexivity. + + rewrite Int.neg_zero. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.and_commut. + rewrite Int.and_mone. + rewrite Int.or_commut. + rewrite Int.or_zero. + reflexivity. - apply DEFAULT. Qed. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index ef02c25a..6f292460 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -529,6 +529,10 @@ module Target (*: TARGET*) = | Pmaddil (rd, rs, imm) -> fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pcmove (bt, rd, rcond, rs) | Pcmoveu (bt, rd, rcond, rs) -> + fprintf oc " cmoved.%a %a? %a = %a\n" + bcond bt ireg rcond ireg rd ireg rs + let get_section_names name = let (text, lit) = match C2C.atom_sections name with diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index a54dbd8f..62cfa85e 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -42,6 +42,44 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := | _, _ => Vbot end. +Definition eval_static_condition0 (cond : condition0) (v : aval) : abool := + match cond with + | Ccomp0 c => cmp_bool c v (I Int.zero) + | Ccompu0 c => cmpu_bool c v (I Int.zero) + | Ccompl0 c => cmpl_bool c v (L Int64.zero) + | Ccomplu0 c => cmplu_bool c v (L Int64.zero) + end. + +Definition eval_static_select (cond : condition0) (v0 v1 vselect : aval) : aval := + match eval_static_condition0 cond vselect with + | Just b => binop_int (fun x0 x1 => if b then x1 else x0) v0 v1 + | _ => Vtop + end. + +Definition eval_static_selectl (cond : condition0) (v0 v1 vselect : aval) : aval := + match eval_static_condition0 cond vselect with + | Just b => binop_long (fun x0 x1 => if b then x1 else x0) v0 v1 + | _ => Vtop + end. + +Definition eval_static_selectf (v0 v1 vselect : aval) : aval := + match vselect with + | I iselect => + if Int.eq Int.zero iselect + then binop_float (fun x0 x1 => x0) v0 v1 + else binop_float (fun x0 x1 => x1) v0 v1 + | _ => Vtop + end. + +Definition eval_static_selectfs (v0 v1 vselect : aval) : aval := + match vselect with + | I iselect => + if Int.eq Int.zero iselect + then binop_single (fun x0 x1 => x0) v0 v1 + else binop_single (fun x0 x1 => x1) v0 v1 + | _ => Vtop + end. + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -166,6 +204,10 @@ 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) + | (Oselect cond), v0::v1::vselect::nil => eval_static_select cond v0 v1 vselect + | (Oselectl cond), v0::v1::vselect::nil => eval_static_selectl cond v0 v1 vselect + | Oselectf, v0::v1::vselect::nil => eval_static_selectf v0 v1 vselect + | Oselectfs, v0::v1::vselect::nil => eval_static_selectfs v0 v1 vselect | _, _ => Vbot end. @@ -191,6 +233,15 @@ Proof. destruct cond; auto with va. Qed. +Theorem eval_static_condition0_sound: + forall cond varg m aarg, + vmatch bc varg aarg -> + cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg). +Proof. + intros until aarg; intro VM. + destruct cond; simpl; eauto with va. +Qed. + Lemma symbol_address_sound: forall id ofs, vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)). @@ -236,12 +287,44 @@ Theorem eval_static_operation_sound: list_forall2 (vmatch bc) vargs aargs -> vmatch bc vres (eval_static_operation op aargs). Proof. - unfold eval_operation, eval_static_operation; intros; + unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros; destruct op; InvHyps; eauto with va. destruct (propagate_float_constants tt); constructor. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + (* select *) + - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption). + rewrite eval_select_to2. + unfold eval_select2. + inv Hcond; trivial; try constructor. + + apply binop_int_sound; assumption. + + destruct a1; destruct a0; try apply vmatch_ifptr_undef. + apply vmatch_ifptr_i. + + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef. + apply vmatch_ifptr_i. + (* selectl *) + - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption). + rewrite eval_selectl_to2. + unfold eval_selectl2. + inv Hcond; trivial; try constructor. + + apply binop_long_sound; assumption. + + destruct a1; destruct a0; try apply vmatch_ifptr_undef. + apply vmatch_ifptr_l. + + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef. + apply vmatch_ifptr_l. + (* selectf *) + - inv H2; simpl; try constructor. + + destruct (Int.eq _ _); apply binop_float_sound; trivial. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + (* selectfs *) + - inv H2; simpl; try constructor. + + destruct (Int.eq _ _); apply binop_single_sound; trivial. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. End SOUNDNESS. |