diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:26:46 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:26:46 +0200 |
commit | 3bef0962079cf971673b4267b0142bd5fe092509 (patch) | |
tree | 6dd283fa6b8305d960fd08938fbbd09e0940c139 /powerpc/ConstpropOp.vp | |
parent | e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (diff) | |
download | compcert-kvx-3bef0962079cf971673b4267b0142bd5fe092509.tar.gz compcert-kvx-3bef0962079cf971673b4267b0142bd5fe092509.zip |
Support for 64-bit architectures: update the PowerPC port
The PowerPC port remains 32-bit only, no support is added for PPC 64.
This shows how much work is needed to update an existing port a minima.
Diffstat (limited to 'powerpc/ConstpropOp.vp')
-rw-r--r-- | powerpc/ConstpropOp.vp | 38 |
1 files changed, 24 insertions, 14 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 7265337d..e768e4a9 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -13,15 +13,25 @@ (** Strength reduction for operators and conditions. This is the machine-dependent part of [Constprop]. *) -Require Import Coqlib. -Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import Registers. +Require Import Coqlib Compopts. +Require Import AST Integers Floats. +Require Import Op Registers. Require Import ValueDomain. +(** * Converting known values to constants *) + +Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) + +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 @@ -187,13 +197,13 @@ Nondetfunction addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with | Aindexed2, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil => - (Aglobal symb (Int.add n1 n2), nil) + (Aglobal symb (Ptrofs.add n1 (Ptrofs.of_int n2)), nil) | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Gl symb n2) :: nil => - (Aglobal symb (Int.add n1 n2), nil) + (Aglobal symb (Ptrofs.add (Ptrofs.of_int n1) n2), nil) | 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, Ptr(Gl symb n1) :: v2 :: nil => (Abased symb n1, r2 :: nil) | Aindexed2, r1 :: r2 :: nil, v1 :: Ptr(Gl symb n2) :: nil => @@ -203,11 +213,11 @@ Nondetfunction addr_strength_reduction | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Aindexed n2, r1 :: nil) | Abased symb ofs, r1 :: nil, I n1 :: nil => - (Aglobal symb (Int.add ofs n1), nil) + (Aglobal symb (Ptrofs.add ofs (Ptrofs.of_int n1)), nil) | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => - (Aglobal symb (Int.add n1 n), nil) + (Aglobal symb (Ptrofs.add n1 (Ptrofs.of_int n)), 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. |