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

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.