| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
|
|
|
| |
Commit 1df887f breaks compilation on some Windows environments,
those where the output of `menhir --suggest-menhirLib` contains `\r\n` end-of-lines
or backslashes in paths. The fix is to filter the output.
Closes: #304 Changes in configure broke Windows build
|
|
|
|
|
|
| |
The generation of some fresh names changes in Coq 8.10 (https://github.com/coq/coq/pull/9160).
The `Hint Mode` declaration that does not specify a hint database now triggers a warning.
Specify the intended database and fix the "auto" tactics accordingly.
|
| |
|
|
|
|
| |
Updated man page + better usage message.
|
|
|
|
|
| |
Easier to type, and consistent with `-Os` (optimize for smaller code /
optimize for fewer conditional branches).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
What's new:
1. A rewrite of the Coq interpreter of Menhir automaton, with
dependent types removing the need for runtime checks for the
well-formedness of the LR stack. This seem to cause some speedup on
the parsing time (~10% for lexing + parsing).
2. Thanks to 1., it is now possible to avoid the use of int31 for
comparing symbols: Since this is only used for validation,
positives are enough.
3. Speedup of Validation: on my machine, the time needed for compiling
Parser.v goes from about 2 minutes to about 1 minute. This seem to
be related to a performance bug in the completeness validator and
to the use of positive instead of int31.
3. Menhir now generates a dedicated inductive type for
(semantic-value-carrying) tokens (in addition to the already
existing inductive type for (non-semantic-value-carrying)
terminals. The end result is that the OCaml support code for the
parser no longer contain calls to Obj.magic. The bad side of this
change is that the formal specification of the parser is perhaps
harder to read.
4. The parser and its library are now free of axioms (I used to use
axiom K and proof irrelevance for easing proofs involving dependent
types).
5. Use of a dedicated custom negative coinductive type for the input
stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
positive coinductive type, which are now deprecated by Coq.
6. The fuel of the parser is now specified using its logarithm instead
of its actual value. This makes it possible to give large fuel
values instead of using the `let rec fuel = S fuel` hack.
7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
The corresponding changes in Menhir have been released as part of
version 20190626. The `MenhirLib` directory is identical to the
content of the `src` directory of the corresponding `coq-menhirlib`
opam package except that:
- In order to try to make CompCert compatible with several Menhir
versions without updates, we do not check the version of menhir
is compatible with the version of coq-menhirlib. Hence the
`Version.v` file is not present in CompCert's copy.
- Build-system related files have been removed.
|
|
|
|
| |
The previous code was unintentionally relying on a strange behavior of `Export` (see https://github.com/coq/coq/issues/10480) that will be removed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The new diagnostics is triggered if a conditional is used that
may not be transformed into linear code by the later by the
if conversion.
The new diagnostic is emitted if a conditional may contain an
unsafe expression or is contained within another conditional,
logical and or logical or expression. An expression is unsafe if
it contains a call, changes memory or if its evaluation leads to
undefined behavior, for example division and modulo.
Also fixes a small typo in a comment in Cutil.
|
|
|
|
|
| |
The function determines whether the given type is an array type
or not.
|
|
|
|
|
|
| |
Refactored the checks functions by using higher order traversal
functions for statements. Also introduce helper functions for the
traversal of initializers.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, the arguments to __builtin_annot, __builtin_ais_annot,
__builtin_debug, and extended asm statements are treated like
arguments to an unprototyped or vararg function call. In particular,
arguments of type "float" are converted to "double", generating useless
code.
To avoid this extra, useless conversion, this commit changes the types
expected for the arguments to these built-ins and to extended asm
statements. Now they are the types of the arguments themselves, after
performing the usual unary conversions (e.g. char -> int), but without
the problematic float -> double conversion. This ensures that no code
is generated to change the representation of the arguments.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When printing an extended asm code fragment, placeholders %n
are replaced by register names.
Currently we ignore the fact that some assemblers use different
register names depending on the width of the data that resides
in the register.
For example, x86_64 uses %rax for a 64-bit quantity and %eax for
a 32-bit quantity, but CompCert always prints %rax in extended asm
statements. This is problematic if we want to use 32-bit integer
instructions in extended asm, e.g.
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
produces
addl %rax, %rdx
which is syntactically incorrect.
Another example is ARM FP registers: D0 is a double-precision float,
but S0 is a single-precision float.
This commit partially solves this issue by taking into account the
Cminor type of the asm parameter when printing the corresponding register.
Continuing the previous example,
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
now produces
addl %eax, %edx
This is not perfect yet: we use Cminor types, because this is all we
have at hand, and not source C types, hence "char" and "short" parameters
are still printed like "int" parameters, which is not good for x86.
(I.e. we produce %eax where GCC might have produced %al or %ax.)
We'll leave this issue open.
|
| |
|
|
|
|
|
| |
A conditional move whose condition is statically known becomes a regular move.
Otherwise, the condition can sometimes be simplified by strength reduction.
|
| |
|
|
|
|
|
|
|
| |
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.
|