aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-0/+106
|\
| * shrxl_shrl_3David Monniaux2020-01-141-0/+52
| |
| * shrx_shr_3David Monniaux2020-01-141-0/+54
| |
* | store_store_otherDavid Monniaux2019-12-131-1/+84
| |
* | swap writes in memoryDavid Monniaux2019-12-131-0/+43
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-1/+18
|\ \
| * | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-3/+22
| |\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * | Ibuiltin proofCyril SIX2019-10-041-1/+18
| | |
* | | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-202-3/+22
|\ \ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| * \ \ Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-202-3/+22
| |\ \ \ | | |/ / | |/| / | | |/ mppa-work-upstream-merge
| | * 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".
* | | | ONE "admitted" and things compileDavid Monniaux2019-09-061-0/+4
| | | |
* | | | more proofs going throughDavid Monniaux2019-09-052-0/+4
| | | |
* | | | moved trapping_mode to a more appropriate placeDavid Monniaux2019-09-031-0/+9
|/ / /
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-283-7/+29
|\| | | | | | | | | | | mppa-work-upstream-merge
| * | 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".
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-193-8/+647
|\| | | | | | | mppa-work-upstream-merge
| * 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.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-039-38/+338
|\ \ | | | | | | | | | mppa-if-conversion
| * | Additional simulation diagrams for determinate source languagesXavier Leroy2019-05-311-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".
* | moved operators to specific file instead of common fileDavid Monniaux2019-04-271-55/+0
| |
* | added code for extfzl/extfsl (not very useful since bitfields are limited to ↵David Monniaux2019-04-251-2/+2
| | | | | | | | 32 bits)
* | start of extfzl/extfslDavid Monniaux2019-04-251-0/+27
| |
* | progressDavid Monniaux2019-04-251-0/+14
| |
* | IT COMPILESDavid Monniaux2019-04-251-5/+5
| |
* | begin bitfieldsDavid Monniaux2019-04-241-0/+15
| |
* | fix for jump tablesv3.5_k1c_1.0David Monniaux2019-03-301-4/+1
| |
* | FIXME: Jumptables have linking issues.David Monniaux2019-03-291-0/+4
| |
* | begin jumptables (does not work)David Monniaux2019-03-211-5/+0
| |
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-41/+53
|\| | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * 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`.
* | Disable the generation of jump tables until issues are fixedDavid Monniaux2019-02-021-1/+6
|/
* 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.
* | Remove coq warnings (#28)Bernhard Schommer2017-09-229-131/+131
|/ | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
generated by cgit (git 2.34.1) at 2024-07-07 07:41:00 +0000