aboutsummaryrefslogtreecommitdiffstats
path: root/x86
Commit message (Collapse)AuthorAgeFilesLines
...
* | Adding copyrightsCyril SIX2020-05-043-0/+38
| |
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-3/+8
|\ \
| * | porting to ppc riscV x86David Monniaux2020-04-011-3/+8
| | |
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-122-4/+63
|\ \ \
| * | | fix IA32 profiling bugDavid Monniaux2020-04-121-2/+4
| | | |
| * | | x86-64 profilingDavid Monniaux2020-04-122-4/+61
| |/ /
* | | Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-091-2/+2
|\ \ \
| * | | adapt the other targets for the new field in CEcondDavid Monniaux2020-04-081-2/+2
| |/ /
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-085-149/+305
|\| |
| * | DuplicateOpcodeHeuristic x86David Monniaux2020-03-171-3/+27
| | |
| * | adjust for x86David Monniaux2020-03-031-44/+35
| | |
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-032-0/+286
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | better 32/64-bit handlingDavid Monniaux2020-03-032-26/+51
| | | |
| | * | moved away x86-dependent partsDavid Monniaux2020-03-031-0/+46
| | | |
| | * | starting to move x86 stuff to x86David Monniaux2020-03-031-0/+215
| | |/
| * | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-0313-16/+166
| |\ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | 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.
* | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-253-19/+31
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-243-19/+31
| |\| | | | |/ | |/| | | | mppa-work-upstream-merge
| | * 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.
* | | fix for x86+arm unsupported thread localDavid Monniaux2020-02-241-3/+9
|/ /
* | stubs to keep compiling on architectures not K1cDavid Monniaux2020-02-071-0/+3
| |
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-3/+0
|\|
| * 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.
* | add: non trapping opsDavid Monniaux2019-09-231-0/+31
| |
* | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-201-4/+4
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| * | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-201-4/+4
| |\| | | | | | | | | | mppa-work-upstream-merge
| | * 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
* | | | more for passing notrap through x86David Monniaux2019-09-075-10/+56
| | | |
* | | | for nontrapDavid Monniaux2019-09-061-0/+28
|/ / /
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-282-15/+19
|\| | | | | | | | | | | mppa-work-upstream-merge
| * | 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
* | helpers broke compilationDavid Monniaux2019-07-192-10/+2
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-197-31/+153
|\| | | | | | | mppa-work-upstream-merge
| * 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.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-0312-45/+305
|\| | | | | | | mppa-if-conversion
| * 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.
* | ça recompile sur x86David Monniaux2019-03-224-3/+37
| |
generated by cgit (git 2.34.1) at 2024-05-19 21:11:51 +0000