| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Merge branch 'towards_2.10' of ../towards_3.10 into kvx-work | David Monniaux | 2021-09-30 | 1 | -1/+0 |
| |\ | |||||
| | * | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-24 | 1 | -1/+0 |
| | |\ | |||||
| | | * | Native support for bit fields (#400) | Xavier Leroy | 2021-08-22 | 1 | -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. | ||||
| * | | | activate non trapping loads on the KVX | David Monniaux | 2021-09-28 | 1 | -1/+1 |
| |/ / | |||||
| * | | - make non trapping loads in scheduling dependent on option (which was ↵ | David Monniaux | 2021-09-14 | 1 | -1/+1 |
| | | | | | | | | | | | | | ignored on BTL) - set this option to false, since Kalray still ships a buggy runtime system | ||||
| * | | activate register pressure by default | David Monniaux | 2021-07-16 | 1 | -1/+1 |
| | | | |||||
| * | | use a more recognizable option name | David Monniaux | 2021-07-16 | 1 | -1/+1 |
| | | | |||||
| * | | Change temporary solution (see prev commits), and add option for it | nicolas.nardino | 2021-06-28 | 1 | -0/+1 |
| | | | |||||
| * | | Changed default threshold value following tests | nicolas.nardino | 2021-06-22 | 1 | -1/+1 |
| | | | |||||
| * | | Add option to set thresold and support for riscv | nicolas.nardino | 2021-06-17 | 1 | -0/+1 |
| | | | |||||
| * | | Adding both RV expansion methods in kvx-work | Léo Gourdin | 2021-05-19 | 1 | -0/+2 |
| | | | |||||
| * | | Remove flags | Léo Gourdin | 2021-04-09 | 1 | -2/+0 |
| | | | |||||
| * | | Compiler options to manage expansions | Léo Gourdin | 2021-03-26 | 1 | -1/+1 |
| | | | |||||
| * | | Adding a flag to test fp_init_exp | Léo Gourdin | 2021-03-02 | 1 | -0/+1 |
| | | | |||||
| * | | Adding a compiler option -fexpanse-rtlcond | Léo Gourdin | 2021-02-16 | 1 | -0/+1 |
| | | | |||||
| * | | Conditions now propagated by CSE3 | David Monniaux | 2021-01-20 | 1 | -1/+3 |
| |\ \ | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work | ||||
| | * | | begin implementing -fcse3-conditions | David Monniaux | 2020-12-09 | 1 | -0/+2 |
| | | | | |||||
| | * | | CSE3 compiles again, but some admitted lemmas | David Monniaux | 2020-12-09 | 1 | -1/+1 |
| | | | | |||||
| | * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 1 | -0/+1 |
| | |\ \ | |||||
| | * | | | start checking for bugs | David Monniaux | 2020-12-02 | 1 | -1/+1 |
| | | | | | |||||
| * | | | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 1 | -0/+1 |
| |\ \ \ \ | | |/ / | |/| | | |||||
| | * | | | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 1 | -0/+7 |
| | |\| | | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure | ||||
| | * | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 1 | -0/+1 |
| | |\ \ \ | | | |/ | | |/| | |||||
| | | * | | Add -main option to specify entrypoint function in interpreter mode (#374) | Xavier Leroy | 2020-10-30 | 1 | -0/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||||
| * | | | | set prepass by default | David Monniaux | 2020-11-27 | 1 | -1/+1 |
| | |_|/ |/| | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-03 | 1 | -0/+1 |
| |\| | | |||||
| | * | | Loop Rotate with -flooprotate | Cyril SIX | 2020-11-03 | 1 | -0/+1 |
| | | | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-31 | 1 | -0/+1 |
| |\| | | |||||
| | * | | refining CSE3 nodes | David Monniaux | 2020-10-31 | 1 | -0/+1 |
| | | | | |||||
| | * | | deactivate LICM | David Monniaux | 2020-10-28 | 1 | -1/+1 |
| | | | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 1 | -0/+2 |
| |\| | | |||||
| | * | | new option for CSE3 (trivial ops) | David Monniaux | 2020-10-27 | 1 | -0/+2 |
| | | | | |||||
| * | | | deactivate LICM by default | David Monniaux | 2020-10-27 | 1 | -1/+1 |
| | | | | |||||
| * | | | -mtune= | David Monniaux | 2020-10-22 | 1 | -0/+2 |
| | | | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 1 | -3/+11 |
| |\| | | |||||
| | * | | Loop body unrolling with -funrollbody n | Cyril SIX | 2020-10-16 | 1 | -0/+1 |
| | | | | |||||
| | * | | new flags: -fpredict, -ftailduplicate n, -funrollsingle n instead of just ↵ | Cyril SIX | 2020-10-09 | 1 | -3/+7 |
| | | | | | | | | | | | | | -fduplicate n | ||||
| * | | | command line selection of prepass scheduler | David Monniaux | 2020-07-11 | 1 | -0/+1 |
| | | | | |||||
| * | | | use a command-line option | David Monniaux | 2020-07-08 | 1 | -0/+1 |
| |/ / | |||||
| * | | k1c -> kvx changes | David Monniaux | 2020-05-26 | 1 | -1/+1 |
| | | | |||||
| * | | -fcse3-glb | David Monniaux | 2020-05-06 | 1 | -0/+1 |
| | | | |||||
| * | | CSE3 across merges | David Monniaux | 2020-05-06 | 1 | -0/+1 |
| | | | |||||
| * | | Merge branch 'mppa-work' of ↵ | David Monniaux | 2020-04-23 | 1 | -2/+13 |
| |\ \ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| | * \ | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-23 | 1 | -2/+3 |
| | |\ \ | |||||
| | | * | | CSE3 across calls | David Monniaux | 2020-04-23 | 1 | -1/+2 |
| | | | | | |||||
| | | * | | Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licm | David Monniaux | 2020-04-23 | 1 | -0/+1 |
| | | |\ \ | |||||
| | | | * | | make tracing output optional | David Monniaux | 2020-04-23 | 1 | -0/+1 |
| | | | | | | |||||
| | * | | | | Merge remote-tracking branch 'origin/mppa-fast-div' into mppa-features | David Monniaux | 2020-04-20 | 1 | -0/+2 |
| | |\ \ \ \ | |||||
| | | * \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div | David Monniaux | 2020-04-20 | 1 | -2/+12 |
| | | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | (unfinished) | ||||
| | | * | | | | | added -fdiv-i32 and -fdiv-i64 options | David Monniaux | 2019-05-29 | 1 | -0/+3 |
| | | | | | | | | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |