aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Adding measures graph generation in the MakefileCyril SIX2019-06-194-12/+26
|
* More .gitignore for a clean git statusCyril SIX2019-06-192-0/+26
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-06-191-0/+3
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Missing make.proto of lustrev4_lustrecCyril SIX2019-06-191-0/+3
| |
* | pretty print statisticsDavid Monniaux2019-06-191-36/+33
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2019-06-19431-2052/+189285
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * "Compilation time" --> "Scheduling pass time"Cyril SIX2019-06-191-1/+1
| |
| * Adding clean to test/monniaux/MakefileCyril SIX2019-06-191-0/+24
| |
| * Putting back lustrev4_lustrec_heater_controlCyril SIX2019-06-191-2/+2
| |
| * Removing lustrev4_lustrec_heater_control and ternary for now from benches.shCyril SIX2019-06-191-1/+3
| |
| * Makefile in test/monniaux that generates the compilation time graphsCyril SIX2019-06-194-48/+37
| |
| * Patch for PostpassSchedulingOracle measuresCyril SIX2019-06-191-0/+33
| |
| * graphique: Label correctionsCyril SIX2019-06-191-2/+2
| |
| * Verification time graph generation scriptCyril SIX2019-06-191-0/+66
| |
| * build_benches printing compile time in compile_times.txtCyril SIX2019-06-191-1/+4
| |
| * Adding Gc.major() before the start_timeCyril SIX2019-06-191-1/+1
| |
| * Instrumentation patch for AsmblockdepsCyril SIX2019-06-191-0/+20
| |
| * add arrow.h from LustreCDavid Monniaux2019-06-194-130/+35
| |
| * for RiscVDavid Monniaux2019-06-181-0/+8
| |
| * Reverting the unwanted time measurement from the other branchCyril SIX2019-06-181-14/+1
| |
| * [NOT TESTED] Compiles and should work ?Cyril SIX2019-06-181-11/+17
| |
| * [BROKEN] still broken, just fixing a logical detailCyril SIX2019-06-171-1/+1
| |
| * [BROKEN] Fixed the dependency oracle, does not compileCyril SIX2019-06-171-8/+42
| | | | | | | | I was removing too many dependencies
| * Merge branch 'mppa-work' into mppa-better-depsCyril SIX2019-06-176-8/+12
| |\
| | * Dans test/mppa : changer k1-mbr-gcc en k1-cos-gccCyril SIX2019-06-176-8/+12
| | |
| * | [NOT TESTED] ça compileCyril SIX2019-06-171-7/+7
| | |
| * | [BROKEN] Replaced the accesses lists by Maps, does not compileCyril SIX2019-06-141-8/+58
| |/
| * Towards supporting the CompCert tests (not finished)Cyril SIX2019-06-143-10/+16
| |
| * Removing the Admitted warning when running "make check-admitted"Cyril SIX2019-06-121-1/+1
| |
| * abstract_bb: few improvements while writing the paperSylvain Boulmé2019-06-086-251/+294
| |
| * Merge branch 'mppa-work' into mppa-abstractbb-devSylvain Boulmé2019-06-08606-11431/+204292
| |\
| | * for zlibDavid Monniaux2019-06-074-2/+34
| | |
| | * zlib-1.2.11David Monniaux2019-06-0729-0/+14142
| | |
| | * c'est pas non plus ça la lenteurDavid Monniaux2019-06-071-1/+7
| | |
| | * réseau de neuronesDavid Monniaux2019-06-075-0/+811
| | |
| | * add clockingDavid Monniaux2019-06-071-0/+12
| | |
| | * tiff exampleDavid Monniaux2019-06-074-38/+17
| | |
| | * libtiff, beginDavid Monniaux2019-06-0759-0/+42962
| | |
| | * compilationDavid Monniaux2019-06-062-0/+38
| | |
| | * added clockedDavid Monniaux2019-06-067-0/+1670
| | |
| | * timings for glpsolDavid Monniaux2019-06-063-0/+348
| | |
| | * GLPK 4.65David Monniaux2019-06-06281-0/+126536
| | |
| | * 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-065-9/+65
| | |\
| | | * 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
| | | |
generated by cgit (git 2.34.1) at 2024-07-11 19:38:10 +0000