aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-102-2/+7
| | | | | | | | | | | | | | | * Define our own `Z_div_mod_eq` lemma The one in the Coq standard library is deprecated since 8.14, but its replacement changed type between 8.13 and 8.14. So the only way to remain compatible from 8.12 to 8.16 is to define our own lemma. Phew. * Do not use `Arith.Max`, deprecated. * Do not use `plus_lt_compat_r`, deprecated. * Do not use `beq_nat_refl` and `beq_nat_true`, deprecated.
* Use `exfalso` instead of `elimtype False` (#470)Pierre-Marie Pédrot2022-12-221-1/+1
| | | | Adapt w.r.t. coq/coq#16904.
* Replace CR, FF and VT with whitespace.Bernhard Schommer2022-11-051-3/+5
| | | | | | | | We use Printlines to copy C code fragments to assembly comments. While CR, FF and VT are treated like whitespace by C, they could possibly mess up the assembly comments if copied verbatim. Moreover, this avoids generating CR CR LF end-of-lines under Windows. Bug 34075
* Use open_in_bin instead of open_in.Bernhard Schommer2022-11-051-1/+1
| | | | | | | On platforms that do distinguish between text mode and binary mode, seek_in cannot reliably be used on files opened in text mode (open_in). The input file must therefore be opened in binary mode (open_in_bin). Bug 34075
* Add `Commandline.longopt` function for options of the form `-<key>=<arg>`Xavier Leroy2022-09-232-20/+18
| | | | | Also: use `int_of_string_opt` instead of `int_of_string` for slightly cleaner code.
* Improved auto goal selection (#443)Andrej Dudenhefner2022-09-081-2/+2
| | | | | | Improves robustness in case of stronger (e)auto. This is in preparation of a change in Coq that will make auto and eauto stronger (https://github.com/coq/coq/pull/16293).
* Add [#global] qualifier on Hint Rewrite (#439)Pierre-Marie Pédrot2022-07-051-0/+8
| | | Adapt w.r.t. coq/coq#16004.
* Extend the boolean_equality tactic (#429)Jerome Hugues2022-06-251-1/+15
| | | | | Handle constructors with 5, 6 and 7 arguments. Handle lists.
* Upgrade to Flocq 4.1.Guillaume Melquiond2022-04-261-2/+2
|
* Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-252-148/+132
|
* Introduce float_conversion_default_nan parameter for float-float conversionsBernhard Schommer2022-04-251-2/+7
| | | | | | | | | | | | | For RISC-V we need to return the canonical NaN value if the argument of a float32->float64 or float64->float32 conversion is any NaN. This is in line with 11.3 from the RISC-V manual, the description of the conversion operations as well as what the spike ISA simulator and qemu do. Other platforms convert the NaN payload (by truncation or expansion) in float32->float64 and float64->float32 conversions. Fixes: #428
* 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>
* 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.
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-23/+23
| | | | This avoids a new warning of Coq 8.14.
* 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
|
* 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.
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-212-4/+3
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | | | | Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Add a canonical encoding of identifiers as numbers and use it in clightgen ↵Xavier Leroy2020-05-191-3/+76
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#353) Within CompCert, identifiers (names of C functions, variables, types, etc) are represented by unique positive numbers, sometimes called "atoms". In the original implementation, atoms 1, 2, ..., N are assigned to identifiers as they are encountered. The resulting number are small and are efficient when used as keys in data structures such as PTrees. However, the mapping from C source-level identifiers to atoms differs between compilation units. This is not a problem for CompCert but complicates CompCert-based verification tools that need to combine several compilation units. This commit introduces an alternate implementation of atoms, suggested by Andrew Appel. The choice between implementations is governed by the Boolean reference `Camlcoq.use_canonical_atoms`. In the alternate implementation, identifiers are converted to bit sequences via a Huffman encoding, then the bits are represented as positive numbers. The same identifier is always represented by the same number. However, the numbers are usually bigger than in the original implementation, making PTree operations slower: lookups and updates take time linear in the length of the identifier, instead of logarithmic time in the number of identifiers encountered. The CompCert compiler (the `ccomp` executable) still uses the original implementation, but the `clightgen` tool used in conjunction with the VST program logic can use either implementations: - The alternate "canonical atoms" implementation is used by default, and also if the `-canonical-idents` option is given. - The original implementation is used if the `-short-idents` option is given. Closes: #222 Closes: #311
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+196
| | | | | | 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/
* Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | | | | So as not to depend on an implicit import from module Program. (See PR #352.)
* Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | | | | | On some versions of Coq, "nil" is of type "Rlist"... This reverts commit f070949a7559675af3e551e16e5cae95af5d4285.
* Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
| | | | | The rest of the code base uses `nil`, so let's be consistent. Also, this avoids depending on `Import ListNotations`.
* Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
| | | | Just moved a frequent failure case ahead of a costly "simpl".
* Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-1/+1
| | | | A stronger `intuition` in the near future would break this use of `intuition`.
* More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
| | | | The proposed proof only uses `zify` for closing the goal. This is needed for Coq PR #10982 which changes the inner working of `zify`.
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-7/+9
| | | | | | | Some hints will move from the core database to the `ordered_type` database (see https://github.com/coq/coq/pull/9772). This commit prepares for this move by adding `with ordered_type` to the invocations of `auto` and `eauto` that use the hints in question.
* AArch64 portXavier Leroy2019-08-081-24/+136
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
|
* Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
| | | | Should simplify reasoning over Boolean equalities.
* Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
|
* Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
| | | | Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
* Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
|
* Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
|
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+2
| | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
| | | | | It supports a branch-free implementation of floatofintu. Not used yet in any of the ports.
generated by cgit (git 2.34.1) at 2024-06-02 16:42:33 +0000