summaryrefslogtreecommitdiff
path: root/arm/CombineOp.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-01-02 15:59:11 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-01-02 15:59:11 +0000
commit29e0c9b2c99a437fc9dfab66e1abdd546a5308d6 (patch)
tree2c3e924125d9b91e5e9b57b87c80f5b5ce9c6710 /arm/CombineOp.v
parentc71e155dbbf34fa17d14e8eee50a019c8ccfd6f5 (diff)
Updated ARM backend wrt new static analyses and optimizations.
NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/CombineOp.v')
-rw-r--r--arm/CombineOp.v12
1 files changed, 4 insertions, 8 deletions
diff --git a/arm/CombineOp.v b/arm/CombineOp.v
index fd347c1..8da6e3a 100644
--- a/arm/CombineOp.v
+++ b/arm/CombineOp.v
@@ -17,13 +17,7 @@ Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Op.
-Require SelectOp.
-
-Definition valnum := positive.
-
-Inductive rhs : Type :=
- | Op: operation -> list valnum -> rhs
- | Load: memory_chunk -> addressing -> list valnum -> rhs.
+Require Import CSEdomain.
Section COMBINE.
@@ -104,7 +98,9 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
end
| Oandimm n, x :: nil =>
match get x with
- | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
+ | Some(Op (Oandimm m) ys) =>
+ Some(let p := Int.and m n in
+ if Int.eq p m then (Omove, x :: nil) else (Oandimm p, ys))
| _ => None
end
| Oorimm n, x :: nil =>