aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Archi.v
Commit message (Collapse)AuthorAgeFilesLines
* Introduce float_conversion_default_nan parameter for float-float conversionsBernhard Schommer2022-04-251-1/+4
| | | | | | | | | | | | | For RISC-V we need to return the canonical NaN value if the argument of a float32->float64 or float64->float32 conversion is any NaN. This is in line with 11.3 from the RISC-V manual, the description of the conversion operations as well as what the spike ISA simulator and qemu do. Other platforms convert the NaN payload (by truncation or expansion) in float32->float64 and float64->float32 conversions. Fixes: #428
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
| | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
|
* Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-021-0/+3
| | | | | | | | | GCC does passes single arguments as singles on the stack but diab and the eabi say single arguments should be passed as double on the stack. This commit changes the alignment of single arguments to 4 for gcc based backends.
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-0/+5
| | | | | | | | We just lift the corresponding functions from Flocq and add the computation of NaN payloads. NaN payloads for FMA are described in the ARM and RISC-V specifications, and were determined experimentally for x86 and for Power.
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-13/+17
| | | | | | | | | | | | | | When an FP arithmetic instruction produces a NaN result, the payload of this NaN depends on the architecture. Before, the payload behavior was specified by 3 architecture-dependent parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32` and `Archi.fpu_results_default_qNaN`. This was adequate for two-argument operations, but doesn't extend to FMA. In preparation for FMA support, this commit generalizes the `Archi.choose` functions from two arguments to any number of arguments. In passing, `Archi.fpu_results_default_qNaN` is no longer needed.
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-11/+14
| | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-6/+6
| | | | | | | | | | | | | 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.
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-3/+12
| | | | | 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.
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-3/+2
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-2/+2
|
* Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-0/+4
| | | | | | Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-281-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-231-3/+11
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC is big-endian, dammit.xleroy2014-02-211-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2412 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-0/+34
- endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 00:30:37 +0000