aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
...
* | | fixes for aarch64 arm ppc ppc64David Monniaux2020-02-241-2/+6
|/ /
* | stubs to keep compiling on architectures not K1cDavid Monniaux2020-02-071-0/+3
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-12-094-6/+87
|\ \
| * | trapping opsDavid Monniaux2019-09-241-0/+24
| | |
| * | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-202-33/+34
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| * \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-101-18/+19
| |\ \ \ | | | | | | | | | | | | | | | mppa-non-trapping-load
| * | | | PowerPC compilesDavid Monniaux2019-09-075-22/+78
| | | | |
* | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-11-132-2/+4
|\ \ \ \ \ | |_|_|/ / |/| | | / | | |_|/ | |/| | mppa-work-upstream-merge
| * | | Model GPR0 in isel (#199)Xavier Leroy2019-09-172-2/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If the first argument to `isel` is GPR0, it reads as the constant 0. This cannot occur in code generated by CompCert, due to the fact that GPR0 is not available as register for register allocation. However the assembler semantics should be as close as possible to the actual hardware.
* | | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-202-33/+34
|\| | | | | | | | | | | | | | | mppa-work-upstream-merge
| * | | Reworked json export.Bernhard Schommer2019-09-121-31/+32
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions
| * | | Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-111-2/+2
| |\ \ \ | | |_|/ | |/| | | | | | Support target architecture AArch64 (ARMv8 in 64-bit mode)
| | * | Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
| | | | | | | | | | | | Some changes were not correctly propagated to all architectures.
* | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-09-101-4/+4
|\| | | | |_|/ |/| |
| * | Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-051-4/+4
| | |
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-283-0/+23
|\| | | | | | | | | | | mppa-work-upstream-merge
| * | Allow Long as const result for ppc64 variant.Bernhard Schommer2019-08-132-0/+3
| | | | | | | | | | | | Since the ppc64 has 64 bit registers it is okay to have a 64 bit constant result.
| * | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-0/+20
| |/ | | | | | | | | | | | | | | | | | | | | | | * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM.
* | various fixesDavid Monniaux2019-07-191-1/+0
| |
* | helpers broke compilationDavid Monniaux2019-07-192-15/+3
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-198-29/+125
|\| | | | | | | mppa-work-upstream-merge
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-15/+55
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-171-2/+2
| | | | | | | | | | | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
| * 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.
| * Extended asm: print register names according to their typesXavier Leroy2019-06-171-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open.
| * Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-172-2/+36
| | | | | | | | | | A conditional move whose condition is statically known becomes a regular move. Otherwise, the condition can sometimes be simplified by strength reduction.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-0316-108/+470
|\| | | | | | | mppa-if-conversion
| * Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-289-7/+101
| | | | | | | | | | | | The FP select for PowerPC stores both addresses in two subsequent stack slots and loads them using an offset created from the result of the comparison.
| * PowerPC: add SelectOp.select functionXavier Leroy2019-05-262-0/+31
| | | | | | | | | | This function and its proof should have been part of commit 43e7b67. They are already there for the other ports.
| * Emulate the "isel" instruction on non-EREF PPC processorsXavier Leroy2019-05-203-22/+42
| | | | | | | | | | On non-EREF processors it expands to instructions that destroy GPR0. Reflect this in the Asm semantics for Pisel.
| * Implement a `Osel` operation for PowerPCXavier Leroy2019-05-207-9/+106
| | | | | | | | | | This operation compiles down to an `isel` instruction (conditional move). The semantics is given by `Val.select`.
| * Give a semantics to the Pisel instructionXavier Leroy2019-05-201-1/+7
| |
| * PowerPC: make sure evaluation of conditions do not destroy any registerXavier Leroy2019-05-204-54/+155
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will be useful to implement a "select" (conditional move) operation later. - Introduce `Asmgen.loadimm64_notemp` to load a 64-bit integer constant into a register without going through memory and without needing a temporary register. - Use `Asmgen.loadimm64_notemp` instead of `Asmgen.loadimm64` in the compilation of conditions, so that GPR12 is no longer needed as a temporary. - Share code and proofs common to the two `Asmgen.loadimm64_` functions as the `Asmgen.loadimm64_32s` function.
| * Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-5/+14
| | | | | | | | | | | | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-262-9/+10
| | | | | | | | | | | | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
| * 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).
* | seems like powerpc runs but the result segfaultsDavid Monniaux2019-03-224-3/+36
| |
* | try to be portable across archsDavid Monniaux2019-03-212-0/+7
|/
* Fix typo in asmexpand. Bug 24953Bernhard Schommer2018-11-071-1/+1
|
* Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776Michael Schmidt2018-10-202-5/+10
|
* Switch conditions for eref plattforms.Bernhard Schommer2018-09-191-4/+4
| | | | | Otherwise an isel is generated if no isel is needed at all. Bug 24516
* Support __builtin_isel64 for non-EREF PPC64 platforms (#141)Xavier Leroy2018-09-181-22/+28
| | | | | | If the isel instruction is missing, it can be emulated just like we do in the 32-bit case (__builtin_isel). Follow-up to commit 51d32b92. Bug 24516
* Add builtin isel (conditional move) for int64, uint64 and _Bool (#140)Bernhard Schommer2018-09-182-1/+16
| | | | | New builtin isel variants to support conditional moves for 64bit integers and _Bool values. Bug 24516
* Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-141-1/+1
| | | | | | | | | | | | | | | | | | * bug 24268: avoid assertion after reporting error for invalid call to builtin_debug * bug 24268, remove duplicated warning tag in lexer messages * bug 24268, fix spelling in array element designator message * bug 24268, unify 'consider adding option ...' messages * bug 24268, add spacing for icbi operands * bug 24268, uniform use of Ignored_attributes class for identical warnings * bug 24268, unify message for 'assignment to const type' to error from error/fatal error * bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-122-6/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067
* Fix typo in pattern match of error case, bug 24326Michael Schmidt2018-08-221-1/+1
|
* Added Pldi to instr_size.Bernhard Schommer2018-08-011-0/+1
| | | | | | Since Pldi generates two instructions instr_size of Pldi should return 2. Bug 24218
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-012-3/+12
| | | | | | | | | | The semantics of external function calls in LTL, Linear, Mach and Asm now consider that all caller-save registers are set to Vundef by the call. This models that fact that the external function can modify those registers arbitrarily. Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes accordingly.
* Add missing tab character, bug 23541Michael Schmidt2018-05-021-1/+1
|
generated by cgit (git 2.34.1) at 2024-07-06 16:30:40 +0000