| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|/
|
|
|
| |
Pull request #188 from Maxime Dénès.
This flag makes it easier for the Coq people to test CompCert with in-development versions of Coq.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes.
The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/
This port required the following additional changes:
- Integers: More properties about shrx
- SelectOp: now provides smart constructors for mulhs and mulhu
- SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu.
- Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library.
- test/: add SIMU make variable to run tests through a simulator
- test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers
commit da14495c01cf4f66a928c2feff5c53f09bde837f
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu Apr 13 17:36:10 2017 +0200
RISC-V port, continued
Now working on Asmgen.
commit 36f36eb3a5abfbb8805960443d087b6a83e86005
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed Apr 12 17:26:39 2017 +0200
RISC-V port, first steps
This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
|
| |
|
| |
|
|
|
|
| |
Menhir's Coq backend has been updated to support Coq 8.6.
|
| |
|
| |
|
| |
|
| |
|
|\
| |
| |
| | |
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).
|
| | |
|
| |
| |
| |
| |
| | |
- Avoid absolute addressing for labels, use RIP-relative addressing
- Different, RIP-relative implementation of jump tables
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|\ \
| | |
| | | |
Add a man page
|
| | | |
|
|/ /
| |
| |
| |
| |
| | |
Since the menhir version required supports the --suggest-menhirLib
flag we can query it already in the configure script simplifying
the Makefile.menhir
|
|/
|
|
|
|
| |
The new configure switch generates a .merlin file and adds the
-bin-annot flag to the compile options.
Bug 20081
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| | |
The diab data compiler has different quoting conventions compared
to the gnu tools.
Bug 18308.
|
| |
| |
| |
| |
| |
| |
| |
| | |
The functions expandargv and writeargv resemble the functions from
the libiberity that are used by the gnu tools. Additionaly a new
configuration is added in order to determine which kind of response
files are supported for calls to other tools.
Bug 18308
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Instead of an addition -little or -big at the end the configure
script now accepts armeb* for the big endian arm targets.
Bug 19418
|
|/
|
|
|
|
|
|
| |
Adds support for the big endian arm targets by making the target
endianess flag configurable, adding support for the big endian
calling conventions, rewriting memory access patterns and adding
big endian versions of the runtime functions.
Bug 19418
|
|
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
| |
|
|
|
|
|
|
| |
The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609
|
| |
|
|
|
|
| |
Earlier versions of Menhir run into "string too long" errors in Coq when building on a 32-bit platform.
|
| |
|
| |
|
| |
|
|
|
|
| |
The test was failing as a consequence of the split casm -> casm / casm_options.
|
|\ |
|
| |
| |
| |
| |
| |
| | |
The diab compiler seems to interpret the alignment as power of two
instead of the value.
Bug 18490
|
| |
| |
| |
| | |
This reverts commit 771d8576fbae8bd48f6bc80c74722ce1c7cc5259.
|
| |
| |
| |
| |
| |
| | |
The default of the diab compiler is to interpret the alignment
as power of two.
Bug 18490.
|
|/
|
|
|
|
|
|
|
|
|
| |
Since the menhir version we use requires ocaml>4.02 we can also
upgrade the required ocaml version to >4.02 and remove the
deprecate String functions.
Also we now activate all warnings except for 4,9 und 27 for regular
code plus a bunch of warnings for the generated code. 4 and 9 are
not really usefull and 27 is deactivated since until the usage
string is printed in a way that requires no newline.
Bug 18394.
|
|
|
|
|
|
| |
Added additional configuration entries to seperate tools from options in the
.ini files. Internally they are just concatenated in Configuration.ml which
allows it to still use old .ini files.
|
|
|
|
| |
The new configuration option -clightgen activates the build of clightgen.
|
|
|
|
| |
Update configure to require Menhir 20151110.
|
|\
| |
| |
| |
| | |
Conflicts:
Makefile.extr
|
| | |
|
| |\
| | |
| | |
| | | |
Resolved conflicts in:configure powerpc/Asmexpand.ml
|
| | |
| | |
| | |
| | |
| | |
| | | |
Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence.
Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
|
| |/
|/| |
|
|/ |
|