aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
...
* | | | 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.
* Constprop strength reduction (#17)Bernhard Schommer2017-07-121-0/+21
| | | | | | | PowerPC port: add strength reduction for 64-bit operations * Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748) * Moved shru_rolml proof to Values.
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-063-15/+20
| | | | | | This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses. Current status: x86 port only, the only new addressing mode handled is reg + offset.
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-039-271/+320
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-132-4/+4
| | | | | This silences a warning of Coq 8.6. Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
* Use "Local" as prefixXavier Leroy2017-02-132-12/+10
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Revised elaboration of attributesXavier Leroy2017-01-312-3/+2
| | | | | | | | | | | | | | | | | | | | | The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-18/+0
|
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+12
| | | | | | This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+100
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-019-401/+1004
| | | | | | | | | | | - 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.
* Implement support for big endian arm targets.Bernhard Schommer2016-08-051-3/+4
| | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-081-1/+1
| | | | | | | | | | | | | | Here are two examples that cause an internal error in Asmexpand.ml: volatile long long x; void f(unsigned int i) { x = i; } unsigned g(unsigned i) { return __builtin_clzll(i); } The argument "i" to builtin volatile store or __builtin_clzll is turned into a BA_splitlong(BA_int 0, BA <variable i>), which Asmexpand.ml doesn't know how to handle. The fix (in AST.builtin_arg_ok) is to prevent this 'optimization' for all builtins except those of the "OK_all" kind, i.e. __builtin_annot. Regression tests were added and tested on IA32. Need to retest on ARM and PowerPC.
* Port to Coq 8.5pl2Xavier Leroy2016-07-084-33/+32
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* common/Determinism.v: dual-license with GPLXavier Leroy2016-06-301-0/+3
| | | | There was no good reason why Determinism.v was the only file in common/ that was not dual-licensed (GPL + noncommercial). Plus, it simplifies the wording of the LICENSE file.
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-222-7/+126
| | | | As suggested by Lennart Beringer, this commits strengthens memory injections and extensions so as to guarantee that the permissions of existing memory locations are not increased by the injection/extension. The only increase of permissions permitted is empty locations in the source memory state of the injection/extension being mapped to nonempty locations.
generated by cgit (git 2.34.1) at 2024-07-06 17:57:44 +0000