aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | so that all architectures compileDavid Monniaux2020-10-021-0/+1
| | |/ / | |/| |
* | | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+10
| | | |
* | | | pointer_eq copiedDavid Monniaux2020-11-251-0/+14
| |/ / |/| |
* | | bug #223 fix on PPCDavid Monniaux2020-11-232-3/+73
|/ /
* | Adding copyrightsCyril SIX2020-05-043-0/+38
| |
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-202-3/+11
|\ \
| * | test whether the instructions are allowedDavid Monniaux2020-04-191-0/+2
| | |
| * | porting to ppc riscV x86David Monniaux2020-04-011-3/+9
| | |
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+1
|\ \ \
| * | | missing cases preventing compilationDavid Monniaux2020-04-081-0/+1
| |/ /
* | | Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-091-1/+1
|\ \ \
| * | | adapt the other targets for the new field in CEcondDavid Monniaux2020-04-081-1/+1
| |/ /
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-086-132/+203
|\| |
| * | DuplicateOpcodeHeuristic ppcDavid Monniaux2020-03-171-3/+27
| | |
| * | fix for ppcDavid Monniaux2020-03-031-14/+22
| | |
| * | ported for ppcDavid Monniaux2020-03-031-22/+17
| | |
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-035-3/+173
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | CSE2 for powerpcDavid Monniaux2020-03-032-0/+152
| | |/
| | * 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.
| * | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-0311-10/+134
| |\ \ | | |/ | |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | 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.
* | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-253-17/+21
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-243-17/+21
| |\| | | | |/ | |/| | | | mppa-work-upstream-merge
| | * 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.
* | | 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()`.
generated by cgit (git 2.34.1) at 2024-05-20 06:34:04 +0000