| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
This avoids a new warning of Coq 8.14.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This big PR adds support for bit fields in structs and unions to
the verified part of CompCert, namely the CompCert C and Clight
languages.
The compilation of bit field accesses to normal integer accesses +
shifts and masks is done and proved correct as part of the Cshmgen
pass.
The layout of bit fields in memory is done by the functions in module
Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic
soundness properties of the layout are shown, such as "two different
bit fields do not overlap" or "a bit field and a regular field do not
overlap".
All this replaces the previous emulation of bit fields by
source-to-source rewriting in the unverified front-end of CompCert
(module cparse/Bitfield.ml). This emulation was prone to errors (see
nonstandard layout instead.
The core idea for the PR is that expressions in l-value position
denote not just a block, a byte offset and a type, but also a bitfield
designator saying whether all the bits of the type are accessed
(designator Full) or only some of its bits (designator
Bits). Designators of the Bits kind appear when the l-value is a bit
field access; the bit width and bit offset in Bits are computed by the
functions in Ctypes that implement the layout algorithm.
Consequently, both in the semantics of CompCert C and Clight and in
the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a
type and a bitfield designator are used in a number of places where a
single type was used before.
The introduction of bit fields has a big impact on static
initialization (module cfrontend/Initializers.v), which had to be
rewritten in large part, along with its soundness proof
(cfrontend/Initializersproof.v).
Both static initialization and run-time manipulation of bit fields are
tested in test/abi using differential testing against GCC and
randomly-generated structs.
This work exposed subtle interactions between bit fields and the
volatile modifier. Currently, the volatile modifier is ignored when
accessing a bit field (and a warning is printed at compile-time), just
like it is ignored when accessing a struct or union as a r-value.
Currently, the natural alignment of bit fields and their storage units
cannot be modified with the aligned attribute. _Alignas on bit fields
is rejected as per C11, and the packed modifier cannot be applied to a
struct containing bit fields.
|
|
|
|
|
| |
The `-version-file` option was removed in commit 600803cae, but remained
in the option summary, as reported in #386.
|
|
|
|
|
| |
The configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".
|
|
|
|
|
| |
This commit adds support for macOS (and probably iOS) running on
AArch64 / ARM 64-bit / "Apple silicon" processors.
|
|
|
|
|
|
| |
Outside of -interp mode, -main has no (known) effect but could be
confused for a linker option that sets the program's entrypoint, say.
It's safer to reject the option.
|
|
|
|
|
|
|
| |
When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function.
This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option.
The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
|
|
|
|
| |
It is specific to AbsInt's commercial version of CompCert.
|
| |
|
| |
|
| |
|
|
|
|
| |
This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
|
|
|
|
|
|
| |
The version string dumped in the file should be the same as the version
string printed by `-version`. The option is also not printed by `-help`
since it is for internal use only.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
The Commandline module is reusable in other projects, and its license
(GPL) allows such reuse, so its natural place is in lib/ rather
than in driver/
|
|
|
|
|
|
|
| |
The list of reserved_registers is never reset between the compilation of
multiple files. Instead of storing them in IRC they are moved in the
CPragmas file and reset in the a new reset function for Cpragmas whic is
called per file.
|
|
|
|
|
|
| |
"open!" is the form used in the examples in the OCaml manual.
Based on a quick poll it seems to be the preferred form of the OCaml
core dev team.
|
|
|
|
|
|
|
|
|
|
| |
Before it was "option typ". Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).
One benefit is that external functions get more precise types that
control better their return values. As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.
|
|
|
|
|
| |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
|
|
|
|
|
|
|
|
| |
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()`.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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
|
|
|
|
| |
Updated man page + better usage message.
|
|
|
|
|
| |
Easier to type, and consistent with `-Os` (optimize for smaller code /
optimize for fewer conditional branches).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
| |
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.
|