diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmblock.v | 17 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 1 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 14 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 111 | ||||
| -rw-r--r-- | mppa_k1c/Machregs.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/NeedOp.v | 45 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 55 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 10 | ||||
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 22 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 103 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 20 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 89 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 34 |
15 files changed, 456 insertions, 73 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 7afed212..245804f3 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -208,6 +208,7 @@ 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 *)
.
(** Correspondance between Asmblock and Asm *)
@@ -354,6 +355,7 @@ 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
(** ARRI32 *)
| PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b341388c..2fe27143 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -412,6 +412,7 @@ 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 *) . Inductive arith_name_arri32 : Type := @@ -1207,6 +1208,22 @@ 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 end. Definition arith_eval_arri32 n v1 v2 v3 := diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 500fc504..6d124556 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1433,6 +1433,7 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring := match n with | Pmaddw => "Pmaddw" | Pmaddl => "Pmaddl" + | Pcmove _ => "Pcmove" end. Definition string_of_name_arri32 (n: arith_name_arri32): pstring := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index c03e319c..cf0b2a0a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -729,6 +729,20 @@ Definition transl_op do rd <- ireg_of res; transl_cond_op cmp rd args k + | Oselect, 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) + + | Oselectl, 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 BTdnez r0 rS r1 ::i k) + | _, _ => Error(msg "Asmgenblock.transl_op") end. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 5486a497..16663522 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1558,6 +1558,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 -> @@ -1645,69 +1665,34 @@ 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 *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold select. + 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. +- (* Oselectl *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold selectl. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int64_eq_comm. + destruct (Int64.eq i Int64.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 4de37af4..2b3fb1aa 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -210,7 +210,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 => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 2577370c..a6ecb820 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 => op3 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -186,6 +187,46 @@ Proof. trivial. Qed. +Lemma select_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 (select v0 v1 v2) (select w0 w1 w2) x. +Proof. + unfold default; intros. + destruct x; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. +Qed. + +Lemma selectl_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 (selectl v0 v1 v2) (selectl 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. destruct nv; simpl; trivial. @@ -238,6 +279,10 @@ Proof. apply mull_sound; trivial. rewrite default_idem; trivial. rewrite default_idem; trivial. + (* select *) +- apply select_sound; trivial. + (* selectl *) +- apply selectl_sound; trivial. Qed. Lemma operation_is_redundant_sound: diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index c4338857..ec3f1077 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -181,7 +181,9 @@ 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 (**r [rd = if r3 then r2 else r1] *) + | Oselectl. (**r [rd = if r3 then r2 else r1] *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -250,6 +252,40 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | _, _ => None end. +Definition select (v0 : val) (v1 : val) (vselect : val) : val := + match vselect with + | Vint iselect => + match v0 with + | Vint i0 => + match v1 with + | Vint i1 => + Vint (if Int.cmp Ceq Int.zero iselect + then i0 + else i1) + | _ => Vundef + end + | _ => Vundef + end + | _ => Vundef + end. + +Definition selectl (v0 : val) (v1 : val) (vselect : val) : val := + match vselect with + | Vlong iselect => + match v0 with + | Vlong i0 => + match v1 with + | Vlong i1 => + Vlong (if Int64.cmp Ceq Int64.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) (op: operation) (vl: list val) (m: mem): option val := @@ -378,6 +414,8 @@ 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, v0::v1::vselect::nil => Some (select v0 v1 vselect) + | Oselectl, v0::v1::vselect::nil => Some (selectl v0 v1 vselect) | _, _ => None end. @@ -565,6 +603,9 @@ 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 => (Tint :: Tint :: Tint :: nil, Tint) + | Oselectl => (Tlong :: Tlong :: Tlong :: nil, Tlong) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -799,6 +840,10 @@ 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; destruct v2; simpl in *; try discriminate; trivial. + (* selectl *) + - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. Qed. End SOUNDNESS. @@ -1324,6 +1369,14 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + (* select *) + - inv H3; simpl; try constructor. + inv H4; simpl; try constructor. + inv H2; simpl; constructor. + (* selectl *) + - 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 56b00c7e..9e6e819c 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -128,6 +128,7 @@ let arith_rri64_str = function let arith_arrr_str = function | Pmaddw -> "Pmaddw" | Pmaddl -> "Pmaddl" + | Pcmove _ -> "Pcmove" let arith_ri32_str = "Pmake" @@ -415,7 +416,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 @@ -482,7 +483,8 @@ let ab_inst_to_real = function | "Pfixedudrzz" -> Fixedudz | "Pfixeddrzz_i32" -> Fixeddz | "Pfixedudrzz_i32" -> Fixedudz - + | "Pcmove" -> Cmoved + | "Plb" -> Lbs | "Plbu" -> Lbz | "Plh" -> Lhs @@ -531,7 +533,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) @@ -584,7 +586,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 0c3618d7..6c34de19 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 @@ -278,8 +286,20 @@ Nondetfunction orl (e1: expr) (e2: expr) := | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) + | (Eop Oandl ((Eop Ocast32signed + ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0)) + (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)), + (Eop Oandl ((Eop Ocast32signed + ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1)) + (y1:::Enil)):::Enil)):::Enil)):::v1:::Enil)) => + if same_expr_pure y0 y1 + && Int64.eq zero0 Int64.zero + && Int64.eq zero1 Int64.zero + then Eop Oselectl (v0:::v1:::y0:::Enil) + else Eop Oorl (e1:::e2:::Enil) | _, _ => Eop Oorl (e1:::e2:::Enil) end. + 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 79187338..dd4cfa69 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,80 @@ 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 f6605c11..13650a2c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -275,7 +275,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 Eop Oselect (v0:::v1:::y0:::Enil) + 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 Eop Oselect (v0:::v1:::y0:::Enil) + 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 89af39ee..d35c4b6d 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,82 @@ 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 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. + rewrite (Val.and_commut _ v5). + destruct v5; simpl; trivial. + rewrite (Val.and_commut _ v9). + rewrite Val.or_commut. + destruct v9; simpl; trivial. + rewrite int_eq_commut. + destruct (Int.eq i1 Int.zero); simpl. + + rewrite Int.and_zero. + rewrite Int.or_commut. + rewrite Int.or_zero. + rewrite Int.and_mone. + reflexivity. + + rewrite Int.and_mone. + rewrite Int.neg_zero. + rewrite Int.and_zero. + 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 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. + rewrite (Val.and_commut _ v5). + destruct v5; simpl; trivial. + rewrite (Val.and_commut _ v9). + rewrite Val.or_commut. + destruct v9; simpl; trivial. + rewrite int_eq_commut. + destruct (Int.eq i1 Int.zero); simpl. + + rewrite Int.and_zero. + rewrite Int.or_commut. + rewrite Int.or_zero. + rewrite Int.and_mone. + reflexivity. + + rewrite Int.and_mone. + rewrite Int.neg_zero. + rewrite Int.and_zero. + rewrite Int.or_zero. + reflexivity. - apply DEFAULT. Qed. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 41a6622a..4be94390 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -504,6 +504,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) -> + 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 fb1977ea..a3843301 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -41,6 +41,24 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := | _, _ => Vbot end. +Definition select (v0 v1 vselect : aval) : aval := + match vselect with + | I iselect => + if Int.eq Int.zero iselect + then binop_int (fun x0 x1 => x0) v0 v1 + else binop_int (fun x0 x1 => x1) v0 v1 + | _ => Vtop + end. + +Definition selectl (v0 v1 vselect : aval) : aval := + match vselect with + | L iselect => + if Int64.eq Int64.zero iselect + then binop_long (fun x0 x1 => x0) v0 v1 + else binop_long (fun x0 x1 => x1) v0 v1 + | _ => Vtop + end. + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -165,6 +183,8 @@ 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, v0::v1::vselect::nil => select v0 v1 vselect + | Oselectl, v0::v1::vselect::nil => selectl v0 v1 vselect | _, _ => Vbot end. @@ -241,6 +261,20 @@ 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. + (* select *) + - inv H2; simpl; try constructor. + + destruct (Int.eq _ _); apply binop_int_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. + (* selectl *) + - inv H2; simpl; try constructor. + + destruct (Int64.eq _ _); apply binop_long_sound; trivial. + + destruct (Int64.eq _ _); + destruct a1; destruct a0; eauto; constructor. Qed. End SOUNDNESS. |