| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port.
Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.
To activate x86-64 bit support, configure with "x86_64-linux".
Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode
To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
(currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.
|
|
|
|
|
| |
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 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.
|
|
|
|
|
| |
The anonymous members are kept but using them is still an error.
Bug 19907
|
| |
|
|
|
|
|
|
| |
Now "expected at least %d" instead of "expected %d". Also improved
error message for __builtin_debug.
Bug 19872
|
| |
|
|\ |
|
| | |
|
|/ |
|
| |
|
|
|
|
|
|
|
|
| |
The only case where compcert raise a pedantic warning was for
implicit int parameters. This is the behavior of clang. However
since not all other pedantic warnings are supported the behavior
of gcc is adopted.
Bug 19872.
|
|
|
|
|
| |
%lf is official part of the C99 standard.
Bug 19877
|
|
|
|
|
|
| |
In order to empty declarations it is necessary to distinguish
between forward declarations and empty declarations.
Bug 19859
|
|\
| |
| |
| |
| |
| | |
Fix minor issues in some proofs and tactics.
Patch by Maxime Dénès.
|
| |
| |
| |
| |
| | |
These minor problems were revealed by porting CompCert to Coq 8.6, where
they trigger errors.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\ \
| | |
| | | |
Advanced diagnostics
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Now the same warning is triggered for both cases, int to ptr and
ptr to int.
Bug 18004
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
This warning should be triggered if a feature is used that is not
part of the code CompCert C language.
Bug 18004
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Some old errors/warnings messages were better before and are now
rephrased. Furthermore some formulations are rephrased to match the
used formulations of the ISO C stanard, e.g. storage class is
replaced with storage-class.
Bug 18004
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Removed duplicated of, changed string to string literal for
wording than the C standard.
Bug 18004
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This avoids introducing line breaks during printing of function
types.
Bug 18004
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Color output is only enabled if stderr is a tty, and the
environment variable TERM is not empty or dumb.
Bug 18004
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Now each warning either has a name and can be turned on/off, made
into an error,etc. or is a warning that always will be triggered.
The message of the warnings are similar to the ones emited by
gcc/clang and all fit into one line.
Furthermore the diagnostics are now colored if colored output is
available.
Bug 18004
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
lib/Integers.v: define division-remainder of a double word by a word
ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction
ia32/*: adapt accordingly
Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
|
| | | | |
| | | | |
| | | | |
| | | | | |
Inline directives in extraction.v make the Caml output efficient and almost nice.
|
| | | | |
| | | | |
| | | | |
| | | | | |
The cut-and-paste was for compatibility with Coq 8.4
|
| | | | | |
|
| | | | | |
|