| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| |
|
|
|
| |
__builtin_bswap64 is now available both in 32 and 64-bit mode.
The DWARF bit is the numbering of registers in ia32/Asmexpand.ml.
|
| | |
|
| | |
|
| |
|
|
|
| |
Cherry-pick commit d1311e6 from trunk.
Simplify convert_external_arg so that it works both in 32 and 64 bits.
|
| |
|
|
|
| |
Tests updated to work with x86 64 bits.
Infrastructure added: script "Runtest", with ability to have different reference outputs depending on platform or bit size.
|
| | |
|
| |
|
|
|
| |
- Avoid absolute addressing for labels, use RIP-relative addressing
- Different, RIP-relative implementation of jump tables
|
| |
|
|
|
|
| |
During the experiments, the integer + pointer cases was removed from the semantics of the C addition operator. The idea was to turn integer + pointer into pointer + integer during elaboration, but it was not implemented.
On second thoughts, we can restore the integer + pointer cases in the formal semantics of CompCert C at low cost. This is what this commit does.
|
| |
|
|
|
| |
This somewhat useful idiom was broken when Val.add was replaced by Val.offset_ptr in the Efield case. This commit restores the previous behavior.
This used to be supported (and is useful
|
| |
|
|
| |
While merging the 32- and 64-bit code generators, some regressions were introduced in the 32 bit case.
|
| |
|
|
|
|
| |
This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case.
For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
|
| |
|
|
|
|
| |
Apparently coq compiled with camlp4 has a problem with the user
defined do <- ... ; ... and do.
Bug 20050
|
| | |
|
| |
|
|
|
|
| |
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
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
