aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-1/+1
|\
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-1/+1
| | | | | | | | This avoids a new warning of Coq 8.14.
* | Merge branch 'towards_2.10' of ../towards_3.10 into kvx-workDavid Monniaux2021-09-303-6/+4
|\ \
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-243-6/+4
| |\|
| | * 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.
* | | activate non trapping loads on the KVXDavid Monniaux2021-09-281-1/+1
|/ /
* | - make non trapping loads in scheduling dependent on option (which was ↵David Monniaux2021-09-141-1/+1
| | | | | | | | | | | | ignored on BTL) - set this option to false, since Kalray still ships a buggy runtime system
* | [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-011-5/+3
|\ \
| * \ Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-103-5/+7
| |\ \
| * | | Dupmap bugfix and some advance in LivegenLéo Gourdin2021-05-311-0/+2
| | | |
| * | | BTL Scheduler oracle and some draftsLéo Gourdin2021-05-311-1/+1
| | | |
| * | | fix some merge errorsLéo Gourdin2021-05-281-1/+1
| | | |
| * | | Merge branch 'BTL' into BTL-translationLéo Gourdin2021-05-192-0/+4
| |\ \ \
| * | | | preparing compiler passes and ml oraclesLéo Gourdin2021-05-171-6/+2
| | | | |
* | | | | Merge branch 'kvx-work' into rtl-tunnelingSylvain Boulmé2021-07-242-6/+12
|\ \ \ \ \
| * | | | | activate register pressure by defaultDavid Monniaux2021-07-162-5/+5
| | | | | |
| * | | | | use a more recognizable option nameDavid Monniaux2021-07-162-3/+3
| | | | | |
| * | | | | Change temporary solution (see prev commits), and add option for itnicolas.nardino2021-06-282-0/+3
| | | | | |
| * | | | | Another schedulernicolas.nardino2021-06-241-1/+1
| | | | | |
| * | | | | Changed default threshold value following testsnicolas.nardino2021-06-221-1/+1
| | | | | |
| * | | | | Add option to set thresold and support for riscvnicolas.nardino2021-06-172-0/+3
| | | | | |
| * | | | | scheduler written, need to test nownicolas.nardino2021-06-141-1/+1
| | |_|/ / | |/| | |
* / | | | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-171-1/+1
|/ / / / | | | | | | | | | | | | To respect the symmetry between RTL- and LTL-Tunneling
* | | | Add target ELFCyril SIX2021-06-011-0/+1
| | | |
* | | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-015-2/+11
|\ \ \ \ | | |/ / | |/| |
| * | | Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-192-0/+4
| |/ /
| * | Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-133-1/+8
| | |
| * | Remove flagsLéo Gourdin2021-04-092-4/+0
| | |
| * | Compiler options to manage expansionsLéo Gourdin2021-03-262-2/+2
| | |
| * | Adding a flag to test fp_init_expLéo Gourdin2021-03-022-0/+2
| | |
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-1/+0
| | | | | | | | | | | | cfrontend/C2C.ml
* | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-232-4/+6
|\ \ \ | |/ / |/| / | |/ | | | | | | | | | | 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-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.
* | Adding a compiler option -fexpanse-rtlcondLéo Gourdin2021-02-162-0/+2
| |
* | Conditions now propagated by CSE3David Monniaux2021-01-203-1/+8
|\ \ | | | | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * | begin implementing -fcse3-conditionsDavid Monniaux2020-12-093-0/+7
| | |
| * | CSE3 compiles again, but some admitted lemmasDavid Monniaux2020-12-091-1/+1
| | |
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-087-229/+51
| |\ \
| * | | start checking for bugsDavid Monniaux2020-12-021-1/+1
| | | |
* | | | Fix --help for prepass (new options)Léo Gourdin2021-01-141-1/+1
| | | |
* | | | Fix --help for prepass (default on)Léo Gourdin2021-01-141-1/+1
| | | |
* | | | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-177-229/+51
|\ \ \ \ | | |/ / | |/| |
| * | | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-0/+2
| |\ \ \ | | | |/ | | |/|
| | * | 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.
| * | | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-043-2/+24
| |\ \ \ | | | |/ | | |/| | | | | | | | | | | | | Conflicts: Makefile configure
| * | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-229/+49
| |\ \ \ | | | |/ | | |/|
| | * | 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.
generated by cgit (git 2.34.1) at 2024-05-09 08:58:30 +0000