diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-04-06 18:32:27 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-04-06 18:32:27 +0000 |
| commit | 76f49ca6af4ffbc77c0ba7965d409c3de04011bd (patch) | |
| tree | d2167acae5dc5c02995fa12c30472a9e7d5a7d47 /ia32/Op.v | |
| parent | 6bad7ed856e016aab1d947c57d373baecf7c98c4 (diff) | |
Support Onot operator / notl instruction. More constant propagation during selection.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2451 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Op.v')
| -rw-r--r-- | ia32/Op.v | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -90,6 +90,7 @@ 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] *) | Oshl: operation (**r [rd = r1 << r2] *) | Oshlimm: int -> operation (**r [rd = r1 << n] *) | Oshr: operation (**r [rd = r1 >> r2] (signed) *) @@ -230,6 +231,7 @@ 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) | Oshl, v1::v2::nil => Some (Val.shl v1 v2) | Oshlimm n, v1::nil => Some (Val.shl v1 (Vint n)) | Oshr, v1::v2::nil => Some (Val.shr v1 v2) @@ -321,6 +323,7 @@ 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) | Oshl => (Tint :: Tint :: nil, Tint) | Oshlimm _ => (Tint :: nil, Tint) | Oshr => (Tint :: Tint :: nil, Tint) @@ -407,6 +410,7 @@ Proof with (try exact I). destruct v0... destruct v0; destruct v1... destruct v0... + destruct v0... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... @@ -835,6 +839,7 @@ 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. destruct (Int.ltu i0 Int.iwordsize); auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. |