aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* Use define for wchar_t typeBernhard Schommer2023-02-011-0/+9
| | | | | | Since the wchar_t type depends on the architecture and the system we are compiling for we replace the typedef to a fixed type by a typedef to a define which is predefined by the compiler itself.
* Handle unstructured 'switch' statements such as Duff's deviceXavier Leroy2022-10-293-6/+11
| | | | | | | | | | | | | | | - New elaboration pass: SwitchNorm - recognizes structured 'switch' statements and puts them in a normalized form; - if selected, transforms unstructured 'switch' statements into a structured switch with goto actions + the original switch body with appropriate labels and gotos. - C2C treatment of 'switch' statements is simplified accordingly. - New language support option `-funstructured-switch`. - Some tests were added (test/regression/switch3.c).
* Revised passing of options to `Parse.preprocessed_file`Xavier Leroy2022-09-271-7/+5
| | | | | | Instead of passing a string that encodes the optional source-to-source transformations to perform, just pass one optional, named argument for each transformation. It is clearer and easier to extend this way.
* Support the `-std=<standard>` option (#456)Xavier Leroy2022-09-233-4/+24
| | | | | | | | | | | | | | It has two effects: - With a GNU toolchain, it's passed down to the preprocessor. This influences the contents of standard includes. - It determines the default effect of the "C11 feature" warning: -std=c99: warn on the use of C11 features -std=c11 or -std=c18: don't warn For backward compatiblity, the default, if no `-std` option is given, is to not warn, but to pass `-std=c99` to the preprocessor. Co-authored-by: Bernhard Schommer <bschommer@users.noreply.github.com>
* Support C11 Unicode string literals and character constants (#452)Xavier Leroy2022-09-191-1/+4
| | | | | | | | | | | | | | | | | * Support C11 Unicode string literals and character constants * Add tests for C11 string literals and character constants * Better error message for ill-formed universal character names E.g. \u followed by fewer than 4 hex digits, or \U followed by fewer than 8 hex digits. * Add new warning `invalid-utf8` for byte sequences that are not valid UTF8. The warning is activated but not fatal by default. * Warn on uses of C11 Unicode character constants and string literals This uses the `c11-extensions` warning, which is off by default. * Support preprocessing option -finput-charset= for GNU toolchains
* Simplify handling of file suffixes.Bernhard Schommer2022-05-183-24/+22
| | | | | | | Since we are sure that all files passed have a valid extension we can use the OCaml function Filename.remove_extension and don't need to pass the suffixes. Bug 33218
* Fix computing of output filenames.Bernhard Schommer2022-05-181-13/+15
| | | | | | | At some places the ".c" was hard coded as suffix for computing the output filenames. This lead to problems if for example `-S`or `-c` is used with preprocessed files. Bug 33196
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-1/+1
| | | | This avoids a new warning of Coq 8.14.
* Native support for bit fields (#400)Xavier Leroy2021-08-223-6/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Remove `-version-file` option from option summaryXavier Leroy2021-04-231-1/+0
| | | | | The `-version-file` option was removed in commit 600803cae, but remained in the option summary, as reported in #386.
* "macosx" is now called "macos"Xavier Leroy2021-01-182-3/+3
| | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
* AArch64: macOS portXavier Leroy2020-12-261-1/+3
| | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
* Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | | | | | 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.
* Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-303-19/+41
| | | | | | | 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.
* Remove -version-file optionXavier Leroy2020-10-121-19/+2
| | | | It is specific to AbsInt's commercial version of CompCert.
* Add missing comment for print_version_file_and_exitChristoph Cullmann2020-07-301-0/+1
|
* No trailing commas for --version-file option.Bernhard Schommer2020-07-091-1/+1
|
* Fix typo.Bernhard Schommer2020-07-081-1/+1
|
* Revert "Use the same version string."Bernhard Schommer2020-07-081-3/+10
| | | | This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
* Use the same version string.Bernhard Schommer2020-07-081-10/+3
| | | | | | 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.
* Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
|
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-3/+5
|
* Add option to print version information in fileBernhard Schommer2020-07-081-1/+17
|
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-196/+0
| | | | | | 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/
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-201-0/+1
| | | | | | | 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.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-2/+2
| | | | | | "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.
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+1
| | | | | | | | | | 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.
* AArch64 portXavier Leroy2019-08-082-1/+2
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* 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.
* 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
* 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
* 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.
generated by cgit (git 2.34.1) at 2024-06-02 17:17:38 +0000