diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-10 09:00:24 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-10 09:00:24 +0000 |
commit | 9e76f90bc5255d6ec933d705bf99baf3ca80d5d5 (patch) | |
tree | 4f479cbabeab8dae4b3c4419d6ecafd64976f60d /arm/CombineOp.v | |
parent | 39fefdbe35d14d063e71738a70deebbae896eb06 (diff) | |
download | compcert-9e76f90bc5255d6ec933d705bf99baf3ca80d5d5.tar.gz compcert-9e76f90bc5255d6ec933d705bf99baf3ca80d5d5.zip |
Updated ARM port.
CSE.v: removed commented-out stuff.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1966 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/CombineOp.v')
-rw-r--r-- | arm/CombineOp.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/arm/CombineOp.v b/arm/CombineOp.v index be9824bc..fd347c1b 100644 --- a/arm/CombineOp.v +++ b/arm/CombineOp.v @@ -74,13 +74,16 @@ Function combine_cond (cond: condition) (args: list valnum) : option(condition * | _, _ => None end. +(* Problem: on ARM, not all load/store instructions accept the Aindexed2 + and Aindexed2shift addressing modes. For the time being, + avoid producing them. *) + Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) := match addr, args with | Aindexed n, x::nil => match get x with - | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys) - | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None - | Some(Op (Oaddshift s) ys) => if Int.eq_dec n Int.zero then Some(Aindexed2shift s, ys) else None + | Some(Op (Oaddimm m) ys) => + Some(Aindexed (Int.add m n), ys) | _ => None end | _, _ => None |