| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
|
|
|
|
| |
ARM: various tweaks, incl. support for SDIV and UDIV insns when available.
test/regression/funptr2.c: Thumb does weird things with <function ptr>+1.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
pseudo-instructions so that it does not need to be re-done in
cchecklink.
cchecklink: updated accordingly.
testsuite: compile with -sdump and run cchecklink if supported.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2498 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
where T is a typedef for a character type.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2488 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|