aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-102-9/+9
| | | | | | | | | | | | | | | * 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-222-3/+3
| | | | Adapt w.r.t. coq/coq#16904.
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-195-1/+8
| | | | | | And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
* Introducing the "eventually" closure and new simulation diagrams using itXavier Leroy2022-09-051-27/+229
| | | | | | These diagrams enable the source program to make a number of finite transitions before eventually reaching a state that restores the simulation relation.
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-292-13/+19
| | | | | | | | | | | | On platforms that support them (ELF, macOS), use mergeable sections (like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals. Works only if the LITERAL section is the default one. If the user provided their own LITERAL section, all literals are put in it regardless of their sizes. Support for mergeable string sections is introduced in this commit too but needs further changes in C2C.ml .
* Add [#global] qualifier on Hint Rewrite (#439)Pierre-Marie Pédrot2022-07-051-0/+4
| | | Adapt w.r.t. coq/coq#16004.
* Update comment re: compile_switch functionXavier Leroy2022-06-251-1/+1
| | | | Fixes: #435
* Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-102-4/+4
| | | | | | | 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>
* An improved PTree data structure (#420)Xavier Leroy2021-11-162-19/+1
| | | | | | | | | | | | | | 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-031-10/+10
| | | | This avoids a new warning of Coq 8.14.
* Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-1/+1
| | | | The change is backward compatible with Coq 8.9 to 8.13 (at least).
* For numerical builtins, support return types that are small integer typesXavier Leroy2021-09-221-25/+47
|
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-152-1/+2
| | | | | | 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
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0822-88/+110
| | | | | | 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.
* Support __builtin_unreachableXavier Leroy2021-05-021-0/+5
| | | | Not yet used for optimizations.
* Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-192-15/+15
|
* Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
| | | | | | coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters. There was one place in CompCert where one of these automatically-generated names was used. This commit avoids using this name.
* Section handling: finer control of variable initializationXavier Leroy2021-02-232-25/+54
| | | | | | | | | | | | | Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8.
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-216-12/+12
| | | | | | | 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`.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2912-382/+382
| | | | | | | | | | | 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`.
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-5/+5
| | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-0/+1
| | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
* Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+5
|
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-211-1/+1
| | | | | | | As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
* Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-292-10/+23
| | | | | | | | Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them.
* Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
| | | | | The proof script for Events.excall_free_ok was incomplete if Archi.ptr64 is unknown (as in the RISC-V case).
* Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-14/+30
| | | | | | | | According to ISO C, `free(NULL)` is correct and does nothing. This commit updates accordingly the formal semantics of the `free` external function and the reference interpreter. Closes: #334
* Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-15/+33
| | | | | | | | Currently we require the memory to be unchanged on readonly locations. This is too strong. For example, current permissions could decrease from readonly to none. This commit weakens the ec_readonly condition to the strict minimum needed to show the correctness of value analysis for const globals.
* Refine the type of function results in AST.signatureXavier Leroy2020-02-219-80/+189
| | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-112-3/+23
|\ | | | | | | Support target architecture AArch64 (ARMv8 in 64-bit mode)
| * Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
| |
| * Errors: fixed a loop in tactic MonadInvXavier Leroy2019-08-071-1/+1
| |
| * Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
| |
| * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-072-6/+6
| | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-1/+23
| | | | | | | | | | | | | | | | | | | | | | | | * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM.
* | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-052-6/+6
|/ | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-8/+647
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
* Additional simulation diagrams for determinate source languagesXavier Leroy2019-06-061-0/+173
| | | | | If the source language is determinate, it can take several steps (not just one) before the "match_state" invariant is reinstated.
* 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.
* Support a "select" operation between two valuesXavier Leroy2019-05-201-0/+126
| | | | | | | | | | `Val.select ob v1 v2 ty` is a conditional operation that chooses between the values `v1` and `v2` depending on the comparison `ob : option bool`. If `ob` is `None`, `Vundef` is returned. If the selected value does not match type `ty`, `Vundef` is returned. This operation will be used to model a "select" (or "conditional move") operation at the CminorSel/RTL/LTL/Mach level.
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-4/+5
| | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-234-11/+11
| | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-234-20/+20
| | | | | | | Use Z.to_nat theorems from the standard Coq library in preference to our theorems in lib/Coqlib.v. Simplify lib/Coqlib.v accordingly.
* Update the comment of the free operation (#277)chaomaer2019-03-251-1/+1
| | | | The comment says "writable" but it should be "freeable".
* Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-271-41/+53
| | | | | | | | | | | | | CompCert currently uses `Instance` in so-called "refine" mode, where Coq drops automatically in proof mode if some members of the instance are missing. This mode is soon going to be turned off by default, see https://github.com/coq/coq/pull/9270. In order to make CompCert robust against this change, this commit replaces those occurrences of `Instance` that use "refine" mode with `Program Instance`.
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-052-0/+6
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+34
|
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-1/+1
|\ | | | | | | Ensure FunInd or Recdef is imported if functional induction is used. This is necessary for Coq 8.7.0.
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-1/+1
| | | | | | | | | | | | Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-195-11/+13
| | | | | | | | | | | | | | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
generated by cgit (git 2.34.1) at 2024-05-18 04:53:01 +0000