| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 treatment of attributes in the current CompCert is often surprising. For example,
attribute(xxx) char * x;
is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char".
CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e.
const char * x;
is really "x is a pointer to a const char", not "x is a const pointer to char".
This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above,
attribute(xxx) char * x; // "attribute(xxx)" applies to "x"
const char * x; // "const" applies to "char"
This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
|
|
|
|
|
|
|
|
|
|
|
|
| |
-> 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).
|
| |
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
| |
- Adjust parameters to bring the running time of each test closer to 1 second
- compression/arcode.c: array access one past
- "inline" -> "static inline"
- Remove cchecklink support
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Here are two examples that cause an internal error in Asmexpand.ml:
volatile long long x; void f(unsigned int i) { x = i; }
unsigned g(unsigned i) { return __builtin_clzll(i); }
The argument "i" to builtin volatile store or __builtin_clzll is turned into a BA_splitlong(BA_int 0, BA <variable i>), which Asmexpand.ml doesn't know how to handle.
The fix (in AST.builtin_arg_ok) is to prevent this 'optimization' for all builtins except those of the "OK_all" kind, i.e. __builtin_annot.
Regression tests were added and tested on IA32. Need to retest on ARM and PowerPC.
|
|
|
|
|
|
|
|
| |
This commits handles the case where the argument is passed with a type different from the actual type of the argument, as in
float f (x) float x; { return x; }
"x" is passed with type "double", and must be converted to "float" at the beginning of the function.
|
| |
|
|
|
|
|
|
|
| |
ARM: add __builtin_clzl, __builtin_clzll
IA32: add __builtin_clzl, __builtin_clzll,
__builtin_ctzl, __builtin_ctzll
Add corresponding tests in tests/regression/
|
|
|
|
| |
Regression test added in regression/initializers.c
|
|\ |
|
| |\ |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
- Added a Cabs.PROTO_OLD constructor to Cabs.decl_type
- Refactored the Parser.vy and pre_parser.mly grammars
- Rewritten the conversion of old function definitions to new-style
|
|/ / |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
was not parsed correctly:
typedef int a;
int f() {
for(int a; ;)
if(1);
a * x;
}
Additionnaly, I tried to add some comments in the pre-parser code,
especially for the different hacks used to solve various conflicts.
|
| |
| |
| |
| | |
In RTL and beyond, the result of a builtin function that has return type different from "void" must be BR, never BR_none. Otherwise, we get compile-time fatal errors, either in Asmexpand or in Lineartyping.
|
|/ |
|
|
|
|
| |
Also: exit on error when a test fails.
|
| |
|
|
|
|
| |
pointer manipulations.
|
|\ |
|
| |
| |
| |
| |
| |
| | |
The copy optimization is not correct in case of overlap between destination
and source. We would need to use an hypothetical __builtin_memmove_aligned
that can cope with overlap to implement the copy at return of callee.
|
| |
| |
| |
| |
| |
| | |
cparser/Bitfields.ml: when assigning to a bit field of type _Bool, the
right-hand side must be normalized to 0 or 1 via a cast to _Bool.
test/regression/bitfields{1,9}.c: add corresponding test cases.
|
|/
|
|
| |
These instructions are approximate and produce different results on different processors. Just check the error bounds specified in the PPC ISA.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- Treat clobbered registers as being destroyed by EF_inline_asm builtins
(which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.
-# Please enter the commit message for your changes. Lines starting
|
|
|
|
| |
unblocking; improve translation of bitfield initializers and compound literals.
|
|
|
|
|
|
| |
Bitfields: better translation of initializers and compound literals; run this pass before unblocking.
Transform.stmt: extend with ability to treat unblocked code.
test/regression: more bitfield tests.
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
- support "r", "m" and "i" constraints
- support "%Q" and "%R" modifiers for register pairs
- support register clobbers
- split off analysis and transformation of asm statements in
cparser/ExtendedAsm.ml
|
|\
| |
| | |
Extended annotations
|
| | |
|
| |
| |
| |
| | |
ARM is done, IA32 and PowerPC remain to be updated.
|
| |
| |
| |
| |
| |
| |
| |
| | |
composites).
- Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD.
- Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions.
- More comprehensive interoperability test in regression/interop1.c.
|
| | |
|
|/
|
|
|
|
|
|
|
|
| |
The passing of struct/union arguments by value implemented in the verified
part of CompCert is not compatible with the ARM, PowerPC and x86 ABI.
Here we enrich the StructReturn source-to-source emulation pass
so that it implements the calling conventions defined in these ABIs.
Plus: for x86, implement the returning of struct/union results by value
in a way compatible with the ABI.
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
|
| |
| |
| |
| |
| | |
Use these constructor functions in C2C to rely less on the types produced
by the unverified elaborator.
|
| |
| |
| |
| | |
passes the reference interpreter.
|
|/ |
|
|
|
|
|
|
|
| |
IA32: add __builtin_clz, __builtin_ctz.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections).
test/regression/sections.c: test for SDA and relative addressings.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|