| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Clarify that ARMv6 is in fact ARMv6T2
The ARMv6 comes in two flavors depending on the version of the Thumb
instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2.
CompCert only supports Thumb2, so its ARMv6 architecture should really be
called ARMv6T2. This makes a difference: the GNU assembler rejects most of
the instructions CompCert generates for ARMv6 with "-mthumb" if the
architecture is specified as ".arch armv6" as opposed to ".arch armv6t2".
This patch fixes the architecture specification in the target printer and
the internal name of the architecture. It does not change the configure
script's flags to avoid breaking changes.
* Always use ARM movw/movt to load large immediates
These move-immediate instructions used to be only emitted in Thumb mode, not
in ARM mode. As far as I understand ARM's documentation, these instructions
are available in *both* modes in ARMv6T2 and above. This should cover all of
CompCert's ARM targets.
Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is
now identical to Clang, and the GNU assembler accepts these instructions in
all configurations.
* Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6
- define separate architecture models for ARMv6 and ARMv6T2
- introduce `Archi.move_imm` parameter on ARM to identify models with
`movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM
and Thumb mode)
* Fixes for support for architectures with Thumb2
- rename relevant parameter to `Archi.thumb2_support`
- on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb)
- allow generation of `sbfx` in ARM mode if Thumb2 is supported
|
|\
| |
| | |
Strength reduction patterns for ARM mla instruction.
|
|/ |
|
|
|
|
| |
Some alignments were wrong. Follow-up to [4d099ef].
|
|
|
|
| |
Even with __GNUC__ undefined, the standard header files contain bizarre __attribute__ declarations that CompCert fails to parse.
|
|
|
|
| |
It got lost during the addition of the x86-64 port in release 3.0.
|
|
|
|
|
| |
Not very useful in practice (make clean is generally done before make all)
and problematic under Cygwin where ../../ccomp is really ../../ccomp.exe
|
|
|
|
|
| |
The latter, in conjunction with some values of the umask, gives weird messages
"new permissions are ... not ...".
|
|
|
|
|
| |
Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert.
Remove 'Require Export' from Clightdefs as suggested in issue #199.
|
|
|
|
| |
Otherwise the interpreter uses the system's header files instead of CompCert's. This can lead to mismatches e.g. on the definition of wchar_t.
|
| |
|
|
|
|
|
|
| |
of type Tfloat
A default size of 1 was used instead of the correct "typesize ty".
|
| |
|
| |
|
|
|
|
| |
E.g. "-Os" for testing in "optimize for size" mode, or "-mthumb" for testing ARM in Thumb2 mode.
|
|
|
|
| |
Running times were too long when executed on low-end ARM or PowerPC hardware, or under QEMU emulation.
|
|
|
|
|
|
|
| |
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.
|