aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* 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
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-171-1/+1
| | | | | | | | | | | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
| * -O0 now implies -fno-inliningMichael Schmidt2019-07-091-1/+1
| |
| * Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
| * Update documentation of -ObranchlessXavier Leroy2019-07-051-1/+1
| | | | | | | | Updated man page + better usage message.
| * Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-052-4/+4
| | | | | | | | | | Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches).
| * If-conversion optimizationXavier Leroy2019-06-062-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.
* | (#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.
| * 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.
generated by cgit (git 2.34.1) at 2024-07-12 00:17:00 +0000