Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | réseau de neurones | David Monniaux | 2019-06-07 | 5 | -0/+811 |
| | |||||
* | add clocking | David Monniaux | 2019-06-07 | 1 | -0/+12 |
| | |||||
* | tiff example | David Monniaux | 2019-06-07 | 4 | -38/+17 |
| | |||||
* | libtiff, begin | David Monniaux | 2019-06-07 | 59 | -0/+42962 |
| | |||||
* | compilation | David Monniaux | 2019-06-06 | 2 | -0/+38 |
| | |||||
* | added clocked | David Monniaux | 2019-06-06 | 7 | -0/+1670 |
| | |||||
* | timings for glpsol | David Monniaux | 2019-06-06 | 3 | -0/+348 |
| | |||||
* | GLPK 4.65 | David Monniaux | 2019-06-06 | 281 | -0/+126536 |
| | |||||
* | finish merging master branch (fixes problems in glpk colamd) | David Monniaux | 2019-06-06 | 3 | -43/+0 |
| | |||||
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work | David Monniaux | 2019-06-06 | 5 | -9/+65 |
|\ | |||||
| * | Added Pfmovite to list of known mnemonic names. | Bernhard Schommer | 2019-06-06 | 1 | -1/+1 |
| | | |||||
| * | Cminortyping: relax typechecking of function calls | Xavier Leroy | 2019-06-06 | 1 | -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 optimization | Xavier Leroy | 2019-06-06 | 10 | -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 Cminor | Xavier Leroy | 2019-06-06 | 2 | -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 languages | Xavier Leroy | 2019-06-06 | 1 | -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 Tlong | Xavier Leroy | 2019-06-06 | 2 | -2/+11 |
| | | |||||
| * | New additional check for void parameters. (#174) | Bernhard Schommer | 2019-06-03 | 1 | -3/+5 |
| | | | | | | | | There should only be one unnamed parameter of type void in the parameter list. | ||||
* | | timings | David Monniaux | 2019-06-06 | 1 | -1/+16 |
| | | |||||
* | | print clock info | David Monniaux | 2019-06-06 | 2 | -0/+27 |
| | | |||||
* | | compiles and links | David Monniaux | 2019-06-06 | 1 | -1/+9 |
| | | |||||
* | | for compiling cjpeg/djpeg | David Monniaux | 2019-06-06 | 2 | -308/+328 |
| | | |||||
* | | fix measures | David Monniaux | 2019-06-06 | 1 | -7/+7 |
| | | |||||
* | | some more benchmarks | David Monniaux | 2019-06-06 | 9 | -27/+60 |
| | | |||||
* | | attempt at -O1 | David Monniaux | 2019-06-06 | 1 | -1/+5 |
| | | |||||
* | | add version.h, prims.c | David Monniaux | 2019-06-06 | 3 | -1/+1160 |
| | | |||||
* | | Merge branch 'mppa-work' of ↵ | David Monniaux | 2019-06-05 | 1 | -1/+1 |
|\ \ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | | Fix for #134 Pjumptable not recognized | Cyril SIX | 2019-06-05 | 1 | -1/+1 |
| | | | |||||
* | | | disable large benchmarks that rely on heap saturation and other limits | David Monniaux | 2019-06-05 | 2 | -10/+14 |
|/ / | |||||
* | | fixed reservation table for cmove | David Monniaux | 2019-06-05 | 1 | -1/+5 |
| | | |||||
* | | move with immediates | David Monniaux | 2019-06-04 | 2 | -1/+31 |
| | | |||||
* | | osel imm | David Monniaux | 2019-06-04 | 8 | -23/+117 |
| | | |||||
* | | begin osel imm | David Monniaux | 2019-06-04 | 3 | -3/+57 |
| | | |||||
* | | added immediate cmove | David Monniaux | 2019-06-04 | 6 | -38/+80 |
| | | |||||
* | | shortcuts for cmove | David Monniaux | 2019-06-04 | 3 | -21/+41 |
| | | |||||
* | | shortcut cmove works | David Monniaux | 2019-06-04 | 2 | -89/+7 |
| | | |||||
* | | why doesn't it work? | David Monniaux | 2019-06-04 | 2 | -7/+265 |
| | | |||||
* | | little restructuring | David Monniaux | 2019-06-04 | 1 | -3/+4 |
| | | |||||
* | | keep the .s files | David Monniaux | 2019-06-04 | 1 | -0/+2 |
| | | |||||
* | | remove old "ternary" stuff | David Monniaux | 2019-06-04 | 5 | -47/+10 |
| | | |||||
* | | start to have whole path if-conversion? | David Monniaux | 2019-06-04 | 3 | -3/+18 |
| | | |||||
* | | Osel -> assembleur | David Monniaux | 2019-06-04 | 3 | -104/+112 |
| | | |||||
* | | Osel is output = 1st input | David Monniaux | 2019-06-04 | 1 | -0/+1 |
| | | |||||
* | | Osel operation (not yet compiled) | David Monniaux | 2019-06-04 | 3 | -31/+39 |
| | | |||||
* | | rm old select/selectl/selectf/selectfs | David Monniaux | 2019-06-03 | 14 | -914/+47 |
| | | |||||
* | | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-06-03 | 158 | -9521/+14486 |
|\ \ | | | | | | | | | | mppa-if-conversion | ||||
| * | | ARM: select is not supported at type Tlong | Xavier Leroy | 2019-06-01 | 3 | -4/+14 |
| | | | |||||
| * | | If-conversion optimization | Xavier Leroy | 2019-05-31 | 10 | -75/+746 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 Cminor | Xavier Leroy | 2019-05-31 | 2 | -1/+799 |
| | | | | | | | | | | | | | | | | | | | | | 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 languages | Xavier Leroy | 2019-05-31 | 1 | -0/+173 |
| |/ | | | | | | | | | If the source language is determinate, it can take several steps (not just one) before the "match_state" invariant is reinstated. | ||||
| * | Fix misspellings in messages, man pages, and comments | Xavier Leroy | 2019-05-31 | 21 | -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. |