| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | | |
| | | |
| | | |
| | | | |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
"deep" inside expressions
For example, with this option,
tmp = *(x + 0) + *(x + 1)
in the original Clight is rewritten to
tmp1 = *(x + 0)
tmp2 = *(x + 1)
tmp = tmp1 + tmp2
with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads.
Squashed commit of the following:
commit 3fb69dae567b1305383b74ce1707945f91369a46
commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a
commit c220ed303d9f3f36cc03c347a77b065a9362c0e7
|
|\
| |
| | |
Do not rely on the hints of BigNumPrelude
|
|/
|
|
|
|
|
|
| |
BigNumPrelude will soon leave Coq stdlib with the rest of the bignum
library (apart from Int31 files) to become a separate package.
With this (very minor) patch, Compcert compiles with or without
the hints declared in BigNumPrelude.
|
|
|
|
|
|
| |
Particularly annoying was the `*&x` sequence where `x` is a local variable, which would force stack-allocation of `x` early, generating extra loads and stores that could not always be optimized later (in CSE and Deadcode).
The `*&` sequences and, by symmetry, the `&*` sequences are now eliminated early during Clight generation, via smart constructors.
|
|\
| |
| | |
Make proof script compatible with an improvement in the 'zify' tactic
|
|/
|
|
| |
See Coq pull request #673 (and original bug #5336).
With the fixed version of zify, this proof could actually be shortened to `intros. unfold shiftpos. now zify.`, but the proposed patch has the advantage of being compatible with both the released versions of Coq, and the coming ones.
|
|
|
|
|
| |
- x86/Op: in 32-bit mode all addressings are valid because offsets are always interpreted as 32-bit signed integers in Asmgen.
- x86/ConstpropOp: in addr_strength_reduction, make sure no invalid addressing mode is generated.
|
|
|
|
|
|
|
| |
The redefinition of a composite with a different tag type is now
a fatal error. This should avoid problems when the composite is
used.
Bug 21542
|
| |
|
|\ |
|
| |
| |
| |
| | |
Commit 7873af3 introduced changes in the Conventions1.v interface. This commit implements those changes for RISC-V.
|
|/ |
|