| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
| |
The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.
|
| |
|
|
|
|
|
| |
The list of reserved_registers is never reset between the compilation of
multiple files. Instead of storing them in IRC they are moved in the
CPragmas file and reset in the a new reset function for Cpragmas whic is
called per file.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Until now the types Tany32 and Tany64 were not used prior to register
allocation, so IRC.class_of_type did not need to be defined for
those types.
However, there are possible uses of stack slots of type Tany32 and Tany64
to specify calling conventions. For this purpose, we need to define
class_of_type for Tany32 and Tany64. We follow the informal convention
that Tany32 goes in integer registers and Tany64 goes into integer
registers if 64-bit wide, or FP registers otherwise.
|
| |
|
|
|
|
|
|
|
|
|
| |
- 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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
architectures
The original Stacking pass and its proof hard-wire assumptions about the processor and the register allocation, namely that integer registers are 32 bit wide and that all stack slots have natural alignment 4, which precludes having stack slots of type Tlong. Those assumptions become false if the target processor has 64-bit integer registers.
This commit makes minimal adjustments to the Stacking pass so as to lift these assumptions:
- Stack slots of type Tlong (or more generally of natural alignment 8) are supported. For slots produced by register allocation, the alignment is validated a posteriori in Lineartyping. For slots produced by the calling conventions, alignment is proved as part of the "loc_argument_acceptable" property in Conventions1.
- The code generated by Stacking to save and restore used callee-save registers no longer assumes 32-bit integer registers. Actually, it supports any combination of sizes for registers.
- To support the new save/restore code, Bounds was changed to record the set of all callee-save registers used, rather than just the max index of callee-save registers used.
On CompCert's current 32-bit target architectures, the new Stacking pass should generate pretty much the same code as the old one, modulo minor differences in the layout of the stack frame. (E.g. padding could be introduced at different places.)
The bulk of this big commit is related to the proof of the Stacking phase. The old proof strategy was painful and not obviously adaptable to the new Stacking phase, so I rewrote Stackingproof entirely, using an approach inspired by separation logic. The new library common/Separation.v defines assertions about memory states that can be composed using a separating conjunction, just like pre- and post-conditions in separation logic. Those assertions are used in Stackingproof to describe the contents of the stack frames during the execution of the generated Mach code, and relate them with the Linear location maps.
As a further simplification, the callee-save/caller-save distinction is now defined in Conventions1 by a function is_callee_save: mreg -> bool, instead of lists of registers of either kind as before. This eliminates many boring classification lemmas from Conventions1. LTL and Lineartyping were adapted accordingly.
Finally, this commit introduces a new library called Decidableplus to prove some propositions by reflection as Boolean computations. It is used to further simplify the proofs in Conventions1.
|
| |
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
| |
|
|
|
|
| |
Since the invariant checks are not currently used and they are not
exported they are renamed to include a _ to avoid warning.
Bug 18394
|
| |
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|
|
|
|
| |
- Use a hashtable instead of an AVL set for adjSet
- Inlining and algebraic simplification of spillCost into selectSpill.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2450 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
PrintLTL: List.map -> List.rev_map
IRC: @ -> List.rev_append + don't maintain "extra" lists on precolored nodes.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2262 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
| |
- 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
|
|
|
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
|
