aboutsummaryrefslogtreecommitdiffstats
path: root/x86
Commit message (Collapse)AuthorAgeFilesLines
* Section handling: finer control of variable initializationXavier Leroy2021-02-231-4/+3
| | | | | | | | | | | | | 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-6/+6
| | | | | | | 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-211-1/+1
| | | | | | | 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`.
* "macosx" is now called "macos"Xavier Leroy2021-01-182-2/+2
| | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-297-60/+60
| | | | | | | | | | | 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-2/+2
| | | | | | 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.
* x86 32 bits: ABI non-conformance for functions returning structs/unionsXavier Leroy2020-12-111-1/+1
| | | | | | | | The wrong value was returned in EAX, instead of the address of the struct/union. Report and fix by Zhenguo Yin. Fixes: #377
* Support Cygwin 64 bitsXavier Leroy2020-10-059-90/+296
| | | | | | - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
* Remove support for x86-32 under macOSXavier Leroy2020-07-291-21/+3
| | | | | | | 32-bit executables cannot be built since XCode 10.0 (sep 2018). 32-bit executables cannot be executed since MacOS 10.15 (oct 2019). Better remove x86-32 support and fail at configuration time instead of at the end of the build.
* 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-13/+0
| | | | These functions are now available on all targets.
* No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-4/+0
| | | | __builtin_fabs has already been expanded in backend/Selection.v .
* 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-3/+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.
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-242-146/+1
| | | | | | | | | | | | | | 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/+14
| | | | | | | | | | | | | | | | | | | | | | | | | 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-19/+17
| | | | | | | | | | 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.
* Remove __builtin_nop from list of x86 builtins.Bernhard Schommer2020-01-031-3/+0
|
* Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-034-0/+10
| | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
* Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-214-10/+0
| | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
* Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-111-4/+4
|\ | | | | | | Support target architecture AArch64 (ARMv8 in 64-bit mode)
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-4/+4
| | | | | | Some changes were not correctly propagated to all architectures.
| * x86: wrong expansion of __builtin_fmadd et alXavier Leroy2019-08-071-13/+19
| | | | | | | | | | | | | | | | | | | | | | | | There was a misunderstanding on the asm syntax for 3-operand instructions such as vfmadd132: when the Intel manual reads vfmadd132 res, arg2, arg3 the corresponding GNU asm syntax is vfmadd132 arg3, arg2, res but not vfmadd132 arg2, arg3, res Closes: #188
* | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-2/+0
| | | | | | | | | | | | | | | | | | | | | | | | * 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.
* | x86: wrong expansion of __builtin_fmadd et alXavier Leroy2019-08-061-13/+19
|/ | | | | | | | | | | | There was a misunderstanding on the asm syntax for 3-operand instructions such as vfmadd132: when the Intel manual reads vfmadd132 res, arg2, arg3 the corresponding GNU asm syntax is vfmadd132 arg3, arg2, res but not vfmadd132 arg2, arg3, res Closes: #188
* x86_64: branchless implementation of floatofintu and intuoffloatXavier Leroy2019-07-172-14/+29
| | | | | | | The implementation uses float <-> signed 64-bit integer conversion instructions, and is both efficient and branchless. Based on a suggestion by Rémi Hutin.
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-10/+75
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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()`.
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-3/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-1/+1
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Implement a `Osel` operation for x86Xavier Leroy2019-05-2011-38/+298
| | | | The operation compiles down to conditional moves.
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-6/+6
| | | | | | | | | | 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.
* x86: wrong modeling of ZF flag for FP comparisonsXavier Leroy2018-12-202-130/+66
| | | | | | | | | | | | | | As written in the comment, ZF should be set if the two floats are equal or unordered. The "or unordered" case was missing in the original modeling of FP comparisons. - Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions. - Update the proofs in Asmgenproof1 accordingly. No change required to the code generated for FP comparisons: this code already anticipated the "or unordered" case. Problem reported by Alix Trieu.
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-123-6/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | * 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 expansion of ctzl/clzl builtin for 64bit targets (#127)Michael Schmidt2018-07-121-2/+15
| | | | bug 24105, issue #243: expand correct version of ctzl/clzl builtin when long type is 64bit wide
* 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.
* Fix register naming for stack pointer.Bernhard Schommer2018-03-081-3/+4
| | | | | | It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and 'sp' for riscV. Bug 23176.
* Removed % prefix from ais annot register names.Bernhard Schommer2018-03-081-1/+18
| | | | | Registers should not contain the % prefix for ais annotations. Bug 23176
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-5/+5
| | | | | | | | | | | | | | | | | | The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-162-15/+49
| | | | | | | | | | | | | | | | | | | When x is known to be either 0 or 1, comparisons such as x == 0 x != 0 x == 1 x != 1 can be optimized away. This optimization was already performed for signed comparisons. This commit extends the optimization to unsigned comparisons as well. Additionally, for PowerPC only, some unsigned (dis)equality comparisons are turned into signed comparisons when we know it makes no difference, i.e. when both arguments are guaranteed not to be pointers. The reason is that Asmgen can produce shorter instruction sequences for some signed equality comparisons than for the corresponding unsigned comparisons. It's important to optimize unsigned integer comparisons because casts to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons. In particular, cascades of casts to _Bool are now reduced to a single cast much more often than before.
* Switching the cases seems to work on x86_32Bernhard Schommer2018-02-121-2/+2
|
* In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bitsXavier Leroy2018-02-123-11/+33
| | | | | | | | | | | | | In 32-bit mode, a symbolic reference "symbol + ofs" (address of "symbol" plus "ofs" bytes) can always be resolved by the linker into a 32-bit quantity that fits the 32-bit displacement field of x86 addressing modes. Not so in 64-bit mode: first, the displacement field is still 32 bits but the full address is 64 bits; second, the displacement is relative to the RIP instruction pointer. In the "small code model" that CompCert uses for x86-64, excessively large offsets lead to link-time overflows of this 32-bit displacement field. This commit addresses the issue by limiting the "ofs" part of "symbol + ofs" global addressing models to the range [-2^24, 2^24 - 1]. As explained in the AMD64 ELF ABI document, this is a safe range in the small code model, under the assumption that no global symbol is bigger than 2^24 bytes. GCC seems to be using a wider range [-2^31, 2^24 - 1] but I'd rather be safe. The limitation of the "ofs" offset is achieved by extending the mechanisms already present to ensure that "ofs" in "reg + ofs" indexed addressing modes fits in 32-bit signed: - Op.addressing_valid checks that the "ofs" part of "symbol + ofs" addressing modes is in the correct interval; - SelectOp.addressing turns invalid addressings into lea's + indexed addressings; - Asmgen.normalize_addrmode_64 turns lea's with invalid addressings into simpler lea's + addq of the large offset.
* x86 ConstpropOp.addr_strength_reduction: always check validity of resulting ↵Xavier Leroy2018-02-082-10/+15
| | | | | | | | addressing In the original code, the addressing_valid check is skipped if we are in 32 bits, because we know the check is always true. This is correct but not obvious nor future-proof. (In the future we may want to make addressing_valid more strict.) This commit restructures ConstpropOp.addr_strength_reduction so that the addressing_valid check is always performed.
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-4/+12
|
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-052-10/+24
| | | | Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-101-2/+0
|
generated by cgit (git 2.34.1) at 2024-06-26 18:55:53 +0000