| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| |
| | |
mppa-if-conversion
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| | |
The AbsInt build number no longer contains "release", so it must
be printed additionally.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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.
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | |
|
|\ \ |
|
| | | |
|
|/ / |
|
|\ \ |
|
| | | |
|
| | | |
|
|/ /
| |
| |
| | |
(-fpostpass nameofscheduler)
|
| | |
|
|\ \
| | |
| | |
| | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
|
| | | |
|
| | | |
|
|/ / |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
.gitignore
|
| |
| |
| |
| |
| |
| | |
Instead of just passing -u to the linker also pass the value of
the option to the linker.
Bug 24316
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| |
| |
| |
| |
| |
| | |
Fix various typos in diagnostic messages and unified wording and
capitalization.
Bug 23850
|
| |
| |
| | |
The `-iquote` option was passed to the GNU preprocessor as `-iquore`
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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.
|
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| |
| |
| |
| | |
machblock
|
| | |
|
| | |
|
| | |
|
| | |
|
|/ |
|
| |
|
|
|
|
|
|
| |
Since the used configuration for passing and returning values
struct values is pretty much static it can be hardwired into the
machine settings.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
CompCert now accepts the target configuration option of the diab
data compiler and passes it on to the preprocessor, assembler and
linker.
Bug 20521
|
|
|
|
|
| |
This time with the correct place for setting the destination files.
Bug 20521
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|