aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asm.v
Commit message (Collapse)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-0/+2
| | | | cfrontend/C2C.ml
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
| | | | | | | | | | | 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`.
* PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-061-1/+1
| | | | Inlined built-in functions destroy GPR0
* Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-061-9/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Model GPR0 in isel (#199)Xavier Leroy2019-09-171-1/+1
| | | | | | | | 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.
* Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-281-0/+8
| | | | | | 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.
* Emulate the "isel" instruction on non-EREF PPC processorsXavier Leroy2019-05-201-1/+1
| | | | | On non-EREF processors it expands to instructions that destroy GPR0. Reflect this in the Asm semantics for Pisel.
* Give a semantics to the Pisel instructionXavier Leroy2019-05-201-1/+7
|
* Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776Michael Schmidt2018-10-201-2/+2
|
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-1/+10
| | | | | | | | | | 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 new powerpc builtins.Michael Schmidt2018-04-271-0/+4
| | | | | | New builtin for 64-bit load/store with byte reversal and 64-bit mul-high. Bug 23541
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-10/+167
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-4/+6
| | | | Without scopes Coq 8.6 warns, probably rightly so.
* Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-29/+29
| | | | | The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima.
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-17/+34
| | | | | | | | | | | | | This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations. In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves. Summary of changes: - AST: introduce the type "rpair A" of register pairs - Conventions1, Conventions: use it when describing calling conventions - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls - Events: suppress external_call', no longer useful - All passes from Allocation to Asmgen: adapt accordingly.
* Bug 17752, add rldicr instruction for PowerPCMichael Schmidt2015-12-151-1/+3
|
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-9/+9
|
* Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-0/+19
| | | | | | Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
* Added builtin for isel.Bernhard Schommer2015-09-081-0/+2
| | | | | The builtin_isel function takes a _Bool as first argument and returns either the second or the third depending on the value of the _Bool.
* Added builtins for call frame and return address.Bernhard Schommer2015-09-071-3/+3
| | | | | | This builtins can be used to get the call frame address and the return address. To correctly compute the load address of the return address the allocframe is extended to contain the offset of the return address.
* Added builtin for the cmpb instruction.Bernhard Schommer2015-09-071-0/+2
|
* Added builtin for mbar instruction.Bernhard Schommer2015-09-031-0/+2
| | | | This commit adds a builtin function for the mbar instruction.
* New builtin for dcbz instruction.Bernhard Schommer2015-09-031-8/+10
| | | | | | This commit adds a builtin for the dcbz instructions. Additionally the dcbt,dcbtst,dcbtls and icbtls instruction are changed to their actually form all taking one additional register in Asm.v.
* Added builtin for the icbtls instruction.Bernhard Schommer2015-09-021-0/+2
| | | | This commit adds a builtin for the icbtls instruction.
* Added builtin for dcbtlsBernhard Schommer2015-09-021-1/+3
| | | | | | THis commit adds a builtin function for the dcbtls instruction. Additionaly it changes the printing of the dcbt and dcbtst instruction to embedded mode and adds support for different address variants.
* Added the gcc builtin prefetch.Bernhard Schommer2015-09-011-0/+4
| | | | | | This commit implements the gcc __builtin_prefetch in a form with all arguments for the powerpc architecture. The resulting instructions are the dcbt and dcbtst instructions in Server Category.
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-1/+1
| | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
* Adapt the PowerPC port to the new builtin representation.Xavier Leroy2015-08-211-26/+23
| | | | | | | __builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating.
* Added builtin for the dcbf instructionBernhard Schommer2015-08-171-0/+2
|
* Added builtin for the dcbi instruction.Bernhard Schommer2015-08-171-4/+4
|
* Added builitin for the icbi instruction.Bernhard Schommer2015-08-141-0/+2
|
* Added builtin for the lwsync barrier.Bernhard Schommer2015-08-141-0/+2
|
* Corrected little typo in __builtin_clz function.Bernhard Schommer2015-07-061-2/+2
|
* Changed a minor typo: Pstwxu should be PstwuxBernhard Schommer2015-06-221-2/+2
|
* Updating the PowerPC and ARM ports.Xavier Leroy2015-03-271-35/+7
| | | | PowerPC: always use full register names to print annotations.
* Add builtins for load with reservation and conditional store.xleroy2014-08-201-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.xleroy2014-08-181-18/+8
| | | | | | | | | | | powerpc/Asmgen*: simplify the code generated for far-data relative accesses, so that the only occurrences of Csymbol_rel_{low,high} are in the pattern Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...) checklink/Check.ml: check the pattern above. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-14/+85
| | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-231-9/+51
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-16/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-4/+4
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just ↵xleroy2013-12-261-27/+26
| | | | | | like we already do in ARM Asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/: new unary operation "addsymbol"xleroy2013-11-171-1/+9
| | | | | | | | Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+6
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:xleroy2013-06-161-1/+1
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-3/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2238 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-41/+38
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-124/+139
| | | | | | | | | | - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-5/+5
| | | | | | | | | | injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-071-6/+0
| | | | | | | | (definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 03:33:22 +0000