aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* moved stuff to appropriate places and removed irrelevant contentDavid Monniaux2022-02-111-0/+18
|
* Merge ../kvx-work into kvx_fp_divisionDavid Monniaux2022-02-031-2/+2
|\
| * Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-02-021-2/+2
| |\
| | * Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-101-2/+2
| | | | | | | | | | | | | | | | | | | | | coq/coq#15442 changes the way `Program` names things, to make it uniform w.r.t. the standard naming schema. This commit removes dependencies on the names chosen by `Program`. Should be backwards compatible. Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr>
* | | moved functions to a more logical placeDavid Monniaux2022-01-131-165/+179
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_divisionDavid Monniaux2021-12-142-742/+915
|\| |
| * | Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-012-742/+915
| |\| | | | | | | | | | Mostly changes in PTree
| | * Maps.v: transparency of NodeXavier Leroy2021-11-161-1/+3
| | | | | | | | | | | | Add one more `Local Transparent Node` to ensure compatibility with Coq < 8.12
| | * An improved PTree data structure (#420)Xavier Leroy2021-11-162-638/+902
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This PR replaces the "PTree" data structure used in lib/Maps.v by the canonical binary tries data structure proposed by A. W. Appel and described in the paper "Efficient Extensional Binary Tries", https://arxiv.org/abs/2110.05063 The new implementation is more memory-efficient and a bit faster, resulting in reduced compilation times (-5% on typical C programs, up to -10% on very large C functions). It also enjoys the extensionality property (two tries mapping equal keys to equal data are equal), which simplifies some proofs.
* | | Values: conversions to nearest intDavid Monniaux2021-12-121-0/+9
| | |
* | | _ne conversionsDavid Monniaux2021-12-121-0/+9
| | |
* | | progress on lemmasDavid Monniaux2021-12-121-1/+81
| | |
* | | minor implicit issueDavid Monniaux2021-12-101-2/+2
| | |
* | | more properties on ZnearestDavid Monniaux2021-12-101-2/+35
| | |
* | | factor proofsDavid Monniaux2021-12-101-1/+20
| | |
* | | factorize proofDavid Monniaux2021-12-101-28/+22
| | |
* | | beautify proofDavid Monniaux2021-12-101-24/+16
| | |
* | | ZofB_ne_correctDavid Monniaux2021-12-101-0/+10
| | |
* | | ZofB_ne_correctDavid Monniaux2021-12-101-2/+31
| | |
* | | progress on ZnearestEDavid Monniaux2021-12-101-24/+54
| | |
* | | ZofB_ne_correct unfinishedDavid Monniaux2021-12-081-1/+18
| | |
* | | Merge branch 'kvx_fp_division' of ↵David Monniaux2021-12-071-1/+1
|\ \ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx_fp_division
| * | | ZnearestE_oppDavid Monniaux2021-12-071-4/+83
| | | |
* | | | ZnearestE_oppDavid Monniaux2021-12-071-3/+121
|/ / /
* | | progress on ZofB_neDavid Monniaux2021-12-061-0/+51
| | |
* | | Zdiv_neDavid Monniaux2021-12-061-0/+11
|/ /
* | option monad tacticSylvain Boulmé2021-11-061-1/+7
| |
* | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-292-23/+23
|\|
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-23/+23
| | | | | | | | This avoids a new warning of Coq 8.14.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-245-4/+198
|\|
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-154-2/+4
| | | | | | | | | | | | Instead, add `Set Asymmetric Patterns` to the files that need it, or use `Arguments` to make inductive types work better with symmetric patterns. Closes: #403
| * Native support for bit fields (#400)Xavier Leroy2021-08-221-0/+112
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
| | | | | | | | | | | | Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly
| * Add `floor` and some propertiesXavier Leroy2021-07-261-0/+37
| |
| * More lemmas about `align`Xavier Leroy2021-07-261-0/+17
| |
| * More lemmas about list appendXavier Leroy2021-07-261-0/+26
| |
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0831-124/+155
| | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
| * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-20/+0
| |
* | Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1033-1327/+1365
|\ \
| * | coq 8.13.2David Monniaux2021-06-071-2/+1
| | |
| * | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-0131-144/+155
| | | | | | | | | | | | cfrontend/C2C.ml
| * | replacing omega with lia in some fileLéo Gourdin2021-03-292-32/+34
| | |
| * | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2315-1150/+1176
| |\| | | | | | | | | | | | | | | | | | | | | | | | | 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
| | * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-213-33/+36
| | | | | | | | | | | | | | | | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
| | * Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| | | | | | | | | | | | | | | | | | The extraction mechanism wants to extract them (because they are in Type, probably). The current opaque definition causes a warning at extraction-time.
| | * Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | | | | | | | | | | | | | | | | | | | | fold_inv is in Type, hence can prove goals such as `{ x | P x }`. Also, no extensionality property is needed. fold_rec is now derived from fold_inv.
| | * Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
| | |
| | * Replace `omega` tactic with `lia`Xavier Leroy2020-12-2914-1026/+1022
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
| | * Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | IEEE754_extra: clear unused context so that none of the context is picked up by tactics and ends as extra parameters to theorems int_round_odd_bits and int_round_odd_le Floats: simplify uses of int_round_odd_bits and int_round_odd_le accordingly.
* | | better autodestruct ?Sylvain Boulmé2021-05-111-1/+16
| | |
generated by cgit (git 2.34.1) at 2024-05-09 06:29:41 +0000