aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-124-15/+48
|\
| * -fbranch-probabilitiesDavid Monniaux2020-04-081-1/+2
| |
| * reloading and exploiting seems to workDavid Monniaux2020-04-084-13/+28
| |
| * fixed a bug in support libraries; reload profiling infoDavid Monniaux2020-04-082-1/+1
| |
| * installed Profiling (not finished)David Monniaux2020-04-081-12/+21
| |
| * begin installing profilingDavid Monniaux2020-04-083-1/+9
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-04-012-7/+6
|\|
| * -fduplicate -1 really desactivates the pass in Coq nowCyril SIX2020-04-012-7/+6
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-172-2/+6
|\|
| * Desactivating branch predictions by defaultCyril SIX2020-03-172-2/+6
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-152-0/+3
|\|
| * by default do not inline muchDavid Monniaux2020-03-151-1/+1
| |
| * more inliningDavid Monniaux2020-03-152-0/+3
| |
* | CSE3 alias analysisDavid Monniaux2020-03-143-4/+10
| |
* | typing and store stuffDavid Monniaux2020-03-121-3/+3
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-113-10/+10
|\|
| * Fixing buildCyril SIX2020-03-101-1/+1
| |
| * [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-093-9/+9
| | | | | | | | To control the threshold for duplication
* | -fcse3 command line optionDavid Monniaux2020-03-101-1/+3
| |
* | starts compiling but still fakeDavid Monniaux2020-03-103-9/+21
| |
* | CSE3 generate lists of killableDavid Monniaux2020-03-051-1/+1
| |
* | streamlined lattice codeDavid Monniaux2020-03-051-0/+1
|/
* Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-036-37/+138
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-142-0/+4
| |\
| | * Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-122-0/+4
| | |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-064-6/+18
| |\|
| | * Added flag to desactivate condition inversionCyril SIX2020-02-032-0/+4
| | |
| | * Tail duplication optimization defaulting to offCyril SIX2020-01-272-2/+1
| | |
| | * Added a flag to desactivate tail duplicationCyril SIX2020-01-274-6/+15
| | |
| * | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-284-11/+28
| |\ \ | | |/ | |/|
| * | Added description for forward movesCyril SIX2020-01-171-0/+1
| | |
| * | connect forward-moves to compilerDavid Monniaux2020-01-084-6/+20
| | |
| * | finish mergeDavid Monniaux2019-12-021-31/+19
| | |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-5/+25
| |\ \
| | * \ [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-1/+2
| | |\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| | * \ \ Merge branch 'mppa-work' into mppa-duplicate-rtlCyril SIX2019-10-021-1/+1
| | |\ \ \
| | * | | | Stubs for Duplicate passCyril SIX2019-09-031-28/+36
| | | | | |
| * | | | | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-202-1/+2
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| | * | | | | fix compilingDavid Monniaux2019-09-201-0/+4
| | | | | | |
| | * | | | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-202-1/+2
| | |\ \ \ \ \ | | | |_|/ / / | | |/| | / / | | | | |/ / | | | |/| | mppa-work-upstream-merge
| * | | | | to v3.6David Monniaux2019-09-201-1/+5
| | | | | |
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-201-1/+1
| |\| | | |
| | * | | | Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-181-1/+1
| | | |/ / | | |/| |
| * / | | -fall-loads-nontrapDavid Monniaux2019-09-094-2/+16
| |/ / /
| * | | helpers broke compilationDavid Monniaux2019-07-191-4/+0
| | | |
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-194-7/+11
| |\ \ \ | | | | | | | | | | | | | | | mppa-work-upstream-merge
| * | | | (#142) Desactivating scheduling when using -O1 optimizationCyril SIX2019-07-171-1/+3
| | | | |
| * | | | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-037-25/+62
| |\ \ \ \ | | | | | | | | | | | | | | | | | | mppa-if-conversion
| | * | | | If-conversion optimizationXavier Leroy2019-05-312-2/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | option -faddx (off by default until questions cleared)David Monniaux2019-05-113-5/+10
| | | | | |