| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
| |
| |
| | |
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
|
| |
|
|\ |
|
| | |
|
|/ |
|
| |
|
|
|
|
|
|
|
|
| |
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
|
| | | |
|