GitLab

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

Start from reasonable defaults before updating them per-target.

Print more details in the final configuration summary.

Update the "manual" mode.

- Use `${toolprefix}ar` instead of `ar` so as to match the choice
  of C compiler (as proposed by Michael Soegtrop in PR #380)

- Use the Diab archiver `dar` if configured for powerpc-eabi-diab

Closes: #380

The wrong value was returned in EAX, instead of the address of the struct/union.

Report and fix by Zhenguo Yin.

Fixes: #377

Outside of -interp mode, -main has no (known) effect but could be
confused for a linker option that sets the program's entrypoint, say.
It's safer to reject the option.

Inlined built-in functions destroy GPR0

Pflid destroys IR14
Inlined built-in functions destroy IR14

Pfmovimms, Pfmovimmd destroy X16
Pbtbl preserves X17
Inlined built-in functions destroy X16 and X30

Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat
PowerPC operations.

The pseudoinstructions were used to implement these operations,
as follows:

Pfcfi  : Ofloatofint   i.e. the conversion signed int32 -> float64
Pfcfiu : Ofloatofintu  i.e. the conversion unsigned int32 -> float64
Pfctiu : Ointuoffloat  i.e. the conversion float64 -> unsigned int32

These pseudoinstructions were expanded (in Asmexpand.ml) in terms of

Pfcfid  : signed int64 -> float64
Pfctidz : float64 -> signed int64

and int32/int64 conversions.

This commit performs this expansion during instruction selection
(SelectOp.vp):

floatofint(n)  becomes floatoflong(longofint(n))
floatofintu(n) becomes floatoflong(longuofint(n))
intuoffloat(n) becomes cast32unsigned(longoffloat(n))

Then there is no need for the 3 removed operations and the 3 removed
pseudoinstructions.

More importantly, the correctness of these expansions is now proved as
part of instruction selection, using the corresponding results from
Floats.v.

Stopping on warnings is useful for development builds, but unhelpful
for released software.

The semantics of the various selection functions are defined analogously
to the ones from the type generic sel function. The semantics for the
various high word multiplication functions is defined using the Integer
functions.
Bug 30035

These comparisons are supported in the hybrid 64 bit mode.
Bug 30035

The two built-in function map to the fmax and fmin instruction.
Bug 30035

When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function.

This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option.

The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.