Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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. | ||||
| | * | 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 |
| | | |