| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| ... | |
| |
|
|
|
| |
- 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.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes.
The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/
This port required the following additional changes:
- Integers: More properties about shrx
- SelectOp: now provides smart constructors for mulhs and mulhu
- SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu.
- Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library.
- test/: add SIMU make variable to run tests through a simulator
- test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers
commit da14495c01cf4f66a928c2feff5c53f09bde837f
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu Apr 13 17:36:10 2017 +0200
RISC-V port, continued
Now working on Asmgen.
commit 36f36eb3a5abfbb8805960443d087b6a83e86005
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed Apr 12 17:26:39 2017 +0200
RISC-V port, first steps
This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
- Avoid reloading LR before a tail call if we're in a leaf function
- Factor out the code that reloads LR if necessary (function Asmgen.transl_epilogue)
- Factor out the corresponding parts of the proof (Asmgenproof1.transl_epilogue_correct, Asmgenproof.step_simulation)
|
| |
|
|
|
|
|
|
|
|
| |
Leaf functions are functions that do not call any other function. For leaf functions, it is not necessary to save the LR register on function entry nor to reload LR on function return, since LR contains the correct return address throughout the function's execution.
This commit suppresses the reloading of LR before returning from a leaf function. LR is still saved on the stack on function entry, because doing otherwise would require extensive changes in the Stacking pass of CompCert. However, preliminary experiments indicate that we get good speedups by avoiding to reload LR, while avoiding to save LR makes little difference in speed.
To support this optimization and its proof:
- Mach is extended with a `is_leaf_function` Boolean function and a `wf_state` predicate to provide the semantic characterization.
- Asmgenproof* is extended with a `important_preg` Boolean function that means "data register or LR". A number of lemmas that used to show preservation of data registers now show preservation of LR as well.
|
| |
|
|
|
|
| |
Instructions expanded by Asmexpand should never end up in
AsmToJSON.
Bug 21345
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
ISO C99 states that "inline defintions", functions with inline
specifier that are not extern, does not provide an external
definition and another compilation unit can contain an external
definition. Thus in the case of non-static inline functions no
code should be generated.
Bug 21343
|
| |
|
|
|
|
| |
The new option f(no-)inline controlls whether inlining is active
or not.
Bug 21343.
|
| |
|
|
|
|
|
|
|
|
| |
This commit eliminates useless conditional branches during the branch tunneling pass over LTL. Conditional branches where both successors go to the same LTL node are turned into unconditional branches, which will stay or be eliminated by the subsequent Linear pass.
One code pattern that triggers this optimization is an empty if/else at the C source level. Commit 4d7a459 eliminates these empty if/else statements early, during the Compcert C -> Clight translation. I think it's good to have both optimizations:
- Early elimination makes sure these empty if/else cause no overhead whatsoever, and in particular cannot degrade the precision of later static analyses.
- Late elimination catches the case where a nonempty if/else in the source becomes empty as a consequence of optimizations.
Future work? If the optimization in Tunneling triggers, it might be worth re-running the Tunneling pass once more, to make sure that the "Lgoto" introduced by the optimization is properly tunneled / skipped over when appropriate.
|
| | |
|
| | |
|
| |
|
|
| |
`-admit Floats` is no longer needed, but Integers and SelectDivproof still need admitting.
|
| |
|
|
|
|
| |
If the label is on a different line than the code we can still
emit a line directive for the label.
Bug 21232
|
| | |
|
| |
|
|
|
|
|
| |
Since before a case statement is potentially unreachable code due
to break, etc. it is better to skip printing line information
directly before the case statement and print it afterwards.
Bug 21232
|
| |
|
|
| |
alloctrace debug-output
|
| |
|
|
|
|
| |
Instead of using Filename.quote, string entries are printed with
%S.
Bug 21216
|
| |
|
|
|
|
| |
The compilation directory entry needs quoting since it could be
a toplevel directory under windows.
Bug 21216
|
| |\
| |
| |
| |
| |
| |
| | |
Adapt proofs to future handling of literal constants in Coq
This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
|
| | |
| |
| |
| |
| |
| | |
This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
| |
The check tests whether the size calculation of an array overflows
or the array covers half of the available address space and reports
an error in this case.
Bug 21034
|
| | |
|
| |
|
|
| |
The noinline attribute prevents functions from inlining.
|
| |
|
|
|
|
|
|
|
| |
The attribute unused can be used to indicate if a variable or
parameter is unused and no warning should be emitted for it.
Furthermore this commit simplifies the check by adding a generic
function to traverse the program.
Bug 19872
|
| |
|
|
|
|
|
|
|
| |
The unused variable check now uses two passes. One to collect the
used variables and one to report the unused variables.
Futhermore attribute checks are extended to composite declaration.
Also the check is now performed after elaboration.
Bug 19872
|
| |
|
|
|
|
| |
The test now also checks whether the parameter are used at all in
the function body.
Bug 19872
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The check test whether the identifier is used at all in the
function and if not issue a warning. It is not tested whether the
usage is reachable at all, so
int i;
if (0)
i;
would not generate a warning. This is the same as gcc/clang does.
The warning is disabled per default, but is active if -Wall is
given.
Bug 19872
|
| |
|
|
|
|
| |
There should not be a single check place, since for example
unknonw attributes should be check after elaboration and other
simplifications.
|
| | |
|
| |
|
|
|
|
|
| |
The new module adds a function which is called during parse after
all C transformation have taken place for adding additional
checks. Currently only unknown attribute are checked.
Bug 19872
|
| |
|
|
|
|
| |
As a cosmetic optimization enabled by the static analysis in Cflow, we used to not insert a 'return 0' at end of 'main' if the body of 'main' cannot fall through.
Since this optimization is cosmetic (the back-end will remove the 'return 0' if unused) and since we don't fully trust this static analysis, revert this optimization and always insert 'return 0'.
|
| |
|
|
| |
If no 'default' case appears in a 'switch', one is implicit at the end of the switch body, making possible to have a fall-through behavior.
|
| |\
| |
| |
| | |
Treat as _Noreturn the standard C11 functions that are _Noreturn but not always declared as such in header files.
|
| | | |
|
| | | |
|
