aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-1/+0
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-1/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Add target ELFCyril SIX2021-06-011-0/+1
| |
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-1/+4
|\ \
| * | Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-1/+4
| | |
* | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-3/+5
|\ \ \ | |/ / |/| / | |/ | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * "macosx" is now called "macos"Xavier Leroy2021-01-181-2/+2
| | | | | | | | | | 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.
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-0/+1
|\|
| * 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.
* | k1c -> kvx changesDavid Monniaux2020-05-261-1/+1
| |
* | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-201-0/+1
|\| | | | | | | mppa-work-upstream-merge
| * AArch64 portXavier Leroy2019-08-081-0/+1
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-1/+1
|\| | | | | | | 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()`.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-4/+26
|\| | | | | | | mppa-if-conversion
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-2/+2
| | | | | | | | | | | | 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.
| * 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
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-6/+17
|\| | | | | | | | | Conflicts: .gitignore
| * 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
| * 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`
| * 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
* | Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-041-0/+1
|/
* 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.
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-12/+3
| | | | | | | | | | | | | | | | | * 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.
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-111-0/+25
| | | | | 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.
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-041-12/+2
| | | | | This time with the correct place for setting the destination files. Bug 20521
* Introduced configuration variable for gnu systems.Bernhard Schommer2017-02-131-2/+2
| | | | | | | The variable gnu_toolchain is true if a gnu toolchain is used and false in all other cases. The variable avoids the explicit test whether the system string is diab and should be easier to change. Bug 20521.
* Use quoted strings.Bernhard Schommer2017-01-181-32/+34
| | | | | | Instead of escaping all newlines etc for the help options use quoted strings. Bug 19872
* Moved assembler and linker into own files.Bernhard Schommer2016-06-241-2/+2
| | | | | | The function to call the assembler and the linker are now in own files like the preprocessor. Bug 19197
* Deactivate options target dependend.Bernhard Schommer2016-06-241-48/+49
| | | | | | Options only available for gnu systems or arm target arch are no longer displayed in the help and cannot be selected any longer. Bug 19197
* Moved shared frontend code in own file.Bernhard Schommer2016-05-241-0/+163
Clightgen and CompCert share the code for preprocessing as well as parsing C files. The code as well as command line switches is moved in the new module Frontend. Bug 18768
generated by cgit (git 2.34.1) at 2024-05-19 23:08:45 +0000