Update ARM port. Not tested yet.

1 files changed, 16 insertions, 4 deletions

diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 872493a6..e0f0889f 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -22,6 +22,18 @@ Require Import Op.
 Require Import Registers.
 Require Import ValueDomain.
 
+(** * Converting known values to constants *)
+
+Definition const_for_result (a: aval) : option operation :=
+  match a with
+  | I n => Some(Ointconst n)
+  | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
+  | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
+  | Ptr(Gl id ofs) => Some (Oaddrsymbol id ofs)
+  | Ptr(Stk ofs) => Some(Oaddrstack ofs)
+  | _ => None
+  end.
+
 (** * Operator strength reduction *)
 
 (** We now define auxiliary functions for strength reduction of
@@ -237,19 +249,19 @@ Nondetfunction addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
   | Aindexed2, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil =>
-      (Ainstack (Int.add n1 n2), nil)
+      (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n2)), nil)
   | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil =>
-      (Ainstack (Int.add n1 n2), nil)
+      (Ainstack (Ptrofs.add (Ptrofs.of_int n1) n2), nil)
   | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
       (Aindexed n1, r2 :: nil)
   | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed n2, r1 :: nil)
   | Aindexed2shift s, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil =>
-      (Ainstack (Int.add n1 (eval_static_shift s n2)), nil)
+      (Ainstack (Ptrofs.add n1 (Ptrofs.of_int (eval_static_shift s n2))), nil)
   | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed (eval_static_shift s n2), r1 :: nil)
   | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil =>
-      (Ainstack (Int.add n1 n), nil)
+      (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n)), nil)
   | _, _, _ =>
       (addr, args)
   end.