| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
|
|
|
|
|
|
|
|
|
| |
The "stof" and "utof" runtime functions contain a round-to-odd step
that avoids double rounding. However, this step was incorrectly coded
on PowerPC (stof and utof), PowerPC64 (utof), and ARM (stof), making
round-to-odd ineffective and causing double rounding.
Closes: #343
|
|
|
|
|
| |
This is a special value that causes double rounding with the naive
conversion schema int64 -> float64 -> float32.
|
|
|
|
|
|
|
|
| |
Introduce an error message for section attributes with non string
arguments,and another for multiple, ambiguous section attributes.
This is more consistent with the handling of other
attributes, like packed, than the old behavior of silently
ignoring them.
|
|
|
| |
In case of redefinition of a typedef name with a different type.
|
|
|
|
|
|
|
|
| |
Double FP arguments passed on stack were incorrectly aligned:
they must be 8-aligned but were 4-aligned only.
This was due to the use of `Location.typealign`, which is the minimal
hardware-supported alignment for a given type, namely 1 word for type Tfloat.
To get the correct alignments, `Location.typesize` must be used instead.
|
|
|
|
|
| |
The proof script for Events.excall_free_ok was incomplete
if Archi.ptr64 is unknown (as in the RISC-V case).
|
|
|
|
|
|
|
|
| |
According to ISO C, `free(NULL)` is correct and does nothing.
This commit updates accordingly the formal semantics of the `free`
external function and the reference interpreter.
Closes: #334
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The EABI and the SVR4 ABI state that single-precision FP arguments passed
on stack are passed as a 64-bit word, extended to double-precision.
This commit implements this behavior by using a stack slot of type Tany64.
Not only this ensures that the slot is of size and alignment 8 bytes,
but it also ensures that it is accessed by stfd and lfd instructions,
using single-extended-to-double format.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
| |
GCC does passes single arguments as singles on the stack but diab
and the eabi say single arguments should be passed as double on
the stack.
This commit changes the alignment of single arguments to 4 for
gcc based backends.
|
|
|
|
|
|
|
|
|
|
|
|
| |
We were implementing the ABI described in the RISC-V Instruction Set
Manual, version 2.1. However, this ABI was superseded by the RISC-V
ELF psABI specification.
This commit changes the calling conventions to better match the ELF psABI
specification. This should greatly improve interoperability with code
compiled by other RISC-V compilers.
One incompatibility remains: when all 8 FP argument registers have been used, further FP arguments should be passed in integer argument registers if available, while this PR passes them on stack.
|
|
|
|
| |
See ISO C2011 standard, section 6.4.4.4 para 11.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
According to AAPCS64 (the AArch64 ABI specification), the
top bits of the register containing the function result have
unspecified value, so we need to sign- or zero-extend the function result
before using it, as in the x86 port.
|
|
|
|
|
|
| |
"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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some ABIs leave more flexibility concerning function return values
than CompCert expects.
For example, the x86 ABI says that a function result of type "char" is
returned in register AL, leaving the top 24 bits of register EAX
unspecified, while CompCert expects EAX to contain 32 valid bits,
namely the zero- or sign-extension of the 8-bit result.
This commits adds a general mechanism to insert "re-normalization"
conversions on the results of function calls. Currently, it only
deals with results of small integer types, and inserts zero- or
sign-extensions if so instructed by a platform-dependent function,
Convention1.return_value_needs_normalization.
The conversions in question are inserted early in the front-end, so
that they can be optimized away in the back-end.
The semantic preservation proof is still conducted against the
CompCert model, where the return values of functions are already
normalized. What the proof shows is that the extra conversions have
no effect in this case. In future work we could relax the CompCert model,
allowing functions to return values that are not normalized.
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We can get linker errors for addresses of the form "symbol + offset"
where "symbol" is in the small data area and "offset" is large enough
to overflow the relative displacement from the SDA base register.
To avoid this, this commit enriches `C2C.atom_is_small_data`,
which is the implementation of `Asm.symbol_is_small_data` in the PPC port,
with a check that the offset is within the bounds of the symbol.
If it is not, `Asm.symbol_is_small_data` returns `false` and Asmgen produces
an absolute addressing instead of a SDA-relative addressing.
To implement the check, we record the sizes of symbols in the atom table,
just like we already record their alignments.
|
|
|
|
| |
Some preprocessors don't remove the vertical tab from the input
so we should be able to handle them in the lexer.
|
|
|
|
|
|
|
| |
Casting from an integer constant to pointer on 64 bit
architectures did not take the signedness into account and always
interpreted the integer as unsigned which causes some
incompatibility with libc implementations.
|
|
|
|
|
|
|
|
| |
Ranges of locations are relative to some base address. Most times
this is just the same as the compilation unit. However if the
compilation unit contains functions in multiple sections we need
to add a base address of the section that the locations are
contained.
|
|
|
|
|
|
|
|
| |
debug/DwarfPrinter.mli: unused functor parameter trigger warning 69,
replace by non-dependent functor type.
Makefile.extr: turn warning 69 (unused functor parameter) off
for extracted code
configure: accept OCaml versions above 4.09
configure: update messages for unsupported versions of OCaml and Coq
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Since Menhir version 20200123, we need to link with menhirLib.cmxa
instead of menhirLib.cmx.
This commit chooses automatically the file to link with:
menhirLib.cmxa if it exists in the menhirLib installation directory,
menhirLib.cmx otherwise.
To reliably find the installation directory, configure was changed
to record the menhirLib directory in Makefile.config, variable MENHIR_DIR,
instead of a pre-cooked command-line option MENHIR_INCLUDES.
Makefile.extr was adapted accordingly.
Fixes: #329
Closes: #330
|
|
|
|
| |
Update configure.
Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
|
|
|
|
|
| |
Currently, the extra size for the variable arguments is too small
for the 64 bit RISC-V and the extra arguments are stored in the
wrong stack slots.
|
|
|
|
| |
Just moved a frequent failure case ahead of a costly "simpl".
|
| |
|
|
|
|
| |
This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
|
|
|
|
|
|
|
|
|
| |
Previously, using an unknown builtin function was treated like any
other call to an undeclared function: a warning was emitted, and
an error occurred at link-time.
With this commit, using an unknown builtin function is an error,
like in Clang.
|
|
|
|
|
|
|
| |
The `__builtin_nop` function is documented only for PowerPC.
It was added to the other architectures by copy paste, but has no
known uses. So, remove `__builtin_nop` from all architectures
but PowerPC.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time.
This PR extends the check for a representable offset for the addressing of global
variables to also check whether the variable is correctly aligned. Only if both conditions are
met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic
loadsymbol sequence.
|
| |
|
| |
|
|
|
|
|
|
|
| |
Instead of constructing four different lists for maintaining the
state of the warnings only one list is now used. This list contains
the name of the warning and a boolean indicating whether this option
should be active by default. The rest is computed from this list.
|
| |
|
|
|
|
| |
A stronger `intuition` in the near future would break this use of `intuition`.
|
|
|
| |
At least OCaml 4.05 is now required as well as Coq 8.8.
|
|
|
|
| |
The proposed proof only uses `zify` for closing the goal. This is
needed for Coq PR #10982 which changes the inner working of `zify`.
|
| |
|
|
|
|
|
| |
A "dollar" sign in a function name or a global variable name was producing
incorrect Coq identifiers. (Issue #319.)
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|