aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* 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.
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-312-3/+3
| | | | | | | | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
| * Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-102-0/+3
| | | | | | | | | | | | | | | | | | | | 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.
| * Change to AbsInt version string.Bernhard Schommer2019-05-101-2/+2
| | | | | | | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
| * Expand the responsefiles earlierBernhard Schommer2019-05-103-13/+13
| | | | | | | | | | | | | | | | | | * Move the expansion of response files to module Commandline, during the initialization of `Commandline.argv`. This way we're sure it's done exactly once. * Make `Commandline.argv` a `string array` instead of a `string array ref`. We no longer need to update it after initialization! * Improve reporting of errors during expansion of response files.
| * 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.
| * Define macros with CompCert's version number (#284)Xavier Leroy2019-03-271-2/+24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As suggested in #282, it can be useful to #ifdef code depending on specific versions of CompCert. Assuming a version number of the form MM.mm , the following macros are predefined: __COMPCERT_MAJOR__=MM (the major version number) __COMPCERT_MINOR__=mm (the minor version number) __COMPCERT_VERSION__=MMmm (two decimal digits for the minor, e.g. 305 for version 3.5) We also define __COMPCERT_BUILDNR__ if the build number is not empty in file ./VERSION. Closes: #282
* | option -faddx (off by default until questions cleared)David Monniaux2019-05-113-5/+10
| |
* | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workDavid Monniaux2019-05-033-0/+5
|\ \
| * | -fcoalesce-memDavid Monniaux2019-05-033-0/+5
| | |
* | | Renaming "dumb" scheduling into "greedy"Cyril SIX2019-05-031-1/+1
|/ /
* | Merge branch 'mppa-xsaddr' into mppa-workDavid Monniaux2019-05-023-0/+16
|\ \
| * | command line options (still incomplete)David Monniaux2019-05-023-0/+16
| | |
* | | Setting fpostpass= optionCyril SIX2019-04-301-6/+8
| | |
* | | The scheduler selection works, but the argument is not optional yet ↵Cyril SIX2019-04-292-3/+6
|/ / | | | | | | (-fpostpass nameofscheduler)
* | -fpostpass-ilpDavid Monniaux2019-03-122-4/+0
| |
* | Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-122-0/+4
|\ \ | | | | | | | | | 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-123-0/+6
| | |
* | | -fpostpass-ilpDavid Monniaux2019-03-122-0/+3
|/ /
* | Added long double = double by default on Kalray architectureCyril SIX2019-03-011-1/+1
| |
* | -O0 will not perform postpass schedulingCyril SIX2019-01-183-1/+7
| |
* | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-271-1/+1
| |
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-1/+1
| |
* | Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-261-322/+0
| |
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-219-93/+202
|\| | | | | | | | | Conflicts: .gitignore
| * Fix passing of -u to linker.Bernhard Schommer2018-08-211-1/+1
| | | | | | | | | | | | Instead of just passing -u to the linker also pass the value of the option to the linker. Bug 24316
| * Add sizeof_reg and new Machine configurations (#129)Bernhard Schommer2018-08-201-4/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | Since the size of integer registers is not identical to the size of pointers for the ppc64 and e5500 model the check for register pairs in ExtendedAsm does not work correctly. In order to avoid this a new field sizeof_intreg is introduced in the Machine configuration which describes the size of integer registers. New configurations for the ppc64 and e5500 model are added and used. Bug 24273
| * Various improvements in the wording of diagnostics.Michael Schmidt2018-08-026-12/+12
| | | | | | | | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
| * Typo in -iquote preprocessing option (#239)Frédéric Besson2018-06-201-1/+1
| | | | | | The `-iquote` option was passed to the GNU preprocessor as `-iquore`
| * Simplify module Complements and add separate compilation (#121)Xavier Leroy2018-05-291-74/+172
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Simplify the theorems about preservation of specifications (section 2) There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand. Plus, the "liveness" and "safety" terminology wasn't very good. Replaced by two theorems: - transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors; - transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces. Added named definitions for properties of interest. Added more explanations. * Added theorems that talk about separate compilation (section 3) These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together.
| * Define C11 conditional feature macros (#77)Bernhard Schommer2018-04-061-1/+10
| | | | | | | | | | | | | | | | These macros can be defined to indicate that variable length arrays, the _Complex type, atomics and threads are not supported. Since the _Complex type is not supported, we also need to undefine __STDC_IEC_559_COMPLEX__ Bug 23408
* | Rajout d'un return_address_offset. Besoin de changer forward_simu de mach ↵Cyril SIX2018-09-061-1/+1
| | | | | | | | machblock
* | Machblock: some renaming and proof simplificationsCyril SIX2018-09-061-15/+15
| |
* | Machblock: adaptation to the generalized ForwardSimulationBlockSylvain Boulmé2018-09-061-8/+103
| |
* | Generalization of ForwardSimulationBlockSylvain Boulmé2018-09-061-33/+24
| |
* | Machblock: Mach language with basic blocksCyril SIX2018-09-061-0/+236
| |
* | Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-042-1/+2
|/
* Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-162-49/+0
|
* Move struct passing/return style to Machine.Bernhard Schommer2018-02-161-1/+5
| | | | | | Since the used configuration for passing and returning values struct values is pretty much static it can be hardwired into the machine settings.
* 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-088-70/+64
| | | | | | | | | | | | | | | | | * 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-292-61/+105
| | | | | | 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-113-22/+29
| | | | | 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-042-13/+5
| | | | | This time with the correct place for setting the destination files. Bug 20521
* Remove duplicated code. Bug 20521Bernhard Schommer2018-01-041-46/+26
|
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-033-18/+16
| | | | | | | | | Replaced calls to Filename.temp_file by own version Driveraux.tmp_file. The Driveraux.tmp_file function takes care that the temporary files are removed at exit. Consequently there is no need to explicitly remove temp files in Driver.
generated by cgit (git 2.34.1) at 2024-07-06 15:17:37 +0000