aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* finish merging master branch (fixes problems in glpk colamd)David Monniaux2019-06-063-43/+0
|
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-063-5/+59
|\
| * 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-064-72/+584
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-061-0/+797
| | | | | | | | | | | | | | 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.
* | start to have whole path if-conversion?David Monniaux2019-06-041-1/+1
| |
* | rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-032-64/+3
| |
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-0321-150/+1552
|\ \ | | | | | | | | | mppa-if-conversion
| * | ARM: select is not supported at type TlongXavier Leroy2019-06-011-2/+3
| | |
| * | If-conversion optimizationXavier Leroy2019-05-314-72/+579
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-05-311-0/+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.
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
| | | | | | | | | | | | 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.
| * Support a "select" operation between two valuesXavier Leroy2019-05-202-0/+86
| | | | | | | | | | | | | | | | | | | | `Val.select ob v1 v2 ty` is a conditional operation that chooses between the values `v1` and `v2` depending on the comparison `ob : option bool`. If `ob` is `None`, `Vundef` is returned. If the selected value does not match type `ty`, `Vundef` is returned. This operation will be used to model a "select" (or "conditional move") operation at the CminorSel/RTL/LTL/Mach level.
| * Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+8
| | | | | | | | | | | | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
| * Change to AbsInt version string.Bernhard Schommer2019-05-102-2/+2
| | | | | | | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
| * Expand the responsefiles earlierBernhard Schommer2019-05-102-4/+4
| | | | | | | | | | | | | | | | | | * Move the expansion of response files to module Commandline, during the initialization of `Commandline.argv`. This way we're sure it's done exactly once. * Make `Commandline.argv` a `string array` instead of a `string array ref`. We no longer need to update it after initialization! * Improve reporting of errors during expansion of response files.
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-263-20/+21
| | | | | | | | | | | | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
| * lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-235-20/+22
| | | | | | | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
| * Replace nat_of_Z with Z.to_natXavier Leroy2019-04-235-17/+17
| | | | | | | | | | | | | | Use Z.to_nat theorems from the standard Coq library in preference to our theorems in lib/Coqlib.v. Simplify lib/Coqlib.v accordingly.
| * Print only debug info for printed functions.Bernhard Schommer2019-04-161-1/+2
| | | | | | | | | | | | | | | | | | | | | | Functions that are removed from the compilation unit, for example inline functions without extern, should not produce debug information. This commit reuses the mechanism used for variables in order to track additionally the printed functions. Therefore the printed variable versions are exchanged for a printed symbol version. Bug 26234
| * Typo in comment about Ijumptable in RTL.vAlix Trieu2019-04-151-1/+1
| |
| * Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
| | | | | | SEL_SWITH_INT -> SEL_SWITCH_INT
| * RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| | | | | | | | | | | | | | `external_call_mem_extends` returns a conjunction of 4 properties, but the destruct pattern was 5 level deep. (Reported by Jeremie Koenig in pull request #278.)
| * Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-2/+2
| | | | | | Preparation for Coq PR 9725 that may make `eauto` stronger.
* | itemize the proof (better for debugging)David Monniaux2019-04-051-10/+10
| |
* | preparing for the builtin connectorDavid Monniaux2019-04-051-3/+69
| |
* | removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-052-72/+6
| |
* | Oselectf, Oselectfs with conditionDavid Monniaux2019-04-051-8/+2
| |
* | selectl with conditionDavid Monniaux2019-04-051-4/+1
| |
* | more on selectDavid Monniaux2019-04-041-4/+1
| |
* | select_soundDavid Monniaux2019-04-041-1/+1
| |
* | ternary ops for float/doubleDavid Monniaux2019-04-031-2/+34
| |
* | problem in ValueAOpDavid Monniaux2019-04-031-1/+17
| |
* | begin implementing ternary builtinDavid Monniaux2019-04-031-4/+13
| |
* | selection of builtin.. progress...David Monniaux2019-04-031-13/+14
| |
* | some more on builtinsDavid Monniaux2019-04-032-3/+20
| |
* | attempts at generating builtins, startDavid Monniaux2019-04-031-3/+6
| |
* | ça recompile sur x86David Monniaux2019-03-228-3/+127
| |
* | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-223-8/+4
|\ \
| * | try to be portable across archsDavid Monniaux2019-03-213-8/+4
| | |
* | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-201-7/+6
|\| |
| * | XLeroy's suggested fix for shared float/int register file.David Monniaux2019-03-201-3/+3
| | |
| * | Revert "Better fix for register allocation?"David Monniaux2019-03-201-4/+3
| | | | | | | | | | | | This reverts commit 5ad25465f77c3009eaff7e9a124c254c1e9f33cd.
* | | Proof of div32/mod32/divf32/divf64 lemmasCyril SIX2019-03-201-3/+3
| | |
* | | la division flottante fonctionneDavid Monniaux2019-03-203-9/+12
| | |
* | | begin float divisionDavid Monniaux2019-03-201-3/+3
| | |
* | | Proving eval_divs_baseCyril SIX2019-03-202-2/+2
| | |
* | | added helper functions but strangeDavid Monniaux2019-03-194-89/+10
|/ / | | | | | | idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-6/+8
|\| | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * Make the checker happy (#272)Vincent Laporte2019-02-121-6/+8
| | | | | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
generated by cgit (git 2.34.1) at 2024-07-06 15:02:51 +0000