| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|\ |
|
| | |
|
| | |
|
|/ |
|
|\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
-> x86/x86_32/x86_64
Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.
This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86.
While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures.
Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
|
| |
| |
| |
| | |
"subslt" changes the flags, affecting the condition of the "sbclt" that follows.
|
| |
| |
| |
| |
| |
| | |
SelectLong.is_longconst was always returning 'false' in 32 bits.
SelectLong.mullimm was generating a Omullimm insn even in 32 bits.
Both functions are used by SelectDiv.
|
| |
| |
| |
| |
| | |
This can make a big difference in which optimizations are triggered later.
Constants were already propagated by "longofintu".
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
__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.
|
| | |
|
| | |
|
|\ \
| | |
| | | |
Add a man page
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
There is a bug in the fstat implementation in ocaml 4.03 under windows. In
order to prevent this we guard the isatty function with an additional try
with.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Since the menhir version required supports the --suggest-menhirLib
flag we can query it already in the configure script simplifying
the Makefile.menhir
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The options controlling the generation of debugging information
are now moved into the Debug module. Futhermore the -gdepth
options are replaced in favor of a more gcc compatible version.
Bug 20193
|
|/ / |
|
| | |
|
| |
| |
| |
| |
| |
| | |
The new configure switch generates a .merlin file and adds the
-bin-annot flag to the compile options.
Bug 20081
|
|/
|
|
|
| |
Commit 60402c5 breaks printing of default floats by adding support for
%lf. This commit adds back support for %f.
|
|
|
|
|
| |
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
|
| |
|