From 76f49ca6af4ffbc77c0ba7965d409c3de04011bd Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 6 Apr 2014 18:32:27 +0000 Subject: 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 --- ia32/Op.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'ia32/Op.v') diff --git a/ia32/Op.v b/ia32/Op.v index 26e6688..5420607 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -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. -- cgit v1.2.3