| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
| |
Instead of just dumping the json output it is now a little bit
formatted for better reading.
Furthermore the AsmToJson function for the non powerpc targets now
prints the json value "null" sucht that the resulting json file is
valid json.
|
|
|
|
|
|
| |
The additional compilation information contains the file, command
line (after @-file expansion) and the current working directory.
Bug 21690
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
The new option f(no-)inline controlls whether inlining is active
or not.
Bug 21343.
|
| |
|
|\
| |
| | |
Introduced configuration variable for gnu systems.
|
| |
| |
| |
| |
| |
| |
| | |
The variable gnu_toolchain is true if a gnu toolchain is used and
false in all other cases. The variable avoids the explicit test
whether the system string is diab and should be easier to change.
Bug 20521.
|
|\ \
| | |
| | |
| | |
| | |
| | | |
Remove CompCert's ability to parse and compile source files written in Cminor
This facility is no longer used (as far as we know) and is painful to maintain.
|
| | | |
|
|/ / |
|
| | |
|
|/
|
|
|
| |
Open Local becomes Local Open. This silences Coq 8.6's warning.
Also: remove one useless Require-inside-a-module that caused another warning.
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Introduce Cutil.class_of_attribute to return the class of the given attribute: one among
Attr_type attribute related to types (e.g. "aligned")
Attr_struct attribute related to struct/union/enum types (e.g. "packed")
Attr_function attribute related to function types (e.g. "noreturn")
Attr_name attribute related to variable and function declarations (e.g. "section")
Attr_unknown attribute was not declared
Cutil.declare_attribute is used to associate a class to a custom attribute.
Standard attributes (const, volatile, _Alignas, etc) are Attr_type.
cfronted/C2C.ml: declare the few attributes that CompCert honors currently.
cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
|
|/ |
|
| |
|
|
|
|
|
|
|
| |
The option -fmax-errors limits the number of errors that are
reported before the compilation is aborted. The default 0 means no
limit.
Bug 19872
|
|
|
|
|
| |
GCC treats files with .sx extension in the same way as it treats
files with .S suffix.
|
|
|
|
|
|
| |
Instead of escaping all newlines etc for the help options use
quoted strings.
Bug 19872
|
|
|
|
|
|
|
|
| |
If CompCert crashes because of an uncaught exception the exception
is caught toplevel and the backtrace is printed plus an additional
message to include the backtrace in a support request, if buildnr
and tag are available.
Bug 20681.
|
| |
|
| |
|
| |
|
| |
|
|\
| |
| |
| | |
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).
|
| |
| |
| |
| |
| | |
Cherry-pick commit d1311e6 from trunk.
Simplify convert_external_arg so that it works both in 32 and 64 bits.
|
| |
| |
| |
| |
| | |
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 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
|
| | |
|
| | |
|
|/
|
|
|
| |
Commit 60402c5 breaks printing of default floats by adding support for
%lf. This commit adds back support for %f.
|
|
|
|
|
| |
%lf is official part of the C99 standard.
Bug 19877
|
| |
|
|\
| |
| | |
Advanced diagnostics
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| |/
|/| |
|
|\ \
| | |
| | | |
Support for ARM Big Endian
|
| |\ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | | |
When response files are used CompCert should still print all
command line arguments since the response file is deleted after
usage.
Bug 19297.
|
|\ \ \
| | | |
| | | | |
Add support for response files
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Also corrected some typos and corrected exception handling for
expandargv.
Bug 18308
|
| | | | |
|
| | | | |
|