| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| |
| |
| |
| | |
E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| | |
Not yet used for optimizations.
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\ \ \
| | | | |
| | | | |
| | | | | |
riscv-work-fpinit-stillexp
|
| | |/ / |
|
| |/ / |
|
| | |
| | |
| | |
| | | |
cfrontend/C2C.ml
|
| | | |
|
| | | |
|
|\ \ \
| |/ /
|/| /
| |/
| |
| |
| |
| |
| | |
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
|
| |
| |
| |
| |
| |
| |
| | |
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`.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is complementary to 28f235806
Some ABIs leave more flexibility concerning function parameters than
CompCert expects.
For instance, the AArch64/ELF ABI allow the caller of a function to
leave unspecified the "padding bits" of function parameters. As an
example, a parameter of type "unsigned char" may not have zeros in
bits 8 to 63, but may have any bits there.
When the caller is compiled by CompCert, it normalizes argument values
to the parameter types before the call, so padding bits are always
correct w.r.t. the type of the argument. This is no longer guaranteed
in interoperability scenarios, when the caller is not compiled by CompCert.
This commit adds a general mechanism to insert "re-normalization"
conversions on the parameters of a function, at function entry.
This is controlled by the platform-dependent function
Convention1.return_value_needs_normalization.
The semantic preservation proof is still conducted against the
CompCert model, where the argument 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 pass arguments that are not normalized.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a follow-up to e81d015e3.
In the RISC-V ABI, FP arguments to functions are passed in integer registers
(or pairs of integer registers) in two cases:
1- the FP argument is a variadic argument
2- the FP argument is a fixed argument but all 8 FP registers reserved for
parameter passing have been used already.
The previous implementation handled only case 1, with some problems.
This commit implements both 1 and 2. To this end, 8 extra FP
caller-save registers are used to hold the values of the FP arguments
that must be passed in integer registers. Fixup code moves these FP
registers to integer registers / register pairs. Symmetrically, at
function entry, the integer registers / register pairs are moved back
to the FP registers.
8 extra FP registers is enough because there are only 8 integer
registers used for parameter passing, so at most 8 FP arguments may
need to be moved to integer registers.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a follow-up to 2076a3bb3.
Integer registers were wrongly reserved for fixed FP arguments,
causing variadic FP arguments to end up in the wrong integer registers.
Added regression test in test/regression/varargs2.c
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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`.
|
| |
| |
| |
| |
| | |
Fixed (non-variadic) arguments follow the standard calling conventions.
It's only the variadic arguments that need special treatment.
|
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
|\ \ |
|
| | | |
|
| | | |
|
| |\ \ |
|