- 23 Feb, 2021 1 commit
-
-
Xavier Leroy authored
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.
-
- 21 Jan, 2021 3 commits
-
-
Xavier Leroy authored
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.
-
Xavier Leroy authored
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`.
-
Xavier Leroy authored
The extraction mechanism wants to extract them (because they are in Type, probably). The current opaque definition causes a warning at extraction-time.
-
- 18 Jan, 2021 4 commits
-
-
Xavier Leroy authored
The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
-
Xavier Leroy authored
The standard includes print irrelevant warnings using `#warning`. The warnings can be restored by passing `-W#warning` to `ccomp`.
-
Xavier Leroy authored
Now subsumed by the tests in abi/
-
Xavier Leroy authored
Using a combination of fixed and randomly-generated function signatures.
-
- 16 Jan, 2021 2 commits
-
-
Xavier Leroy authored
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.
-
Xavier Leroy authored
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.
-
- 15 Jan, 2021 1 commit
-
-
Xavier Leroy authored
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.
-
- 14 Jan, 2021 2 commits
-
-
Xavier Leroy authored
However it produces new warnings that should be investigated later.
-
Xavier Leroy authored
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.
-
- 13 Jan, 2021 5 commits
-
-
Xavier Leroy authored
Follow-up to aba0e740
-
Xavier Leroy authored
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.
-
Xavier Leroy authored
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}`.
-
Xavier Leroy authored
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.
-
Xavier Leroy authored
-
- 10 Jan, 2021 1 commit
-
-
Xavier Leroy authored
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
-
- 07 Jan, 2021 1 commit
-
-
Xavier Leroy authored
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.
-
- 29 Dec, 2020 2 commits
-
-
Xavier Leroy authored
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`.
-
Xavier Leroy authored
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.
-
- 28 Dec, 2020 3 commits
-
-
Guillaume Melquiond authored
-
Xavier Leroy authored
Factor out the substitution of `$prefix` for `\$(PREFIX)` using a shell function `expandprefix`.
-
Daniel Dickman authored
To control where man pages are installed. The default `/usr/local/share/man` is good for Linux but BSD prefers `/usr/local/man`.
-
- 26 Dec, 2020 5 commits
-
-
Xavier Leroy authored
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.
-
Xavier Leroy authored
This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
-
Xavier Leroy authored
All the built-in types declared in $ARCH/CBuiltins.ml are now recognized as type names initially.
-
Xavier Leroy authored
The extended register is now printed as an X register if the extension mode is UXTX, and as a W register otherwise.
-
Xavier Leroy authored
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.
-
- 25 Dec, 2020 3 commits
-
-
Xavier Leroy authored
Fixed (non-variadic) arguments follow the standard calling conventions. It's only the variadic arguments that need special treatment.
-
Bernhard Schommer authored
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.
-
Xavier Leroy authored
To make sure it works if `gmake` is required. Fixes: #381
-
- 24 Dec, 2020 3 commits
-
-
Xavier Leroy authored
Start from reasonable defaults before updating them per-target. Print more details in the final configuration summary. Update the "manual" mode.
-
Xavier Leroy authored
-
Xavier Leroy authored
- 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
-
- 11 Dec, 2020 1 commit
-
-
Xavier Leroy authored
The wrong value was returned in EAX, instead of the address of the struct/union. Report and fix by Zhenguo Yin. Fixes: #377
-
- 06 Dec, 2020 3 commits
-
-
Xavier Leroy authored
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.
-
Xavier Leroy authored
Inlined built-in functions destroy GPR0
-
Xavier Leroy authored
Pflid destroys IR14 Inlined built-in functions destroy IR14
-