aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workv3.6_mppa_2019-09-20David Monniaux2019-09-2086-300/+16263
|\ | | | | | | merge with v3.6
| * fix compiling for aarch64David Monniaux2019-09-204-4/+42
| |
| * fix compilingDavid Monniaux2019-09-204-3/+8
| |
| * extraction problemsDavid Monniaux2019-09-202-2/+2
| |
| * Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-2082-298/+16217
| |\ | | | | | | | | | mppa-work-upstream-merge
| | * Update for release 3.6v3.6Xavier Leroy2019-09-171-2/+3
| | |
| | * Revise the "bench" entries of the test suiteXavier Leroy2019-09-175-12/+110
| | | | | | | | | | | | | | | | | | | | | | | | Initially, the "bench" entries of the test suite used a "xtime" utility developed in-house and not publically available. This commit adds a version of "xtime" written in OCaml (tools/xtime.ml) and updates the "bench" entries of the test/*/Makefile to use it.
| | * Updates in preparation for release 3.6Xavier Leroy2019-09-162-1/+63
| | |
| | * -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The temporary variables introduced by SimplLocals reuse the same integer identifiers as the local variables they come from. This commit ensures that these variables are printed as "$var", where "var" is the original variable name, instead of "$NNN" as before. The "$NNN" form is retained for temporary variables that do not correspond to a source-level local variable, such as the temporary variables introduced by SimplExpr. This commit should make no difference for "ccomp -dclight", because the Clight that is printed is the Clight version 1 produced by SimplExpr, where every temporary is fresh and does not correspond to a source-level local variable. This commit does change the output of "clightgen -dclight", because the Clight that is printed is the Clight version 2 produced by SimplLocals. The printed Clight is much more legible thanks to the more meaningful temporary variable names.
| | * clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-163-16/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Clight output of clightgen is Clight version 2, after SimplLocals conversion, where function parameters are temporary variables, not variables. This commit makes sure the function parameters are printed as temporary variables and not as variables. In passing, it generalizes the Clight pretty-printer so that it can print both Clight version 1 and Clight version 2. Closes: #314
| | * Reworked json export.Bernhard Schommer2019-09-125-78/+91
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The json export prints formatted json, which takes a lot of additional time, however the result is only consumed by other tools and not meant for human reading. This commit implements several small changes in order to speedup the json export: * Removal of usage of the Format Module * Replacing `fprintf` calls by calls to function that print directly, such as `output_string`, etc. * Replacing list of all instruction names by a set of all instructions
| | * Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
| | | | | | | | | | | | "omega" fails in Coq 8.7, but not in 8.8 and later.
| | * Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-1163-167/+15898
| | |\ | | | | | | | | | | | | Support target architecture AArch64 (ARMv8 in 64-bit mode)
| | | * AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.leroy2019-08-312-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The argument is of type Tlong, not Tint. This caused spurious errors in RTLtyping. Also: in AArch64/PrintOp.ml, print Cmaskl{zero,notzero} with "&l" to distinguish them from Cmask{zero,notzero}.
| | | * Offset out of range for ldp/stp instructionsxavier.leroy2019-08-231-1/+3
| | | | | | | | | | | | | | | | These instructions are generated by __builtin_memcpy.
| | | * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-176-16/+16
| | | | | | | | | | | | Some changes were not correctly propagated to all architectures.
| | | * Test for the compilation of floating-point literalsXavier Leroy2019-08-083-1/+562
| | | | | | | | | | | | | | | | With special emphasis on the use of the AArch64 fmov #imm instruction.
| | | * AArch64 portXavier Leroy2019-08-0848-87/+14874
| | | | | | | | | | | | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
| | | * Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
| | | |
| | | * Factor out endianness determination between testsXavier Leroy2019-08-074-30/+14
| | | |
| | | * ndfun: add support for guards on patternsXavier Leroy2019-08-071-5/+16
| | | | | | | | | | | | | | | | | | | | | | | | Syntax is "pat ?? bexpr => action". The whole case is selected only when "pat" matches and then "bexpr" evaluates to "true".
| | | * More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
| | | |
| | | * Errors: fixed a loop in tactic MonadInvXavier Leroy2019-08-071-1/+1
| | | |
| | | * Asmgenproof0: add predicate exec_straight0Xavier Leroy2019-08-071-0/+26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a variant of exec_straight where it is allowed to take zero steps. In other words, exec_straight0 is the "star" relation, while exec_straight is the "plus" relation. In the end we need "plus" relations in simulation diagrams, to show the absence of stuttering. But the "star" relation exec_straight0 is useful to reason about code fragments that are always preceded or followed by at least one instruction.
| | | * Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
| | | |
| | | * Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
| | | | | | | | | | | | | | | | Should simplify reasoning over Boolean equalities.
| | | * Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
| | | |
| | | * Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
| | | | | | | | | | | | | | | | Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
| | | * Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
| | | |
| | | * x86: wrong expansion of __builtin_fmadd et alXavier Leroy2019-08-071-13/+19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a misunderstanding on the asm syntax for 3-operand instructions such as vfmadd132: when the Intel manual reads vfmadd132 res, arg2, arg3 the corresponding GNU asm syntax is vfmadd132 arg3, arg2, res but not vfmadd132 arg2, arg3, res Closes: #188
| | | * Add support for Coq 8.10Xavier Leroy2019-08-071-2/+2
| | | |
| | | * Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-071-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.
| | | * Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
| | | |
| | | * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-078-23/+22
| | | | | | | | | | | | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
| | | * Simplify invocation of Emacs + Proof GeneralXavier Leroy2019-08-071-17/+3
| | | | | | | | | | | | | | | | PG now uses the _Coqproject file and finds relevant paths there.
* | | | More work on test, regression/packedstruct1.c and regression/varargs2.c ↵Cyril SIX2019-09-204-24/+33
| | | | | | | | | | | | | | | | don't pass
* | | | Adding SIMU=k1-cluster -- in configureCyril SIX2019-09-201-0/+1
|/ / /
* | | __builtin_bswap16, 32 and 64Cyril SIX2019-09-204-39/+38
| | |
* | | Fixing machine description (error in wchar signedness + trying different ↵Cyril SIX2019-09-191-5/+32
| | | | | | | | | | | | value for passing structs)
* | | Desactivating CompCert tests taking too longCyril SIX2019-09-191-1/+3
| | |
* | | Adding some function calls in interop testsCyril SIX2019-09-192-7/+15
| | |
* | | Detailing oracle/vérificateur in the timingsCyril SIX2019-09-182-2/+3
| | |
* | | Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-184-7/+10
| | |
* | | Compatibility fix for Coq 8.7.1Cyril SIX2019-09-131-3/+3
| | |
* | | Adding back "exit 2" to the test target of test/c/MakefileCyril SIX2019-09-131-2/+2
| | |
* | | Scaling down compression testsCyril SIX2019-09-131-5/+11
| | |
* | | Reducing further the input size of the testsCyril SIX2019-09-1330-71/+68
| | |
* | | Scaling down most of c/ CompCert testsCyril SIX2019-09-1318-37/+56
| | |
* | | Merge branch 'mppa-work' of ↵David Monniaux2019-09-1025-107/+559
|\ \ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | | Starting to modify official CompCert tests to be passable with the simuCyril SIX2019-09-1018-89/+81
| | | |
generated by cgit (git 2.34.1) at 2024-06-03 01:50:42 +0000