aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-078-23/+22
| | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* Simplify invocation of Emacs + Proof GeneralXavier Leroy2019-08-071-17/+3
| | | | PG now uses the _Coqproject file and finds relevant paths there.
* Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
| | | | | It supports a branch-free implementation of floatofintu. Not used yet in any of the ports.
* x86_64: branchless implementation of floatofintu and intuoffloatXavier Leroy2019-07-172-14/+29
| | | | | | | The implementation uses float <-> signed 64-bit integer conversion instructions, and is both efficient and branchless. Based on a suggestion by Rémi Hutin.
* When testing builtin functions, prevent constant propagationXavier Leroy2019-07-174-28/+31
| | | | | | | | | | Now that some builtin functions have known semantics, constant propagation can happen in this test. This defeats the purpose, which is to check that the correct processor instructions are generated. To prevent this constant propagation, we move the initialized variables to global scope. Since they are not "const", their values are not known to the optimizer.
* Make __builtin_sel available from C source codeXavier Leroy2019-07-177-32/+195
| | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
* Improve CSE for known built-in functionsXavier Leroy2019-07-172-7/+14
| | | | Known built-in functions are guaranteed not to change memory.
* Perform constant propagation for known built-in functionsXavier Leroy2019-07-174-16/+168
| | | | | | | When an external function is a known built-in function and it is applied to compile-time integer or FP constants, we can use the known semantics of the builtin to compute the result at compile-time.
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-1720-187/+1154
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
* Remove the cparser/Builtins moduleXavier Leroy2019-07-1719-104/+82
| | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-176-3/+76
| | | | | | | | We just lift the corresponding functions from Flocq and add the computation of NaN payloads. NaN payloads for FMA are described in the ARM and RISC-V specifications, and were determined experimentally for x86 and for Power.
* Add FMA (fused multiply-add)Xavier Leroy2019-07-171-0/+121
| | | | | Cherry-pick of the following commit on upstream Flocq: https://gitlab.inria.fr/flocq/flocq/commit/28cc6ee3a278878f3df002aab64a6b93e9412d34
* Fix tracing options for clightgen.Bernhard Schommer2019-07-151-10/+23
| | | | | | | | The clightgen tracing options did not result in printing of the intermediate files, but were ignored. Added also two new options, `-dprepro` to print the preprocessed file and `-dall` to dump all intermediate files.
* Revised specification of NaN payload behaviorXavier Leroy2019-07-126-193/+209
| | | | | | | | | | | | | | When an FP arithmetic instruction produces a NaN result, the payload of this NaN depends on the architecture. Before, the payload behavior was specified by 3 architecture-dependent parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32` and `Archi.fpu_results_default_qNaN`. This was adequate for two-argument operations, but doesn't extend to FMA. In preparation for FMA support, this commit generalizes the `Archi.choose` functions from two arguments to any number of arguments. In passing, `Archi.fpu_results_default_qNaN` is no longer needed.
* More precise description of '-O0' and 'non-linear-cond-expr'Michael Schmidt2019-07-101-1/+2
|
* Change condition for warning of conditional exprBernhard Schommer2019-07-101-1/+1
| | | | | | The warning should only be active if the optimization is active, so the check is only performed when the warning is active and additionally the command line flag -Obranchless is specified.
* -O0 now implies -fno-inliningMichael Schmidt2019-07-091-1/+1
|
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-089-12/+11
| | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
* Make configure resistant to Windows EOL and paths (#305)MSoegtropIMC2019-07-081-1/+1
| | | | | | | Commit 1df887f breaks compilation on some Windows environments, those where the output of `menhir --suggest-menhirLib` contains `\r\n` end-of-lines or backslashes in paths. The fix is to filter the output. Closes: #304 Changes in configure broke Windows build
* Fix compatibility with Coq 8.10 (#303)Jacques-Henri Jourdan2019-07-063-9/+10
| | | | | | The generation of some fresh names changes in Coq 8.10 (https://github.com/coq/coq/pull/9160). The `Hint Mode` declaration that does not specify a hint database now triggers a warning. Specify the intended database and fix the "auto" tactics accordingly.
* Update synonymous list for -O0, add new named warning classMichael Schmidt2019-07-051-1/+6
|
* Update documentation of -ObranchlessXavier Leroy2019-07-052-7/+9
| | | | Updated man page + better usage message.
* Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-053-7/+7
| | | | | Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches).
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-0534-3583/+3163
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
* Avoid relying on `Export` bug (#301)Maxime Dénès2019-07-041-1/+2
| | | | The previous code was unintentionally relying on a strange behavior of `Export` (see https://github.com/coq/coq/issues/10480) that will be removed.
* Deref is not safe.Bernhard Schommer2019-07-041-1/+1
|
* Added new diagnostic for non-linear conditionalsBernhard Schommer2019-07-046-1/+179
| | | | | | | | | | | | | | The new diagnostics is triggered if a conditional is used that may not be transformed into linear code by the later by the if conversion. The new diagnostic is emitted if a conditional may contain an unsafe expression or is contained within another conditional, logical and or logical or expression. An expression is unsafe if it contains a call, changes memory or if its evaluation leads to undefined behavior, for example division and modulo. Also fixes a small typo in a comment in Cutil.
* Added helper function for array types.Bernhard Schommer2019-07-042-0/+7
| | | | | The function determines whether the given type is an array type or not.
* Added statement traversal functions.Bernhard Schommer2019-07-041-107/+90
| | | | | | Refactored the checks functions by using higher order traversal functions for statements. Also introduce helper functions for the traversal of initializers.
* Change the expected types for arguments to __builtin_annot, and extended asmXavier Leroy2019-06-191-5/+25
| | | | | | | | | | | | | | | Currently, the arguments to __builtin_annot, __builtin_ais_annot, __builtin_debug, and extended asm statements are treated like arguments to an unprototyped or vararg function call. In particular, arguments of type "float" are converted to "double", generating useless code. To avoid this extra, useless conversion, this commit changes the types expected for the arguments to these built-ins and to extended asm statements. Now they are the types of the arguments themselves, after performing the usual unary conversions (e.g. char -> int), but without the problematic float -> double conversion. This ensures that no code is generated to change the representation of the arguments.
* Extended asm: print register names according to their typesXavier Leroy2019-06-176-19/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open.
* Updated man page.Bernhard Schommer2019-06-171-0/+10
|
* Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-177-6/+128
| | | | | A conditional move whose condition is statically known becomes a regular move. Otherwise, the condition can sometimes be simplified by strength reduction.
* Added Pfmovite to list of known mnemonic names.Bernhard Schommer2019-06-061-1/+1
|
* Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| | | | | | | Sometimes the result of a void function is assigned to a variable. This can occur with C conditional expressions ?: at type void, e.g. the "assert" macro of MacOS. A similar relaxation was already there in RTLtyping.
* If-conversion optimizationXavier Leroy2019-06-0610-75/+751
| | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
* Type inference and type checking for CminorXavier Leroy2019-06-062-1/+798
| | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
* Additional simulation diagrams for determinate source languagesXavier Leroy2019-06-061-0/+173
| | | | | If the source language is determinate, it can take several steps (not just one) before the "match_state" invariant is reinstated.
* ARM: select is not supported at type TlongXavier Leroy2019-06-062-2/+11
|
* New additional check for void parameters. (#174)Bernhard Schommer2019-06-031-3/+5
| | | | There should only be one unnamed parameter of type void in the parameter list.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-3121-31/+31
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-289-7/+101
| | | | | | The FP select for PowerPC stores both addresses in two subsequent stack slots and loads them using an offset created from the result of the comparison.
* PowerPC: add SelectOp.select functionXavier Leroy2019-05-262-0/+31
| | | | | This function and its proof should have been part of commit 43e7b67. They are already there for the other ports.
* ARM: Fix expansion of FP conditional moveXavier Leroy2019-05-261-2/+2
| | | | | The "vmov" instruction (Advanced SIMD) cannot be conditional. The "vmov.f64" instruction (VFPv2) can be conditional.
* Coq 8.9.1 supportXavier Leroy2019-05-211-3/+3
| | | | It works fine with the current sources.
* Csyntax.v: Fix a typo in a documentation comment (#292)Bart Jacobs2019-05-211-1/+1
|
* Add a check for the args of unprototyped calls.Bernhard Schommer2019-05-201-3/+8
| | | | | | The arguments that are passed to an unprototyped function must also be checked to be valid types passed to a function, i.e. they must be complete types after argument conversion.
* Provide a default "select" operation for the RiscV portXavier Leroy2019-05-202-0/+20
| | | | | No `Osel` operation for this port, so `SelectOp.select` always returns None.
* Implement a `Osel` operation for ARMXavier Leroy2019-05-2012-7/+115
| | | | | The operation comples down to conditional moves. Both integer and floating-point conditional moves are supported.
* Implement a `Osel` operation for x86Xavier Leroy2019-05-2011-38/+298
| | | | The operation compiles down to conditional moves.
generated by cgit (git 2.34.1) at 2024-06-29 10:52:55 +0000