aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
...
| * 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.
* | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-123-15/+75
|\ \
| * | fix reverse printing problem for hashesDavid Monniaux2020-04-111-1/+8
| | |
| * | print hashesDavid Monniaux2020-04-082-3/+4
| | |
| * | begin installing profilingDavid Monniaux2020-04-083-7/+8
| | |
| * | added EF_profilingDavid Monniaux2020-04-083-14/+65
| | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-085-37/+108
|\| |
| * | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-012-10/+23
| |\|
| | * 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.
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-033-27/+85
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | CSE2 alias analysis for Risc-VDavid Monniaux2020-03-031-0/+7
| | | |
| | * | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-029-106/+249
| | |\|
| | | * 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.
| | * | loadv_storev_sameDavid Monniaux2020-03-021-0/+18
| | | |
| * | | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-035-2/+269
| |\ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
* | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-259-80/+189
|\ \ \ \
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-249-80/+189
| |\| | | | | |/ / | |/| | | | | | mppa-work-upstream-merge
| | * | 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.
* | / thread local declarations now workDavid Monniaux2020-02-242-9/+17
|/ /
* | 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.
generated by cgit (git 2.34.1) at 2024-05-20 04:50:23 +0000