From 91dcfe11ff321386f7924da053be83523073a50c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 24 Feb 2012 15:49:19 +0000 Subject: Improved instruction selection for "notint". powerpc/PrintAsm.ml: fixed MacOS X problems with malloc and free git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1824 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgen.v | 6 ++++++ powerpc/Asmgenproof1.v | 5 +++++ powerpc/Op.v | 15 +++++++++++++++ powerpc/PrintAsm.ml | 4 ++-- powerpc/PrintOp.ml | 3 +++ powerpc/SelectOp.vp | 12 +++++++++++- powerpc/SelectOpproof.v | 27 +++++++++++++++++++-------- 7 files changed, 61 insertions(+), 11 deletions(-) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 6d1a1fc0..b166d34c 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -350,12 +350,18 @@ Definition transl_op Pxor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Oxorimm n, a1 :: nil => xorimm (ireg_of r) (ireg_of a1) n k + | Onot, a1 :: nil => + Pnor (ireg_of r) (ireg_of a1) (ireg_of a1) :: k | Onand, a1 :: a2 :: nil => Pnand (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Onor, a1 :: a2 :: nil => Pnor (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Onxor, a1 :: a2 :: nil => Peqv (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oandc, a1 :: a2 :: nil => + Pandc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k + | Oorc, a1 :: a2 :: nil => + Porc (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Oshl, a1 :: a2 :: nil => Pslw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Oshr, a1 :: a2 :: nil => diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 77a19aff..2af4f700 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1340,6 +1340,11 @@ Opaque Val.add. (* Oxorimm *) destruct (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. exists rs'; auto with ppcgen. + (* Onor *) + replace (Val.notint (rs (ireg_of m0))) + with (Val.notint (Val.or (rs (ireg_of m0)) (rs (ireg_of m0)))). + TranslOpSimpl. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.or_idem. auto. (* Oshrximm *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. diff --git a/powerpc/Op.v b/powerpc/Op.v index d2b7ed59..64e47e32 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -74,9 +74,12 @@ Inductive operation : Type := | Oorimm: int -> operation (**r [rd = r1 | n] *) | Oxor: operation (**r [rd = r1 ^ r2] *) | Oxorimm: int -> operation (**r [rd = r1 ^ n] *) + | Onot: operation (**r [rd = ~r1] *) | Onand: operation (**r [rd = ~(r1 & r2)] *) | Onor: operation (**r [rd = ~(r1 | r2)] *) | Onxor: operation (**r [rd = ~(r1 ^ r2)] *) + | Oandc: operation (**r [rd = r1 & ~r2] *) + | Oorc: operation (**r [rd = r1 | ~r2] *) | Oshl: operation (**r [rd = r1 << r2] *) | Oshr: operation (**r [rd = r1 >> r2] (signed) *) | Oshrimm: int -> operation (**r [rd = r1 >> n] (signed) *) @@ -180,9 +183,12 @@ Definition eval_operation | Oorimm n, v1::nil => Some (Val.or v1 (Vint n)) | Oxor, v1::v2::nil => Some(Val.xor v1 v2) | Oxorimm n, v1::nil => Some (Val.xor v1 (Vint n)) + | Onot, v1::nil => Some(Val.notint v1) | Onand, v1::v2::nil => Some (Val.notint (Val.and v1 v2)) | Onor, v1::v2::nil => Some (Val.notint (Val.or v1 v2)) | Onxor, v1::v2::nil => Some (Val.notint (Val.xor v1 v2)) + | Oandc, v1::v2::nil => Some (Val.and v1 (Val.notint v2)) + | Oorc, v1::v2::nil => Some (Val.or v1 (Val.notint v2)) | Oshl, v1::v2::nil => Some (Val.shl v1 v2) | Oshr, v1::v2::nil => Some (Val.shr v1 v2) | Oshrimm n, v1::nil => Some (Val.shr v1 (Vint n)) @@ -267,9 +273,12 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oorimm _ => (Tint :: nil, Tint) | Oxor => (Tint :: Tint :: nil, Tint) | Oxorimm _ => (Tint :: nil, Tint) + | Onot => (Tint :: nil, Tint) | Onand => (Tint :: Tint :: nil, Tint) | Onor => (Tint :: Tint :: nil, Tint) | Onxor => (Tint :: Tint :: nil, Tint) + | Oandc => (Tint :: Tint :: nil, Tint) + | Oorc => (Tint :: Tint :: nil, Tint) | Oshl => (Tint :: Tint :: nil, Tint) | Oshr => (Tint :: Tint :: nil, Tint) | Oshrimm _ => (Tint :: nil, Tint) @@ -338,6 +347,9 @@ Proof with (try exact I). destruct v0... destruct v0; destruct v1... destruct v0... + destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... @@ -765,6 +777,9 @@ Proof. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index f396a235..8323d56f 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -1049,7 +1049,7 @@ let print_fundef oc (name, defn) = match defn with | Internal code -> print_function oc name code - | External (EF_external _ as ef) -> + | External ((EF_external _ | EF_malloc | EF_free) as ef) -> if function_needs_stub name then stub_function oc name (ef_sig ef) | External _ -> () @@ -1057,7 +1057,7 @@ let print_fundef oc (name, defn) = let record_extfun (name, defn) = match defn with | Internal _ -> () - | External (EF_external _) -> + | External (EF_external _ | EF_malloc | EF_free) -> if function_needs_stub name then stubbed_functions := IdentSet.add name !stubbed_functions | External _ -> () diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 3b5e98d2..13eb4aee 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -69,9 +69,12 @@ let print_operation reg pp = function | Oorimm n, [r1] -> fprintf pp "%a | %ld" reg r1 (camlint_of_coqint n) | Oxor, [r1;r2] -> fprintf pp "%a ^ %a" reg r1 reg r2 | Oxorimm n, [r1] -> fprintf pp "%a ^ %ld" reg r1 (camlint_of_coqint n) + | Onot, [r1] -> fprintf pp "not(%a)" reg r1 | Onand, [r1;r2] -> fprintf pp "not(%a & %a)" reg r1 reg r2 | Onor, [r1;r2] -> fprintf pp "not(%a | %a)" reg r1 reg r2 | Onxor, [r1;r2] -> fprintf pp "not(%a ^ %a)" reg r1 reg r2 + | Oandc, [r1;r2] -> fprintf pp "%a & not %a" reg r1 reg r2 + | Oorc, [r1;r2] -> fprintf pp "%a | not %a" reg r1 reg r2 | Oshl, [r1;r2] -> fprintf pp "%a << %a" reg r1 reg r2 | Oshr, [r1;r2] -> fprintf pp "%a >>s %a" reg r1 reg r2 | Oshrimm n, [r1] -> fprintf pp "%a >>s %ld" reg r1 (camlint_of_coqint n) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 08968f7c..290704bc 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -63,10 +63,16 @@ Definition addrstack (ofs: int) := Nondetfunction notint (e: expr) := match e with | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil + | Eop Onot (t1:::Enil) => t1 | Eop Oand (t1:::t2:::Enil) => Eop Onand (t1:::t2:::Enil) | Eop Oor (t1:::t2:::Enil) => Eop Onor (t1:::t2:::Enil) | Eop Oxor (t1:::t2:::Enil) => Eop Onxor (t1:::t2:::Enil) - | _ => Elet e (Eop Onor (Eletvar O ::: Eletvar O ::: Enil)) + | Eop Onand (t1:::t2:::Enil) => Eop Oand (t1:::t2:::Enil) + | Eop Onor (t1:::t2:::Enil) => Eop Oor (t1:::t2:::Enil) + | Eop Onxor (t1:::t2:::Enil) => Eop Oxor (t1:::t2:::Enil) + | Eop Oandc (t1:::t2:::Enil) => Eop Oorc (t2:::t1:::Enil) + | Eop Oorc (t1:::t2:::Enil) => Eop Oandc (t2:::t1:::Enil) + | _ => Eop Onot (e:::Enil) end. (** ** Boolean value and boolean negation *) @@ -248,6 +254,8 @@ Nondetfunction and (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => andimm n1 t2 | t1, Eop (Ointconst n2) Enil => andimm n2 t1 + | Eop Onot (t1:::Enil), t2 => Eop Oandc (t2:::t1:::Enil) + | t1, Eop Onot (t2:::Enil) => Eop Oandc (t1:::t2:::Enil) | _, _ => Eop Oand (e1:::e2:::Enil) end. @@ -280,6 +288,8 @@ Nondetfunction or (e1: expr) (e2: expr) := else Eop Oor (e1:::e2:::Enil) | Eop (Ointconst n1) Enil, t2 => orimm n1 t2 | t1, Eop (Ointconst n2) Enil => orimm n2 t1 + | Eop Onot (t1:::Enil), t2 => Eop Oorc (t2:::t1:::Enil) + | t1, Eop Onot (t2:::Enil) => Eop Oorc (t1:::t2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 59f2a419..39205dbd 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -134,18 +134,24 @@ Qed. Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. + assert (forall v, Val.lessdef (Val.notint (Val.notint v)) v). + destruct v; simpl; auto. rewrite Int.not_involutive; auto. unfold notint; red; intros until x; case (notint_match a); intros; InvEval. - TrivialExists. + TrivialExists. + subst. exists v1; split; auto. subst. TrivialExists. subst. TrivialExists. subst. TrivialExists. - econstructor; split; eauto. - eapply eval_Elet. eexact H. - eapply eval_Eop. - eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - apply eval_Enil. - simpl. destruct x; simpl; auto. rewrite Int.or_idem. auto. + subst. exists (Val.and v1 v0); split; auto. EvalOp. + subst. exists (Val.or v1 v0); split; auto. EvalOp. + subst. exists (Val.xor v1 v0); split; auto. EvalOp. + subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp. + destruct v0; destruct v1; simpl; auto. rewrite Int.not_and_or_not. rewrite Int.not_involutive. + rewrite Int.or_commut. auto. + subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. + destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive. + rewrite Int.and_commut. auto. + TrivialExists. Qed. Theorem eval_boolval: unary_constructor_sound boolval Val.boolval. @@ -407,6 +413,8 @@ Proof. red; intros until y; unfold and; case (and_match a b); intros; InvEval. rewrite Val.and_commut. apply eval_andimm; auto. apply eval_andimm; auto. + subst. rewrite Val.and_commut. TrivialExists. + subst. TrivialExists. TrivialExists. Qed. @@ -460,6 +468,9 @@ Proof. (* intconst *) InvEval. rewrite Val.or_commut. apply eval_orimm; auto. InvEval. apply eval_orimm; auto. +(* orc *) + InvEval. subst. rewrite Val.or_commut. TrivialExists. + InvEval. subst. TrivialExists. (* default *) TrivialExists. Qed. -- cgit