diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-24 15:49:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-24 15:49:19 +0000 |
| commit | 91dcfe11ff321386f7924da053be83523073a50c (patch) | |
| tree | dc8291da94c66665ca8dd2496cdd74e32e08ae92 /powerpc/Op.v | |
| parent | 0e76ac320601a81a67c700759526d0f8b7a8ed7b (diff) | |
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
Diffstat (limited to 'powerpc/Op.v')
| -rw-r--r-- | powerpc/Op.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/powerpc/Op.v b/powerpc/Op.v index d2b7ed5..64e47e3 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. |