GitLab

When desugaring a bitfield, allow any integral type that is 32 bits
or smaller. Previously this was checking the rank of the type rather
than the size.

This rank check caused issues with standard headers that
declare `uint32_t` to be an `unsigned long` rather than an
`unsigned int`. Here, any bitfields declared as `uint32_t` were
failing to compile even though they are still actually 32 bits.
Co-authored-by: Amos Robinson <amos@gh.st>

- Use pipeline notation `|>` for legibility and better GC behavior
  (in bytecode at least).
- Introduce auxiliary functions.
- Remove useless function parameters.
- Fix the timing of the "Emulations" pass
  (because of an extra parameter, what was timed took zero time).

After Menhir version 20210310, the `Fail_pr` constructor of the
`parse_result` type becomes `Fail_pr_full` with two extra arguments.

This PR enables CompCert to handle both versions of the `parse_result`
type in MenhirLib.

coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters.
There was one place in CompCert where one of these automatically-generated names was used.
This commit avoids using this name.

Closes: #389

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.

Either because the code change that would silence the warning is not
desirable, or because it would break compatibility with earlier versions
of Coq.

Explain the silenced warnings as comments in the Makefile.

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 extraction mechanism wants to extract them (because they are in
Type, probably).  The current opaque definition causes a warning at
extraction-time.

The configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".

The standard includes print irrelevant warnings using `#warning`.
The warnings can be restored by passing `-W#warning` to `ccomp`.

Now subsumed by the tests in abi/

Using a combination of fixed and randomly-generated function signatures.

This is complementary to 28f23580

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.

Follow-up to 35e2b11d.

Put the warning "pragmas are ignored inside functions" inside the Unnamed
category, so that it is displayed by default and cannot be disabled.

In function Asmexpand.next_arg_locations:

If 7 integer parameter passing registers have been used already,
and the next fixed arguments are Tlong then Tint, the Tlong argument
was correctly analyzed as being passed on the stack, but the Tint
argument was incorrectly analyzed as being passed in the 8th register.

However it produces new warnings that should be investigated later.

This is a follow-up to e81d015e.

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.

Follow-up to aba0e740

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}`.

fold_inv is in Type, hence can prove goals such as `{ x | P x }`.
Also, no extensionality property is needed.

fold_rec is now derived from fold_inv.

This is a follow-up to 2076a3bb.

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

Pragmas can occur either outside external declarations, at the top level
of a compilation unit, or within a compound statement, inside a function
definition.

The parse tree in cparse/C.mli cannot represent pragmas occuring within
a compound statement.

In this case, the elaborator used to silently move the pragma to top
level, just before the function definition where the pragma occurs.

It looks safer to just ignore pragmas occurring inside a function
definition, and emit a specific warning.

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`.

IEEE754_extra: clear unused context so that none of the context is
picked up by tactics and ends as extra parameters to theorems
int_round_odd_bits and int_round_odd_le

Floats: simplify uses of int_round_odd_bits and int_round_odd_le
accordingly.

Factor out the substitution of `$prefix` for `\$(PREFIX)`
using a shell function `expandprefix`.

To control where man pages are installed.

The default `/usr/local/share/man` is good for Linux but BSD prefers `/usr/local/man`.

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.

All the built-in types declared in $ARCH/CBuiltins.ml are now recognized
as type names initially.

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.

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.

To make sure it works if `gmake` is required.

Fixes: #381