aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* Change warning for pragmas inside functionsXavier Leroy2021-01-161-1/+1
| | | | | | | Follow-up to 35e2b11db. Put the warning "pragmas are ignored inside functions" inside the Unnamed category, so that it is displayed by default and cannot be disabled.
* PowerPC: wrong computation of the position of the first vararg argumentXavier Leroy2021-01-151-2/+3
| | | | | | | | | 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.
* Coq 8.13.0 is supportedXavier Leroy2021-01-141-3/+3
| | | | However it produces new warnings that should be investigated later.
* RISC-V: fix FP calling conventionsXavier Leroy2021-01-146-122/+176
| | | | | | | | | | | | | | | | | | | | | | | 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.
* Replace `omega` tactic with `lia`, continuedXavier Leroy2021-01-131-1/+1
| | | | Follow-up to aba0e740f
* Improve branch tunnelingXavier Leroy2021-01-132-60/+328
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
| | | | | | | | | | 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}`.
* Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | | | | | | 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.
* Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
|
* RISC-V: wrong fixup code generated for vararg calls with fixed FP argsXavier Leroy2021-01-103-12/+35
| | | | | | | | | 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
* Ignore and warn about pragmas inside functionsXavier Leroy2021-01-071-1/+4
| | | | | | | | | | | | | | | 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.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-29110-2695/+2694
| | | | | | | | | | | 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`.
* Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
| | | | | | | | | 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.
* Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-2830-638/+1841
|
* configure: simplify the final printing of the configurationXavier Leroy2020-12-281-9/+8
| | | | | Factor out the substitution of `$prefix` for `\$(PREFIX)` using a shell function `expandprefix`.
* configure: add -mandir option (#382)Daniel Dickman2020-12-281-1/+7
| | | | | To control where man pages are installed. The default `/usr/local/share/man` is good for Linux but BSD prefers `/usr/local/man`.
* AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)Xavier Leroy2020-12-261-1/+1
| | | | | | | | 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.
* AArch64: macOS portXavier Leroy2020-12-2618-220/+570
| | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
* C parser: handle other built-in types than __builtin_va_listXavier Leroy2020-12-261-1/+2
| | | | | All the built-in types declared in $ARCH/CBuiltins.ml are now recognized as type names initially.
* AArch64: clarify the printing of extending-register arithmetic operationsXavier Leroy2020-12-261-13/+13
| | | | | The extended register is now printed as an X register if the extension mode is UXTX, and as a W register otherwise.
* AArch64: wrong function alignmentXavier Leroy2020-12-261-1/+1
| | | | | 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.
* RISC-V: revised calling conventions for variadic functionsXavier Leroy2020-12-252-63/+105
| | | | | Fixed (non-variadic) arguments follow the standard calling conventions. It's only the variadic arguments that need special treatment.
* Changed cc_varargs to an option typeBernhard Schommer2020-12-2512-27/+36
| | | | | | 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.
* configure: use `$make` instead of `make`Xavier Leroy2020-12-251-1/+1
| | | | | | To make sure it works if `gmake` is required. Fixes: #381
* configure script revised and simplifiedXavier Leroy2020-12-241-83/+43
| | | | | | | | Start from reasonable defaults before updating them per-target. Print more details in the final configuration summary. Update the "manual" mode.
* configure: support Coq 8.12.2Xavier Leroy2020-12-241-2/+2
|
* Configure the correct archiver to build runtime/libcompcert.aXavier Leroy2020-12-242-2/+8
| | | | | | | | | - 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
* x86 32 bits: ABI non-conformance for functions returning structs/unionsXavier Leroy2020-12-111-1/+1
| | | | | | | | The wrong value was returned in EAX, instead of the address of the struct/union. Report and fix by Zhenguo Yin. Fixes: #377
* Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | | | | | 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.
* PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | Inlined built-in functions destroy GPR0
* ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | | | Pflid destroys IR14 Inlined built-in functions destroy IR14
* AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
* Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Updates for release 3.8v3.8Xavier Leroy2020-11-163-5/+10
|
* Do not use -warn-error when building from a release tarballXavier Leroy2020-11-141-2/+9
| | | | | Stopping on warnings is useful for development builds, but unhelpful for released software.
* Support Coq 8.12.1Xavier Leroy2020-11-142-3/+3
|
* Update READMEXavier Leroy2020-11-091-4/+4
|
* Update ChangesXavier Leroy2020-11-081-0/+48
|
* Added semantics for the PowerPC sel and mulh built-insBernhard Schommer2020-11-071-4/+44
| | | | | | | | 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
* Added missing printer for PowerPC 64 bit comparison.Bernhard Schommer2020-11-061-0/+8
| | | | | These comparisons are supported in the hybrid 64 bit mode. Bug 30035
* Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-063-0/+12
| | | | | The two built-in function map to the fmax and fmin instruction. Bug 30035
* Better "make clean"Xavier Leroy2020-11-011-1/+1
|
* Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-304-20/+42
| | | | | | | 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.
* Add `string_of_ident` conversionXavier Leroy2020-10-121-0/+110
| | | | | | This is the left inverse of `ident_to_string`. Closes: #372
* Remove -version-file optionXavier Leroy2020-10-121-19/+2
| | | | It is specific to AbsInt's commercial version of CompCert.
* Support Cygwin 64 bitsXavier Leroy2020-10-0517-118/+415
| | | | | | - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
* Test clightgen with -short-idents and -normalize optionsXavier Leroy2020-09-221-0/+6
| | | | Use different combination of options for different test files.
* Use exact arithmetic for printing positive numbersXavier Leroy2020-09-221-52/+56
| | | | | | And also for the computations in name_temporary. Overflowing OCaml's integer types is unlikely in actual use but happened in the past owing to another mistake (see issue #370).
* Fix computation of next temporary in -canonical-idents modeXavier Leroy2020-09-221-1/+12
| | | | | | | Variables were confused for temporaries, causing the temporaries introduced by this pass to be very big integers. Fixes: #370
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-2111-67/+82
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
generated by cgit (git 2.34.1) at 2024-06-29 23:50:43 +0000