| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
|
|
|
|
|
|
|
| |
Sometimes the result of a void function is assigned to a variable.
This can occur with C conditional expressions ?: at type void,
e.g. the "assert" macro of MacOS.
A similar relaxation was already there in RTLtyping.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
There should only be one unnamed parameter of type void in the
parameter list.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
Add a check for alignment on command-line switches `-falign-*`.
The check is similar to the one for the alignment attribute and
ensures that only powers of two can be specified.
|
|
|
|
|
|
| |
The previous implementation used to build the full powers-of-two decomposition
of the number. The present implementation recognizes powers of two directly,
then takes the log2.
|
|
|
|
|
|
|
|
| |
The `field_simplify` tactics will be improved soon (https://github.com/coq/coq/pull/9854).
Flocq was made compatible with this improvement (https://gitlab.inria.fr/flocq/flocq/commit/0752761a6a344d62f6bc728eac442ebb4ba655ac).
This commit updates CompCert's copy of Flocq accordingly.
|
|
|
|
|
| |
To match the new module names from version 3 of Flocq.
Plus, it's shorter.
|
|
|
|
|
|
|
|
|
|
| |
The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size. These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.
This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.
|
|
|
|
|
| |
Instead, use definitions and lemmas from the Coq standard library
(ZArith, Znumtheory).
|
|
|
|
|
|
|
| |
Use Z.to_nat theorems from the standard Coq library in preference to
our theorems in lib/Coqlib.v.
Simplify lib/Coqlib.v accordingly.
|
|\
| |
| |
| | |
Merge of branch dwarf-ranges
|
| |
| |
| |
| |
| |
| |
| | |
Instead of printing an the start label and adding the offset by
computing the difference of the range label and the start label
use the range label directly.
Bug 26234
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Functions that are removed from the compilation unit, for example
inline functions without extern, should not produce debug
information.
This commit reuses the mechanism used for variables in order to
track additionally the printed functions. Therefore the printed
variable versions are exchanged for a printed symbol version.
Bug 26234
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The fist changes changes the offset for range entries to used labels
instead of integer constants, leaving the computation to the
assembler.
The second part of the change the address changes the way ranges
entries of scopes are printed. They need to be relative to the start
address of the code in the section they are included.
Bug 26234
|
| |
| |
| |
| |
| |
| |
| | |
In order to avoid adding ranges to the wrong scopes due to
inlining they are numbered consecutively for the whole compilation
unit.
Bug 26234
|
| |
| |
| |
| |
| |
| | |
As noted in the DWARF 3 specification empty ranges have no effect
and can be left out.
Bug 26234
|
|/
|
|
|
|
| |
Ranges for non-contiguous address ranges are already part of dwarf
version 3.
Bug 26234
|
| |
|
|
|
| |
SEL_SWITH_INT -> SEL_SWITCH_INT
|
|
|
|
| |
These were committed by mistake.
|
|
|
|
|
|
|
|
| |
Rumor has it that this module is scheduled for removal.
This is based on pull request #286, with a different implementation.
Closes: #286
|
|
|
|
| |
In the `Sswitch` case, the original expression was used instead of the result of `norm_expr`.
|
|
|
|
|
| |
A grep through Coq's source files show that it uses more cache files
than just .lia.cache. Ignore them all.
|