| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
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
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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 configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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`.
|
| |
| |
| |
| |
| |
| |
| |
| | |
The .const section cannot contain absolute references to symbols,
as these may need relocation and therefore must be writable.
This should be fixed more generally by distinguishing between initialization
data that contains absolute references to symbols and initialization data
that does not.
|
| |
| |
| |
| |
| | |
This commit adds support for macOS (and probably iOS) running on
AArch64 / ARM 64-bit / "Apple silicon" processors.
|
| |
| |
| |
| |
| | |
The extended register is now printed as an X register if the
extension mode is UXTX, and as a W register otherwise.
|
| |
| |
| |
| |
| | |
The alignment was 2 bytes (like for ARM) but should be 4 bytes.
It was ignored by the GNU assembler, but the LLVM assembler warns.
|
| | |
|
| | |
|
|\ \ |
|
| | | |
|
|\| | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
|\ \ \
| |/ /
|/| |
| | | |
Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
aarch64-peephole
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
|\ \ \ \ \ \ \
| | |_|_|_|/ /
| |/| | | | | |
|
| | |_|_|/ /
| |/| | | | |
|
| |\ \ \ \ \
| | | |_|_|/
| | |/| | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Pfmovimms, Pfmovimmd destroy X16
Pbtbl preserves X17
Inlined built-in functions destroy X16 and X30
|
| |\ \ \ \ \
| | | |_|_|/
| | |/| | |
| | | | | |
| | | | | |
| | | | | | |
Conflicts:
Makefile
configure
|