| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|/
|
|
|
|
| |
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.
|
|/ |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
|
|
|
|
| |
Since commit e5b37a6 (useless conditional branch elimination), the proof of the Tunneling pass was assuming forall c, destroyed_by_cond c = nil. This is not true for architecture variants that we will support soon. This commit rewrites the proof so as to remove this assumption. The old proof was by memory and value equalities, the new one is by memory extensions and "lessdef" values.
|
| |
|
| |
|