aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inlining.v
Commit message (Collapse)AuthorAgeFilesLines
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-6/+6
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-9/+3
|
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-11/+11
|
* 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.
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-9/+12
| | | | | | | | | | | | | | | | | | | | | | | | Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations.
* Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-271-0/+12
| | | | | | | | | | variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet.
* Inlining: preserve all RTL regs mentioned in the function, not justxleroy2014-03-291-29/+3
| | | | | | | | those defined in the function. Semantically, both are correct, but the latter may cause RTLtyping to fail if some regs are uninitialized and a collision occurs between regs of different types. RTL: move the function resource computations there, as it could be useful for other passes some day. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2440 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised renumbering of nodes and registers so that main function is not ↵xleroy2013-10-181-4/+6
| | | | | | shifted by 1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:xleroy2013-06-161-2/+0
| | | | | | | | | | | | | | - 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
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-6/+12
| | | | | | | | | 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
* Pointers one pastxleroy2013-02-151-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove some useless "Require".xleroy2012-12-301-1/+0
| | | | | | | Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-11/+7
| | | | | | | | | | | function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem branch:xleroy2012-05-211-0/+477
- Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 05:40:56 +0000