aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Machregs.v
Commit message (Collapse)AuthorAgeFilesLines
* Applied a few simplification for temporary registers.Bernhard Schommer2015-09-211-3/+2
|
* Use fix registers for atomic builtins.Bernhard Schommer2015-09-141-5/+12
| | | | | | In order to avoid clashes during register allocation etc. The builtins now use fixed registers and mark additional registers as destroyed for temporaries.
* Added builtin for atomic compare and exchange.Bernhard Schommer2015-09-101-0/+2
| | | | | | The new __builtin_atomic_compare_exchange(int *ptr,int *exp,int *dsr); writes dsr into ptr if ptr is equal to exp and returns true if ptr is not equal to exp it writes ptr into exp and returns false.
* Merge branch 'master' into atomic-builtinsBernhard Schommer2015-09-101-2/+3
|\ | | | | | | | | Conflicts: powerpc/CBuiltins.ml
* | Added an builtin for the atomic exchange operation.Bernhard Schommer2015-09-091-1/+7
|/ | | | | The new builtin __builtin_atomic_exchange(int *a, int *b, int *c) stores *b in *a and sets *c to the old value of *a.
* Simplified generation of builtins for cache instructions.Bernhard Schommer2015-09-071-3/+3
| | | | | | The cache instructions need no special constraint on the address argument. Therefore also the generation of the address is no longer needed.
* Added builtin for mbar instruction.Bernhard Schommer2015-09-031-0/+2
| | | | This commit adds a builtin function for the mbar instruction.
* 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-0/+2
| | | | | | 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/+2
| | | | | | 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.
* Adapt the PowerPC port to the new builtin representation.Xavier Leroy2015-08-211-5/+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.
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-0/+42
| | | | | | | | | | - 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
* Merge of "newspilling" branch:xleroy2014-07-231-27/+10
| | | | | | | | | | | | | | | - 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
* 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
* Merge of the float32 branch: xleroy2013-05-191-1/+7
| | | | | | | | - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-31/+93
| | | | | | | | | 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
* Merge of the reuse-temps branch:xleroy2010-09-021-12/+15
| | | | | | | | | | | | - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x ↵xleroy2009-02-261-9/+9
| | | | | | >= 0' and 'x < 0'. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@999 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+107
Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 05:22:32 +0000