aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* Stubs for Duplicate passCyril SIX2019-09-031-0/+1
|
* Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-281-0/+1
|\ | | | | | | mppa-work-upstream-merge
| * Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-051-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | The "undeclared-scope" warning fires when we use a "notation" scope before having declared it. This is a good thing, except that the "Declare Scope" vernacular that declares a scope was introduced in Coq 8.10 and is not available in earlier versions. Hence there is no way to avoid triggering the warning yet remain compatible with pre-8.10 Coq versions. This commit silences the warning. It will have to revisited when Coq 8.10 is the oldest version of Coq we support in CompCert.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-12/+12
|\| | | | | | | mppa-work-upstream-merge
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
| * Type inference and type checking for CminorXavier Leroy2019-06-061-1/+1
| | | | | | | | | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-25/+22
|\ \ | | | | | | | | | mppa-if-conversion
| * | Type inference and type checking for CminorXavier Leroy2019-05-311-1/+1
| |/ | | | | | | | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
| * Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-171-12/+12
| | | | | | | | | | | | | | | | Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs.
| * Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-261-1/+1
| | | | | | | | | | To match the new module names from version 3 of Flocq. Plus, it's shorter.
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+1
| | | | | | | | | | | | | | | | | | | | 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.
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-11/+8
| | | | | | | | | | | | | | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
* | ça recompile sur x86David Monniaux2019-03-221-1/+1
| |
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-5/+2
|\| | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * Ignore and clean file .lia.cacheXavier Leroy2019-02-121-0/+1
| | | | | | | | This file is created by Coq when running some tactics
| * Make the checker happy (#272)Vincent Laporte2019-02-121-5/+1
| | | | | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
* | Adding Mem as a possible location for accessesCyril SIX2019-01-111-0/+1
| |
* | compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-281-1/+1
| |
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-4/+5
| |
* | Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow thatCyril SIX2018-11-261-3/+3
| |
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-13/+20
|\| | | | | | | | | Conflicts: .gitignore
| * Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
| | | | | | | | | | | | | | For consistency with other generated .v files, and because it protects against editing the generated file, see Github issue #248. Closes: #248
| * Ensure compatibility with Menhir before and after version 20180530Xavier Leroy2018-06-061-1/+1
| | | | | | | | Inspired by and adapted from pull request #235 by Benoît Viguier.
| * Fix menhirLib namespaces, following changes in Menhir version 20180530Jacques-Henri Jourdan2018-06-061-2/+2
| |
| * Use the standalone coq2html tool to generate the HTML documentationXavier Leroy2018-06-011-10/+2
| | | | | | | | | | coq2html is now a standalone project (https://github.com/xavierleroy/coq2html) packaged as coq-coq2html in OPAM-Coq.
| * Install the VERSION file along the .vo filesBenoît Viguier2018-05-311-0/+1
| | | | | | This is useful for the VST project and can be useful for others.
| * Install Coq development (.vo files) if requested (#232)Xavier Leroy2018-05-301-1/+10
| | | | | | | | | | | | | | | | | | .vo files are installed if configure options -install-coqdev or -clightgen or -coqdevdir are given. Installation directory is $(PREFIX)/lib/compcert/coq by default and can be changed by configure option -coqdevdir. Closes: #227
| * Upgrade Flocq to version 2.6.1 from upstream (#71)Xavier Leroy2018-04-251-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We were previously at 2.5.2. Quoting the NEWS from upstream: Version 2.6.1: - ensured compatibility from Coq 8.4 to 8.8 Version 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Also: in preparation for Coq 8.8, silence warning "compatibility-notation" when building Flocq, because this warning is on by default in 8.8, and Flocq triggers it a lot.
* | Removed the bundle attemptCyril SIX2018-09-281-1/+0
| |
* | MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-251-1/+1
| |
* | a few stubs for bundlingSylvain Boulmé2018-09-241-0/+1
| |
* | premier jet Asmblockgenproof.return_address_offsetSylvain Boulmé2018-09-181-1/+1
| |
* | Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-061-1/+1
| |
* | Asmblock: Adding forward_simulation and determinism as axiomsCyril SIX2018-09-061-1/+1
| |
* | Asmblockgen.v finished (no proof yet)Cyril SIX2018-09-061-1/+1
| |
* | Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléterCyril SIX2018-09-061-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Asmblock.v: - Rajout de "header" dans wf_bblock - Remplacer "code" par "bblocks". Pour la suite, je trouve plus clair de manipuler des bblocks, plutôt qu'un "code constitué de bblocks". ça permet de minimiser les modifications dans Asmblockgen.v - fn_code --> fn_blocks . fn_code ne devrait pas être utilisé dans le code OCaml de toute façon (vu la translation Asmblock -> Asm) - Rajout d'un type instruction qui regroupe les basic et les control ; facilite certaines définitions Asmblockgen.v: - Copie conforme de Asmgen.v, avec quelques changements (pas fini). Ce vers quoi je m'oriente : garder les fonctions existantes de génération de code ; on leur donne à manger la liste de basics de Machblock. On traduit le exit (qui peut spiller sur la liste de basics déjà traduite), et on met la dernière instruction de la trad du exit (qui doit être un control) dans le exit du bblock. - Pour le prologue : chaque instruction rajoutée "à la main" est dans son propre bblock. Voir la notation ::b pour le faire. A terme, il devrait y avoir moyen "d'accumuler" l'instruction au code généré ; pour l'instant je préfère ne pas compliquer la génération.
* | Machblock: Mach language with basic blocksCyril SIX2018-09-061-1/+2
|/
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-281-3/+0
| | | | | | | Implicit Arguments is deprecated in Coq since 8.6 or so. Some Implicit Arguments remained in Flocq but were recently changed to Arguments. Apply the same change to our local copy of Flocq. As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
* Removed no longer needed struct passing.Bernhard Schommer2018-02-261-2/+0
|
* Fix check-proof target of the Makefile after merge of Coq #6277.Pierre-Marie Pédrot2017-12-071-1/+1
| | | | We simply fully qualify the modules. This is backward compatible.
* Makefile: chmod a-w instead of chmod -wXavier Leroy2017-09-111-1/+1
| | | | | The latter, in conjunction with some values of the umask, gives weird messages "new permissions are ... not ...".
* Update the "make check-proof" entry for Coq 8.6Xavier Leroy2017-03-241-3/+2
| | | | `-admit Floats` is no longer needed, but Integers and SelectDivproof still need admitting.
* Turn warning "deprecated-implicit-arguments" off while compiling FlocqXavier Leroy2017-02-131-1/+4
| | | | Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
* Also remove coq aux files.Bernhard Schommer2017-01-241-0/+1
|
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-1/+1
| | | | | | | | Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.) The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque. Fixes #151
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-10/+26
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-8/+23
| | | | | | | | | | | | | | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-2/+3
| | | | | | | | | | | | | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* | Add a man-pageMichael Schmidt2016-10-141-0/+2
|/