From 1f004665758e26e6e48d13f5702fe55af8944448 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 25 Oct 2016 15:11:30 +0200 Subject: Update ARM port. Not tested yet. --- arm/ConstpropOp.vp | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'arm/ConstpropOp.vp') 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. -- cgit