diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-05-03 11:18:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-03 11:18:32 +0200 |
| commit | 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch) | |
| tree | 74500c845c99b39ba91a5507656060dea60404ea /arm/ConstpropOp.vp | |
| parent | 25ea686abc4cce13aba92196dbeb284f727b6e0e (diff) | |
| download | compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip | |
Hybrid 64bit/32bit PowerPC port
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
Diffstat (limited to 'arm/ConstpropOp.vp')
| -rw-r--r-- | arm/ConstpropOp.vp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index e0f0889f..cb7a73eb 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Static analysis and strength reduction for operators +(** Static analysis and strength reduction for operators and conditions. This is the machine-dependent part of [Constprop]. *) Require Import Coqlib. @@ -51,7 +51,7 @@ Definition eval_static_shift (s: shift) (n: int) : int := | Sror x => Int.ror n x end. -Nondetfunction cond_strength_reduction +Nondetfunction cond_strength_reduction (cond: condition) (args: list reg) (vl: list aval) := match cond, args, vl with | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => @@ -98,7 +98,7 @@ Nondetfunction cond_strength_reduction if Float32.eq_dec n2 Float32.zero then (Cnotcompfszero c, r1 :: nil) else (cond, args) - | _, _, _ => + | _, _, _ => (cond, args) end. @@ -206,7 +206,7 @@ Definition make_cast8signed (r: reg) (a: aval) := Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). -Nondetfunction op_strength_reduction +Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := match op, args, vl with | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1 |