aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
* Fix regression on PowerPC / DiabXavier Leroy2021-02-231-2/+4
| | | | | | | | | | | | | On PowerPC/Diab, common declarations must not be used for small data sections. Add a `~common` option to `PrintAsmaux.variable_section` to control the use of common declarations. The default is whatever is specified on the command line using the `-fcommon` and `-fno-common` options. Use `~common:false` for `Section_small_data` on PowerPC / Diab. Note that on PowerPC/Linux, GCC uses common declarations for uninitialized variables in small data section, so we keep doing this in CompCert as well.
* Section handling: finer control of variable initializationXavier Leroy2021-02-231-1/+1
| | | | | | | | | | | | | Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8.
* Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-14/+8
| | | | | | | This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data.
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-212-8/+8
| | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to pass arguments that are not normalized.
* PowerPC: wrong computation of the position of the first vararg argumentXavier Leroy2021-01-151-2/+3
| | | | | | | | | In function Asmexpand.next_arg_locations: If 7 integer parameter passing registers have been used already, and the next fixed arguments are Tlong then Tint, the Tlong argument was correctly analyzed as being passed on the stack, but the Tint argument was incorrectly analyzed as being passed in the 8th register.
* Replace `omega` tactic with `lia`, continuedXavier Leroy2021-01-131-1/+1
| | | | Follow-up to aba0e740f
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-299-81/+81
| | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-1/+1
| | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | Inlined built-in functions destroy GPR0
* Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat PowerPC operations. The pseudoinstructions were used to implement these operations, as follows: Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64 Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64 Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32 These pseudoinstructions were expanded (in Asmexpand.ml) in terms of Pfcfid : signed int64 -> float64 Pfctidz : float64 -> signed int64 and int32/int64 conversions. This commit performs this expansion during instruction selection (SelectOp.vp): floatofint(n) becomes floatoflong(longofint(n)) floatofintu(n) becomes floatoflong(longuofint(n)) intuoffloat(n) becomes cast32unsigned(longoffloat(n)) Then there is no need for the 3 removed operations and the 3 removed pseudoinstructions. More importantly, the correctness of these expansions is now proved as part of instruction selection, using the corresponding results from Floats.v.
* Added semantics for the PowerPC sel and mulh built-insBernhard Schommer2020-11-071-4/+44
| | | | | | | | The semantics of the various selection functions are defined analogously to the ones from the type generic sel function. The semantics for the various high word multiplication functions is defined using the Integer functions. Bug 30035
* Added missing printer for PowerPC 64 bit comparison.Bernhard Schommer2020-11-061-0/+8
| | | | | These comparisons are supported in the hybrid 64 bit mode. Bug 30035
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
* Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-12/+0
| | | | These functions are now available on all targets.
* No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | | | __builtin_fabs has already been expanded in backend/Selection.v .
* Added asserts for constraints of PowerPC builtinsBernhard Schommer2020-07-011-0/+6
|
* Fix typo in name of builtin function.Bernhard Schommer2020-07-011-1/+1
|
* Move shared code in new file.Bernhard Schommer2020-06-282-18/+0
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-282-5/+0
| | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
|
* In strict PPC ABI mode, pass single FP on stack in double FP formatXavier Leroy2020-03-021-2/+2
| | | | | | | | | | The EABI and the SVR4 ABI state that single-precision FP arguments passed on stack are passed as a 64-bit word, extended to double-precision. This commit implements this behavior by using a stack slot of type Tany64. Not only this ensures that the slot is of size and alignment 8 bytes, but it also ensures that it is accessed by stfd and lfd instructions, using single-extended-to-double format.
* Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-023-3/+20
| | | | | | | | | 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.
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-126/+0
| | | | | | | | | | | | | | The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions.
* Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+6
| | | | | | | | | | | | | | | | | | | | | | | | | Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized.
* Refine the type of function results in AST.signatureXavier Leroy2020-02-213-17/+15
| | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* 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.
* 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.
* | Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-051-4/+4
| |
* | 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.
* 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.
* 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).
generated by cgit (git 2.34.1) at 2024-06-26 18:59:38 +0000