| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
| |
|
|\
| |
| |
| | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
|
| | |
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\
| |
| |
| | |
mppa-if-conversion
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Extends the instruction selection pass with an if-conversion optimization:
some if/then/else statements are converted into "select" operations,
which in turn can be compiled down to branchless instruction sequences
if the target architecture supports them.
The statements that are converted are of the form
if (cond) { x = a1; } else { x = a2; }
if (cond) { x = a1; }
if (cond) { /*skip*/; } else { x = a2; }
where a1, a2 are "safe" expressions, containing no operations that can
fail at run-time, such as memory loads or integer divisions.
A heuristic in backend/Selectionaux.ml controls when the optimization occurs,
depending on command-line flags and the complexity of the "then" and "else"
branches.
|
| |
| |
| |
| |
| |
| |
| | |
This module is similar to RTLtyping: it performs type inference and
type checking, but on the Cminor intermediate representation rather
than the RTL IR. For each function, it returns a mapping from variables
to types. Its first use will be if-conversion optimization.
|
| |
| |
| |
| |
| | |
If the source language is determinate, it can take several steps
(not just one) before the "match_state" invariant is reinstated.
|
| |
| |
| |
| |
| |
| | |
This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
|
| |
| |
| |
| |
| |
| | |
The FP select for PowerPC stores both addresses in two
subsequent stack slots and loads them using an offset created
from the result of the comparison.
|
| |
| |
| |
| |
| | |
This function and its proof should have been part of commit 43e7b67.
They are already there for the other ports.
|
| |
| |
| |
| |
| | |
The "vmov" instruction (Advanced SIMD) cannot be conditional.
The "vmov.f64" instruction (VFPv2) can be conditional.
|
| |
| |
| |
| | |
It works fine with the current sources.
|
| | |
|
| |
| |
| |
| |
| |
| | |
The arguments that are passed to an unprototyped function must
also be checked to be valid types passed to a function, i.e. they
must be complete types after argument conversion.
|
| |
| |
| |
| |
| | |
No `Osel` operation for this port, so `SelectOp.select` always
returns None.
|
| |
| |
| |
| |
| | |
The operation comples down to conditional moves.
Both integer and floating-point conditional moves are supported.
|
| |
| |
| |
| | |
The operation compiles down to conditional moves.
|
| |
| |
| |
| |
| | |
On non-EREF processors it expands to instructions that destroy GPR0.
Reflect this in the Asm semantics for Pisel.
|
| |
| |
| |
| |
| | |
This operation compiles down to an `isel` instruction (conditional move).
The semantics is given by `Val.select`.
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
`Val.select ob v1 v2 ty` is a conditional operation that chooses between
the values `v1` and `v2` depending on the comparison `ob : option bool`.
If `ob` is `None`, `Vundef` is returned.
If the selected value does not match type `ty`, `Vundef` is returned.
This operation will be used to model a "select" (or "conditional move")
operation at the CminorSel/RTL/LTL/Mach level.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This will be useful to implement a "select" (conditional move) operation later.
- Introduce `Asmgen.loadimm64_notemp` to load a 64-bit integer
constant into a register without going through memory and without
needing a temporary register.
- Use `Asmgen.loadimm64_notemp` instead of `Asmgen.loadimm64` in the
compilation of conditions, so that GPR12 is no longer needed as a
temporary.
- Share code and proofs common to the two `Asmgen.loadimm64_` functions
as the `Asmgen.loadimm64_32s` function.
|
| |
| |
| |
| |
| |
| |
| |
| | |
Following the gnu Makefile Conventions the variable $(DESTDIR)
should be prepended to all installation commands. This allows
staged installs.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Since a definition/declaration is completed with after the
separator to the next init group member it is also possible to
use it for example in the next init group member:
char s[]="miaou", buf[sizeof s];
In order to ensure that this works the declarations are added to
the environment directly during the elaboration of the init member
group instead of later.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The option -fcommon controls whether uninitialized global
variables are placed in the COMMON section. If the option is given
in the negated form, -fno-common, variables are not placed in the
COMMON section. They are placed in the same sections as gcc does.
If the variables are not placed in the COMMON section merging of
tentative definitions is inhibited and multiple definitions lead
to a linker error, as it does for gcc.
|
| |
| |
| |
| |
| | |
The AbsInt build number no longer contains "release", so it must
be printed additionally.
|
| |
| |
| |
| |
| |
| | |
`_Complex` and `_Imaginary` are reserved keywords. Since CompCert does
not support these types they could be used as identifiers. However
the standard requires to reject this.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Pass the environment to all expr eval functions since
the functions themselve may be called recursively and modify
the environment.
The other change introduces new scopes that are strict
subsets of their surrounding scopes for if, switch, while,
do and for statement, as prescribed by ISO C standards.
|
| |
| |
| |
| |
| | |
Since the error formatter is not automatically flushed at program
exit we need to ensure that it is flushed at exit.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* Move the expansion of response files to module Commandline,
during the initialization of `Commandline.argv`.
This way we're sure it's done exactly once.
* Make `Commandline.argv` a `string array` instead of a `string array ref`.
We no longer need to update it after initialization!
* Improve reporting of errors during expansion of response files.
|