| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
| |
The runtime functions are prefixed with compcert in order to
avoid potential clashes with runtime/builtin functions of other
compilers.
Bug 22062
|
| |
|
| |
|
|
|
|
|
| |
For dcc one needs to pass -Ws to tell the linker that it should
not link the default startfiles.
|
|
|
|
| |
A 16-bit "nop" is needed because in "add pc, r14" pc reads as the address of the add instruction plus 4, and "add pc, r14" has a 16-bit encoding.
|
|
|
|
| |
It is also easier to recognize than the old one for binary analysis tools.
|
| |
|
| |
|
|\ |
|
| |\
| | |
| | | |
Issue #P18: handle large offsets when accessing return address and back link in the stack frame
|
| | |
| | |
| | |
| | | |
This reduces the chances that back link and return address cannot be saved by a single str instruction. We generate correct code for the overflow case, but the code isn't very efficient, so let's make it uncommon.
|
| | |
| | |
| | |
| | |
| | |
| | | |
Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12.
R12 can be used as a temporary because it is marked as destroyed at function entry. We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed. In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.
|
| | |
| | |
| | |
| | | |
Next commit uses those lemmas in the ARM port.
|
| | |
| | |
| | |
| | | |
This is what we do for PowerPC and is more resilient to changes in code generation. We need to give Pcfi_rel_offset a dynamic semantics, but that's just a no-op.
|
| | | |
|
| | |
| | |
| | |
| | | |
Functions which require large amounts of stack for spilling and/or arguments for function calls lead to stackframe offsets that exceed the 12bit limit of immediate constants in ARM instructions. This patch fixes the stack-offsets in the function prolog/epilog.
|
| | | |
|
|/ / |
|
|/
|
|
|
|
| |
The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196.
The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
|
|\ |
|
| |
| |
| |
| | |
These are the configurations for the new RISC-V port.
|
| |
| |
| |
| | |
8.6.1 works just fine with the current CompCert.
|
|/ |
|
|\ |
|
| | |
|
| | |
|
|/ |
|
|
|
|
|
|
|
| |
12 was a too small overaproximation for call which require fixup
code for arguments and result. The new constant is 72, which
consists of 4 for the branch instruction, 16 * 4 for the arguments
and 4 for the result.
|
| |
|
| |
|
|
|
|
|
|
| |
We don't need verbose debug for the assembler. The verbose debug
information should only be printed if assembler files are
generated.
|
|
|
|
| |
Some modules new in 3.0 were not mentioned.
|
|
|
|
|
|
|
| |
PowerPC port: add strength reduction for 64-bit operations
* Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748)
* Moved shru_rolml proof to Values.
|
|
|
|
|
|
| |
Fixes: Github issue #190.
Tint was used instead of the correct Tptr.
|
|
|
|
| |
These Coq people have version "numbers" that look nothing like numbers, such as "trunk". Also, they didn't test their pull request #188. Fixing this.
|
|
|
|
|
|
|
|
| |
- Add support for PowerPC, with all addressing modes.
- Add support for ARM, with "reg + ofs" addressing mode.
- Add support for RISC-V, with the one addressing mode.
- Constprop.v: forgot to recurse in BA_addptr
- volatile4 test: more tests
|
|
|
|
|
|
| |
This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses.
Current status: x86 port only, the only new addressing mode handled is reg + offset.
|
|
|
|
| |
This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
|
|\ |
|
| |\
| | |
| | | |
Extension of configure for issue #189
|
| |/ |
|
| |
| |
| |
| | |
Typo in configure help message.
|
|/
|
|
|
| |
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 reverts commit 414225093054f0fdd9222e0ba9fbb95d345f5457.
|
|\ |
|
| |
| |
| |
| |
| |
| | |
ignore generated directory additional_files
Bug 20000
|
|/
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
The inline assembler instructions are numbered with consecutives
id's per compilation unit.
Bug 21689
|