Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Graph in 1/cycles | Cyril SIX | 2019-06-19 | 2 | -7/+10 |
| | |||||
* | Adding measures graph generation in the Makefile | Cyril SIX | 2019-06-19 | 4 | -12/+26 |
| | |||||
* | More .gitignore for a clean git status | Cyril SIX | 2019-06-19 | 2 | -0/+26 |
| | |||||
* | Merge branch 'mppa-work' of ↵ | David Monniaux | 2019-06-19 | 1 | -0/+3 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | Missing make.proto of lustrev4_lustrec | Cyril SIX | 2019-06-19 | 1 | -0/+3 |
| | | |||||
* | | pretty print statistics | David Monniaux | 2019-06-19 | 1 | -36/+33 |
| | | |||||
* | | Merge branch 'mppa-work' of ↵ | David Monniaux | 2019-06-19 | 431 | -2052/+189285 |
|\| | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | "Compilation time" --> "Scheduling pass time" | Cyril SIX | 2019-06-19 | 1 | -1/+1 |
| | | |||||
| * | Adding clean to test/monniaux/Makefile | Cyril SIX | 2019-06-19 | 1 | -0/+24 |
| | | |||||
| * | Putting back lustrev4_lustrec_heater_control | Cyril SIX | 2019-06-19 | 1 | -2/+2 |
| | | |||||
| * | Removing lustrev4_lustrec_heater_control and ternary for now from benches.sh | Cyril SIX | 2019-06-19 | 1 | -1/+3 |
| | | |||||
| * | Makefile in test/monniaux that generates the compilation time graphs | Cyril SIX | 2019-06-19 | 4 | -48/+37 |
| | | |||||
| * | Patch for PostpassSchedulingOracle measures | Cyril SIX | 2019-06-19 | 1 | -0/+33 |
| | | |||||
| * | graphique: Label corrections | Cyril SIX | 2019-06-19 | 1 | -2/+2 |
| | | |||||
| * | Verification time graph generation script | Cyril SIX | 2019-06-19 | 1 | -0/+66 |
| | | |||||
| * | build_benches printing compile time in compile_times.txt | Cyril SIX | 2019-06-19 | 1 | -1/+4 |
| | | |||||
| * | Adding Gc.major() before the start_time | Cyril SIX | 2019-06-19 | 1 | -1/+1 |
| | | |||||
| * | Instrumentation patch for Asmblockdeps | Cyril SIX | 2019-06-19 | 1 | -0/+20 |
| | | |||||
| * | add arrow.h from LustreC | David Monniaux | 2019-06-19 | 4 | -130/+35 |
| | | |||||
| * | for RiscV | David Monniaux | 2019-06-18 | 1 | -0/+8 |
| | | |||||
| * | Reverting the unwanted time measurement from the other branch | Cyril SIX | 2019-06-18 | 1 | -14/+1 |
| | | |||||
| * | [NOT TESTED] Compiles and should work ? | Cyril SIX | 2019-06-18 | 1 | -11/+17 |
| | | |||||
| * | [BROKEN] still broken, just fixing a logical detail | Cyril SIX | 2019-06-17 | 1 | -1/+1 |
| | | |||||
| * | [BROKEN] Fixed the dependency oracle, does not compile | Cyril SIX | 2019-06-17 | 1 | -8/+42 |
| | | | | | | | | I was removing too many dependencies | ||||
| * | Merge branch 'mppa-work' into mppa-better-deps | Cyril SIX | 2019-06-17 | 6 | -8/+12 |
| |\ | |||||
| | * | Dans test/mppa : changer k1-mbr-gcc en k1-cos-gcc | Cyril SIX | 2019-06-17 | 6 | -8/+12 |
| | | | |||||
| * | | [NOT TESTED] ça compile | Cyril SIX | 2019-06-17 | 1 | -7/+7 |
| | | | |||||
| * | | [BROKEN] Replaced the accesses lists by Maps, does not compile | Cyril SIX | 2019-06-14 | 1 | -8/+58 |
| |/ | |||||
| * | Towards supporting the CompCert tests (not finished) | Cyril SIX | 2019-06-14 | 3 | -10/+16 |
| | | |||||
| * | Removing the Admitted warning when running "make check-admitted" | Cyril SIX | 2019-06-12 | 1 | -1/+1 |
| | | |||||
| * | abstract_bb: few improvements while writing the paper | Sylvain Boulmé | 2019-06-08 | 6 | -251/+294 |
| | | |||||
| * | Merge branch 'mppa-work' into mppa-abstractbb-dev | Sylvain Boulmé | 2019-06-08 | 606 | -11431/+204292 |
| |\ | |||||
| | * | for zlib | David Monniaux | 2019-06-07 | 4 | -2/+34 |
| | | | |||||
| | * | zlib-1.2.11 | David Monniaux | 2019-06-07 | 29 | -0/+14142 |
| | | | |||||
| | * | c'est pas non plus ça la lenteur | David Monniaux | 2019-06-07 | 1 | -1/+7 |
| | | | |||||
| | * | 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. |