| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
| |
A self assign `x = x` can be classified as a skip in `classify_stmt`.
This helps with the if-conversion of some code that the previous passes
generates, e.g. for nested C conditional expressions.
Closes: #466
|
|
|
|
|
|
|
|
|
| |
Variadic functions can use the stack frame to store values of registers.
Hence, a pointer within the stack frame can be put in a va_list, and
the stack frame should not be deallocated before a function call that
may use this va_list.
Fixes: #473
|
|
|
|
| |
Adapt w.r.t. coq/coq#16904.
|
| |
|
|
|
|
|
|
| |
And re-enable the `undeclared-scope` warning.
`Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
|
| |
|
|
|
|
|
|
| |
Improves robustness in case of stronger (e)auto.
This is in preparation of a change in Coq that will make auto and eauto stronger
(https://github.com/coq/coq/pull/16293).
|
|
|
|
|
|
|
|
| |
Ignore debug statements that could have prevented the recognition
of a simple assignment.
Since debug statements can formally get stuck, revise the simulation
diagram to use the "eventually" modality.
|
|
|
|
|
|
|
|
|
|
| |
The `reset_constants` was only used for ARM and there it was superfluous
since the jumptables, which it additionally resets in contrast to
`reset_literals`, are always empty since jumptables are handled directly
in during printing of the instruction.
The `exists_constants` function is now also unused since we test directly
for the different sizes in `emit_constants`.
|
|
|
|
|
|
|
| |
Use the same code to split 64 bit literals into two 32 bit halfs as is
used for 64 bit initialization data and print them in PrintAsm. This
removes the need for a target specific printing function for 64 bit
literals.
|
|
|
|
|
|
| |
The function was the same for nearly all backends and also the way 32 bit
literals are printed so we moved it to PrintAsm. The 64 bit literals
however are still target specific.
|
|
|
|
| |
This makes compilation runs more reproducible.
|
|
|
|
|
|
|
|
|
|
|
|
| |
On platforms that support them (ELF, macOS), use mergeable sections
(like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals.
Works only if the LITERAL section is the default one. If the user
provided their own LITERAL section, all literals are put in it
regardless of their sizes.
Support for mergeable string sections is introduced in this commit too
but needs further changes in C2C.ml .
|
|
|
|
|
|
|
|
|
|
| |
As written previously, OCaml can evaluate `nodeOfVar g v1` and
`nodeOfVar g v2` in any order. Consequently, `v1` and `v2` can be
entered in the `varTable` hash table in different order. This can
result in different (but equally valid) register allocations.
It's better to enforce one evaluation order for the sake of
reproducible compilations when the OCaml version changes.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This PR replaces the "PTree" data structure used in lib/Maps.v by the
canonical binary tries data structure proposed by A. W. Appel and
described in the paper "Efficient Extensional Binary Tries",
https://arxiv.org/abs/2110.05063
The new implementation is more memory-efficient and a bit faster,
resulting in reduced compilation times (-5% on typical C programs, up
to -10% on very large C functions).
It also enjoys the extensionality property (two tries mapping equal
keys to equal data are equal), which simplifies some proofs.
|
|
|
|
| |
This avoids a new warning of Coq 8.14.
|
|
|
|
|
|
| |
Instead, add `Set Asymmetric Patterns` to the files that need it,
or use `Arguments` to make inductive types work better with symmetric patterns.
Closes: #403
|
|
|
|
|
|
|
|
|
|
|
| |
Warning 69 "mutable record field is never mutated":
3 occurrences in backend/IRC.ml
removed the "mutable" qualifier on these fields
Warning 70 "cannot find interface file"
many .ml files have no .mli
no strong motivation to add the .mli files
turned off the warning in Makefile.extr
|
|
|
|
|
|
| |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
|
|
|
|
|
|
| |
Variables without init do not generated any assembly code so no entry in
the json AST should be generated. They correspond to extern variables
without initializer that are defined in another compilation unit.
Bug 30112
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On PowerPC/Diab, common declarations must not be used for small data sections.
Add a `~common` option to `PrintAsmaux.variable_section` to control
the use of common declarations. The default is whatever is specified
on the command line using the `-fcommon` and `-fno-common` options.
Use `~common:false` for `Section_small_data` on PowerPC / Diab.
Note that on PowerPC/Linux, GCC uses common declarations for uninitialized
variables in small data section, so we keep doing this in CompCert as well.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Distinguish between:
- uninitialized variables, which can go in COMM if supported
- variables initialized with fixed, numeric quantities,
which can go in a readonly section if "const"
- variables initialized with symbol addresses which may need relocation,
which cannot go in a readonly section even if "const",
but can go in a special "const_data" section.
Also: on macOS, use ".const" instead of ".literal8" for literals,
as not all literals have size 8.
|
|
|
|
|
|
|
| |
This is a generalization of the previous PrintAsmaux.common_section
function that
- handles initialized variables in addition to uninitialized variables;
- can be used for Section_const, not just for Section_data.
|
|
|
|
|
|
|
| |
This avoids a new warning of Coq 8.13.
Eventually these `Global Hint` should become `#[export] Hint`,
with a cleaner but different meaning than `Global Hint`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The previous branch tunneling was missing optimization opportunities
introduced by the optimization of conditional branches. For example:
L1: instr; branch L2
L2: if cond then branch L3 else branch L4
L3: branch L4
L4: ...
was transformed into
L1: instr; branch L2
L2: branch L4
L3: branch L4
L4: ...
missing a tunneling opportunity (branch L2 -> branch L4).
This commit improves branch tunneling so that the expected code is produced:
L1: instr; branch L4
L2: branch L4
L3: branch L4
L4: ...
To this end, additional equalities are introduced in the union-find
data structure corresponding to optimizable conditional branches.
In rare cases these additional equalities trigger new opportunities for
optimizing conditional branches. Hence we iterate the analysis
until no optimizable conditional branch remains.
|
|
|
|
|
|
|
|
|
|
| |
We used to define an instrumented version record_goto' that also
builds the measure f, prove it correct, then show equivalence with
record_goto.
The new proofs make do without the instrumented version. They prove
strong existence of the measure, as in
`{ f | branch_map_correct (record_goto fn) f}`.
|
|
|
|
|
|
|
|
|
|
|
| |
Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal.
Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`,
and `xomegaContradiction` with `lia` and `extlia`.
Turn back on the deprecation warning for uses of `omega`.
Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
|
|
|
|
|
|
| |
Instead of being a simple boolean we now use an option type to record
the number of fixed (non-vararg) arguments. Hence, `None` means
not vararg, and `Some n` means `n` fixed arguments followed with varargs.
|
| |
|
| |
|
|
|
|
|
| |
The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A typical example is `(void) __builtin_sel(a, b, c)`.
It is safe to generate zero code for these uses of builtins
because builtins whose semantics are known to the compiler
are pure. Other builtins with side effects (e.g. `__builtin_trap`)
are not known and will remain in the compiled code.
It is useful to generate zero code for these uses of builtins
because some of them (e.g. `__builtin_sel`) must be transformed
into proper CminorSel expressions during instruction selection.
Otherwise, they propagate all the way to ExpandAsm, causing
a "not implemented" error there.
|
|
|
|
|
|
|
| |
As detected by the new warning in Coq 8.12.
The use of Fixpoint here is not warranted and either an oversight or a
leftover from an earlier version.
|
|
|
|
|
|
|
| |
The list of reserved_registers is never reset between the compilation of
multiple files. Instead of storing them in IRC they are moved in the
CPragmas file and reset in the a new reset function for Cpragmas whic is
called per file.
|
|
|
|
|
|
|
|
| |
Currently we require the memory to be unchanged on readonly locations.
This is too strong. For example, current permissions could decrease
from readonly to none.
This commit weakens the ec_readonly condition to the strict minimum
needed to show the correctness of value analysis for const globals.
|
|
|
|
|
|
|
|
|
|
|
|
| |
Until now the types Tany32 and Tany64 were not used prior to register
allocation, so IRC.class_of_type did not need to be defined for
those types.
However, there are possible uses of stack slots of type Tany32 and Tany64
to specify calling conventions. For this purpose, we need to define
class_of_type for Tany32 and Tany64. We follow the informal convention
that Tany32 goes in integer registers and Tany64 goes into integer
registers if 64-bit wide, or FP registers otherwise.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The "size_arguments" function and its properties can be systematically
derived from the "loc_arguments" function and its properties.
Before, the RISC-V port used this derivation, and all other ports
used hand-written "size_arguments" functions and proofs.
This commit moves the definition of "size_arguments" to the
platform-independent file backend/Conventions.v, using the systematic
derivation, and removes the platform-specific definitions.
This reduces code and proof size, and makes it easier to change the
calling conventions.
|
|
|
|
|
|
| |
"open!" is the form used in the examples in the OCaml manual.
Based on a quick poll it seems to be the preferred form of the OCaml
core dev team.
|
|
|
|
|
|
|
|
|
|
| |
Before it was "option typ". Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).
One benefit is that external functions get more precise types that
control better their return values. As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.
|
| |
|
|
|
|
|
|
|
| |
Some hints will move from the core database to the `ordered_type` database
(see https://github.com/coq/coq/pull/9772).
This commit prepares for this move by adding `with ordered_type` to the invocations
of `auto` and `eauto` that use the hints in question.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The json export prints formatted json, which takes a lot of
additional time, however the result is only consumed by other tools
and not meant for human reading.
This commit implements several small changes in order to speedup
the json export:
* Removal of usage of the Format Module
* Replacing `fprintf` calls by calls to function that print
directly, such as `output_string`, etc.
* Replacing list of all instruction names by a set of all
instructions
|
|
|
| |
Some changes were not correctly propagated to all architectures.
|
|
|
|
|
| |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
|
|
|
|
|
|
|
|
|
| |
This is a variant of exec_straight where it is allowed to take zero steps.
In other words, exec_straight0 is the "star" relation, while exec_straight
is the "plus" relation.
In the end we need "plus" relations in simulation diagrams, to show
the absence of stuttering. But the "star" relation exec_straight0 is
useful to reason about code fragments that are always preceded or
followed by at least one instruction.
|
|
|
|
|
| |
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
|
|
|
|
| |
Known built-in functions are guaranteed not to change memory.
|
|
|
|
|
|
|
| |
When an external function is a known built-in function and it is
applied to compile-time integer or FP constants, we can use
the known semantics of the builtin to compute the result
at compile-time.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds mechanisms to
- recognize certain built-in and run-time functions by name and signature;
- associate semantics to these functions, as a partial function from
list of values to values;
- interpret external calls to these functions according to this semantics
(pure function from values to values, memory unchanged, no observable
events in the trace);
- external calls to unknown built-in and run-time functions remain
interpreted as generating observable events and possibly changing
memory, like before.
The description of the built-ins is split into a target-independent
part (in common/Builtins0.v) and a target-specific part (in
$ARCH/Builtins1.v).
Instruction selection uses the new mechanism in order to
- recognize some built-in functions and turn them into operations
of the target processor. Currently, this is done for
__builtin_sel and __builtin_fabs; more to come.
- remove the axioms about int64 helper functions from the standard
library. More precisely, the behavior of these functions is
still axiomatized, but now it is specified using the more general
machinery introduced in this commit, rather than ad-hoc axioms
in backend/SplitLongproof.
The only built-ins currently described are __builtin_fsqrt (for all platforms)
and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be
added later.
|