aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
* Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-141-6/+6
|
* Updated PrintOp for the single-precision FP operations.Xavier Leroy2015-05-091-0/+8
|
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-093-35/+51
| | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-301-35/+35
| | | | Val.lessdef, etc.
* Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵Xavier Leroy2015-04-232-1/+4
| | | | clobber lists.
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-232-0/+8
|
* Cleanups and updates for extended asm.Xavier Leroy2015-04-211-2/+1
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-212-2/+2
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-173-7/+16
|
* Merge branch 'master' into dwarfBernhard Schommer2015-04-028-52/+54
|\
| * Ccompuimm now depends on the memory, this is needed to proof the Lemma ↵Bernhard Schommer2015-04-021-2/+3
| | | | | | | | op_depends_on_memory_correct.
| * Updating the PowerPC and ARM ports.Xavier Leroy2015-03-277-50/+51
| | | | | | | | PowerPC: always use full register names to print annotations.
* | Print all files ever encountered in the filenum.Bernhard Schommer2015-04-011-4/+3
| |
* | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+12
| | | | | | | | global target dependend option to activate the printing only for targets wher it works.
* | Started integrating the debug printing in the common backend_printer.Bernhard Schommer2015-03-111-6/+54
|/
* Removed unused sel_target, changed cygwin symbol names and changed the ↵Bernhard Schommer2015-02-191-0/+1
| | | | default function aligment to be target dependent.
* Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-181-6/+17
|
* Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-181-2/+2
|
* Changed arm backend to the common backend printer.Bernhard Schommer2015-02-091-2/+2
|
* Changed the ia32 backend to the new Printer.Bernhard Schommer2015-02-061-5/+2
|
* Changed the ASM printer of the powerpc to the generalized backend.Bernhard Schommer2015-02-053-803/+744
|
* Moved more common functions into a seperate file.Bernhard Schommer2015-02-041-34/+6
|
* Started moving common backend functions into one file.Bernhard Schommer2015-02-031-40/+9
|
* Changed the print_globaldef function of the powerpc backend to look like the ↵Bernhard Schommer2015-01-281-10/+2
| | | | functions used in the arm and ia32 backend.
* In -g -S mode, annotate the generated asm file with the C source code in ↵Xavier Leroy2015-01-071-39/+18
| | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml
* Clean up support for common symbols. Uninitialized "const" symbols can be ↵Xavier Leroy2014-12-171-9/+10
| | | | common.
* Update PowerPC port.Xavier Leroy2014-11-242-21/+51
|
* Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-241-67/+0
| | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* Refactored the code of powerpc/PrintAsm.ml by moving the function depending ↵Bernhard Schommer2014-10-081-200/+236
| | | | on the target system in a seperate module.
* Cold feet: suppress builtins for load with reservation/store conditional, ↵xleroy2014-08-282-11/+1
| | | | | | use case is unclear. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename __builtin_cntlz to __builtin_clz.xleroy2014-08-272-2/+2
| | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add builtins for load with reservation and conditional store.xleroy2014-08-204-1/+19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink/Check.ml: missing SDA addressing for store instructions.xleroy2014-08-191-12/+20
| | | | | | | | powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections). test/regression/sections.c: test for SDA and relative addressings. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.xleroy2014-08-186-118/+117
| | | | | | | | | | | 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
* All targets: add __builtin_membarxleroy2014-07-281-7/+9
| | | | | | | ARM: add __builtin_dsb __builtin_isb git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-285-507/+711
| | | | | | | | | | 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
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-281-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-232-0/+6
| | | | | | | | | The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-2316-311/+550
| | | | | | | | | | | | | | | - 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-247-100/+61
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated the proofs.xleroy2014-04-121-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2454 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-094-28/+153
| | | | | | | | | | over booleans. Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In Regalloc, dead code elimination, don't eliminate move operationsxleroy2014-02-231-0/+2
| | | | | | | | that pop the x87 FP stack (var <- FP0). Otherwise, (void) f(); where f returns a float eventually produces a FP stack overflow. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2416 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC is big-endian, dammit.xleroy2014-02-211-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2412 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-195-4/+13
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize .i and .p source files as C sources not to be preprocessed.xleroy2014-02-051-0/+1
| | | | | | | Add CompCert version number and command line as comments in generated asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2407 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Eradication of Mfloat64al32, continued.xleroy2014-01-121-4/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2404 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-123-8/+8
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-5/+13
| | | | | | | | | | - endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for the multiple-input-needs case.xleroy2014-01-031-40/+45
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2401 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 14:36:36 +0000