aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | more inliningDavid Monniaux2020-03-151-0/+2
| | | |
* | | | CSE3 alias analysisDavid Monniaux2020-03-141-2/+4
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-111-3/+3
|\| | |
| * | | Fixing buildCyril SIX2020-03-101-1/+1
| | | |
| * | | [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-091-2/+2
| | | | | | | | | | | | | | | | To control the threshold for duplication
* | | | -fcse3 command line optionDavid Monniaux2020-03-101-1/+3
|/ / /
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-141-0/+3
|\ \ \
| * | | Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-121-0/+3
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-1/+6
|\| | |
| * | | Added flag to desactivate condition inversionCyril SIX2020-02-031-0/+3
| | | |
| * | | Tail duplication optimization defaulting to offCyril SIX2020-01-271-1/+0
| | | |
| * | | Added a flag to desactivate tail duplicationCyril SIX2020-01-271-1/+4
| | | |
* | | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-2/+6
|\ \ \ \ | |/ / / |/| | |
| * | | connected (just a silly problem)David Monniaux2020-01-281-2/+5
| | |/ | |/|
* | | Added description for forward movesCyril SIX2020-01-171-0/+1
| | |
* | | connect forward-moves to compilerDavid Monniaux2020-01-081-0/+1
| | |
* | | -fall-loads-nontrapDavid Monniaux2019-09-091-0/+1
| | |
* | | helpers broke compilationDavid Monniaux2019-07-191-4/+0
| | |
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-3/+7
|\| | | | | | | | | | | mppa-work-upstream-merge
| * | -O0 now implies -fno-inliningMichael Schmidt2019-07-091-1/+1
| | |
| * | Update documentation of -ObranchlessXavier Leroy2019-07-051-1/+1
| | | | | | | | | | | | Updated man page + better usage message.
| * | Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-051-3/+3
| | | | | | | | | | | | | | | Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches).
| * | If-conversion optimizationXavier Leroy2019-06-061-2/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | (#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-031-5/+17
|\ \ \ | | | | | | | | | | | | mppa-if-conversion
| * | | If-conversion optimizationXavier Leroy2019-05-311-2/+8
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
| * | Check for alignment of command-line switches.Bernhard Schommer2019-05-101-3/+7
| | | | | | | | | | | | | | | | | | Add a check for alignment on command-line switches `-falign-*`. The check is similar to the one for the alignment attribute and ensures that only powers of two can be specified.
* | | option -faddx (off by default until questions cleared)David Monniaux2019-05-111-1/+2
| |/ |/|
* | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workDavid Monniaux2019-05-031-0/+1
|\ \
| * | -fcoalesce-memDavid Monniaux2019-05-031-0/+1
| | |
* | | Renaming "dumb" scheduling into "greedy"Cyril SIX2019-05-031-1/+1
|/ /
* | Merge branch 'mppa-xsaddr' into mppa-workDavid Monniaux2019-05-021-0/+3
|\ \
| * | command line options (still incomplete)David Monniaux2019-05-021-0/+3
| | |
* | | Setting fpostpass= optionCyril SIX2019-04-301-6/+8
| | |
* | | The scheduler selection works, but the argument is not optional yet ↵Cyril SIX2019-04-291-2/+5
|/ / | | | | | | (-fpostpass nameofscheduler)
* | -fpostpass-ilpDavid Monniaux2019-03-121-1/+0
| |
* | Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-121-0/+1
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * | Added cascaded_scheduler but the flag does not workCyril SIX2019-03-121-2/+3
| | |
| * | Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-121-0/+2
| | |
* | | -fpostpass-ilpDavid Monniaux2019-03-121-0/+2
|/ /
* / -O0 will not perform postpass schedulingCyril SIX2019-01-181-1/+3
|/
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-1/+1
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* Added error summary in case of fatal error.Bernhard Schommer2018-02-091-1/+1
|
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-26/+20
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Share code for common options.Bernhard Schommer2018-01-291-61/+16
| | | | | | In order to avoid more divergence between the command line options of clightgen and ccomp the code for the common options, the language support options, the version string and the general options.
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-111-22/+1
| | | | | The initialization of Machine.config, as well as the calls to various initialization functions for the C front-end, are now performed by the new `Frontend.init` function. This avoids code duplication in driver/Driver.ml and exportclight/Clightgen.ml.
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-051-45/+3
|
* Added toolchain specific option for dcc. (#47)Bernhard Schommer2018-01-051-1/+16
| | | | | | CompCert now accepts the target configuration option of the diab data compiler and passes it on to the preprocessor, assembler and linker. Bug 20521
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-041-1/+3
| | | | | This time with the correct place for setting the destination files. Bug 20521