aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
...
| | * Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
| | | | | | | | | | | | Don't use sed, just echo the contents of the file.
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-271-1/+1
|\| |
| * | Adding Duplicatepasses.v to MakefileCyril SIX2020-10-271-1/+1
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+1
|\| |
| * | reorder phasesDavid Monniaux2020-10-161-0/+1
| | |
* | | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-171-1/+1
| | |
* | | ccomp.force target for forcing compilation without Coq processingDavid Monniaux2020-10-011-0/+4
| | |
* | | just missing OpWeights for AARCH64David Monniaux2020-09-161-4/+13
| | |
* | | starting to move common filesDavid Monniaux2020-09-161-1/+1
|/ /
* | automated writing Compiler.vDavid Monniaux2020-04-221-1/+1
| |
* | begin scripting the Compiler.v fileDavid Monniaux2020-04-211-0/+5
| |
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-1/+3
|\ \
| * | attempt at compilingDavid Monniaux2020-04-011-0/+1
| | |
| * | use inject_lDavid Monniaux2020-03-301-1/+1
| | |
| * | more on injectionDavid Monniaux2020-03-301-0/+1
| | |
| * | nop insertion at entrypointDavid Monniaux2020-03-291-1/+1
| | |
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+2
|\ \ \ | |/ / |/| |
| * | reloading and exploiting seems to workDavid Monniaux2020-04-081-0/+1
| | |
| * | begin installing profilingDavid Monniaux2020-04-081-0/+1
| | |
* | | pass to insert a nop at start position in functionsDavid Monniaux2020-03-271-0/+1
| | |
* | | starts compiling but still fakeDavid Monniaux2020-03-101-1/+1
| | |
* | | just the analysisDavid Monniaux2020-03-051-1/+1
| | |
* | | fix MakefileDavid Monniaux2020-03-051-0/+1
| | |
* | | more about extraction and linkingDavid Monniaux2020-03-051-0/+1
|/ /
* | try to get it to compileDavid Monniaux2020-03-031-0/+1
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-141-1/+1
|\ \
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-1/+1
| |\| | | | | | | | | | mppa-work-upstream-merge
| | * Support Coq 8.11.0 (#212)Xavier Leroy2020-02-051-1/+1
| | | | | | | | | | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
* | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-0/+1
|\ \ \ | |/ / |/| |
| * | CSE2 split in two filesDavid Monniaux2020-01-281-0/+1
| |/
* | connect forward-moves to compilerDavid Monniaux2020-01-081-0/+1
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-0/+1
|\ \
| * | Stubs for Duplicate passCyril SIX2019-09-031-0/+1
| | |
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-101-0/+1
|\ \ \ | |/ / |/| / | |/ mppa-non-trapping-load
* | 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.
generated by cgit (git 2.34.1) at 2024-05-20 04:17:57 +0000