aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Update documentation index for release 3.1v3.1Xavier Leroy2017-08-181-23/+17
|
* Merge remote-tracking branch 'private/master'Xavier Leroy2017-08-188-91/+201
|\
| * Merge pull request #22 from AbsIntPrivate/arm_large_offsetsXavier Leroy2017-08-188-91/+201
| |\ | | | | | | Issue #P18: handle large offsets when accessing return address and back link in the stack frame
| | * ARM: tweak stack layout so that back link and return address are lowerXavier Leroy2017-08-171-37/+34
| | | | | | | | | | | | This reduces the chances that back link and return address cannot be saved by a single str instruction. We generate correct code for the overflow case, but the code isn't very efficient, so let's make it uncommon.
| | * ARM port: replace Psavelr pseudo-instruction by actual instructionsXavier Leroy2017-08-176-47/+88
| | | | | | | | | | | | | | | | | | Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12. R12 can be used as a temporary because it is marked as destroyed at function entry. We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed. In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.
| | * Asmgenproof0: some more useful lemmasXavier Leroy2017-08-171-0/+29
| | | | | | | | | | | | Next commit uses those lemmas in the ARM port.
| | * ARM: Generate Pcfi_rel_offset directives directly from AsmgenXavier Leroy2017-08-174-12/+17
| | | | | | | | | | | | This is what we do for PowerPC and is more resilient to changes in code generation. We need to give Pcfi_rel_offset a dynamic semantics, but that's just a no-op.
| | * Push correct registerMichael Schmidt2017-08-021-1/+1
| | |
| | * Improve stack offset addressingMichael Schmidt2017-08-025-35/+73
| | | | | | | | | | | | Functions which require large amounts of stack for spilling and/or arguments for function calls lead to stackframe offsets that exceed the 12bit limit of immediate constants in ARM instructions. This patch fixes the stack-offsets in the function prolog/epilog.
* | | configure: Wording and formatting of the Skylake/OCaml warningXavier Leroy2017-08-181-2/+3
| | |
* | | Update Changelog in preparation for release 3.1Xavier Leroy2017-08-181-2/+8
|/ /
* / Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-153-13/+34
|/ | | | | | The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196. The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-07-311-1/+3
|\
| * Mention rv32- and rv64- configurations in the help messageXavier Leroy2017-07-311-0/+2
| | | | | | | | These are the configurations for the new RISC-V port.
| * Accept Coq version 8.6.1 as supportedXavier Leroy2017-07-311-1/+1
| | | | | | | | 8.6.1 works just fine with the current CompCert.
* | Warning for Skylake/Kabylake systems.Bernhard Schommer2017-07-311-0/+4
|/
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-07-271-20/+27
|\
| * use TMPDIR also for asm-cfi testMichael Schmidt2017-07-271-5/+5
| |
| * generalize test for compiler optionsMichael Schmidt2017-07-271-15/+22
| |
* | Update Changelog with news since release 3.0.1Xavier Leroy2017-07-271-4/+29
|/
* Integrated fixup code in estimated size.Bernhard Schommer2017-07-261-0/+3
| | | | | | | 12 was a too small overaproximation for call which require fixup code for arguments and result. The new constant is 72, which consists of 4 for the branch instruction, 16 * 4 for the arguments and 4 for the result.
* Added annot to json dump.Bernhard Schommer2017-07-241-3/+20
|
* Print_annot should produce a string.Bernhard Schommer2017-07-195-40/+54
|
* No verbose debug info in default mode.Bernhard Schommer2017-07-141-5/+17
| | | | | | We don't need verbose debug for the assembler. The verbose debug information should only be printed if assembler files are generated.
* Update documentation entry point for release 3.0 (retroactively)Xavier Leroy2017-07-131-5/+8
| | | | Some modules new in 3.0 were not mentioned.
* Constprop strength reduction (#17)Bernhard Schommer2017-07-124-16/+325
| | | | | | | 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.
* SimlLocals.Sdebug_var: wrong type for 64-bit platformsXavier Leroy2017-07-091-1/+1
| | | | | | Fixes: Github issue #190. Tint was used instead of the correct Tptr.
* Add a -ignore-coq-version flag to configure (continued)Xavier Leroy2017-07-061-2/+2
| | | | These Coq people have version "numbers" that look nothing like numbers, such as "trunk". Also, they didn't test their pull request #188. Fixing this.
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-0618-99/+283
| | | | | | | | - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-0629-37/+211
| | | | | | 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.
* Issue #16P: wrong rlwinm instruction generated by constant propagationXavier Leroy2017-07-053-13/+30
| | | | This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-07-051-0/+30
|\
| * Merge pull request #14 from AbsIntPrivate/configure_no_pieMichael Schmidt2017-07-051-0/+30
| |\ | | | | | | Extension of configure for issue #189
| | * add check for -no-pie at configure-timeMichael Schmidt2017-07-041-0/+30
| |/
* | Add a -ignore-coq-version flag to configure (continued)Xavier Leroy2017-07-051-1/+1
| | | | | | | | Typo in configure help message.
* | Add a -ignore-coq-version flag to configureXavier Leroy2017-07-051-2/+10
|/ | | | | Pull request #188 from Maxime Dénès. This flag makes it easier for the Coq people to test CompCert with in-development versions of Coq.
* Adopted section names in AsmToJson.Bernhard Schommer2017-06-291-10/+23
|
* Revert "Update git ignore spec"Bernhard Schommer2017-06-281-1/+0
| | | | This reverts commit 414225093054f0fdd9222e0ba9fbb95d345f5457.
* Merge branch 'master' of /common/repositories/git/tools/compcertBernhard Schommer2017-06-281-0/+1
|\
| * Update git ignore specMarkus Pister2017-06-281-0/+1
| | | | | | | | | | | | ignore generated directory additional_files Bug 20000
* | Formatted json printing.Bernhard Schommer2017-06-289-353/+370
|/ | | | | | | | | Instead of just dumping the json output it is now a little bit formatted for better reading. Furthermore the AsmToJson function for the non powerpc targets now prints the json value "null" sucht that the resulting json file is valid json.
* Added a little bit more compilation info to sdump.Bernhard Schommer2017-06-263-4/+16
| | | | | | The additional compilation information contains the file, command line (after @-file expansion) and the current working directory. Bug 21690
* Added pseudo instruction for inline asm.Bernhard Schommer2017-06-201-0/+15
| | | | | | The inline assembler instructions are numbered with consecutives id's per compilation unit. Bug 21689
* Update Changelog for clightgenXavier Leroy2017-06-121-0/+1
|
* clightgen: add option -normalize to ensure that memory loads never occur ↵Xavier Leroy2017-06-122-2/+177
| | | | | | | | | | | | | | | | | | | | | "deep" inside expressions For example, with this option, tmp = *(x + 0) + *(x + 1) in the original Clight is rewritten to tmp1 = *(x + 0) tmp2 = *(x + 1) tmp = tmp1 + tmp2 with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads. Squashed commit of the following: commit 3fb69dae567b1305383b74ce1707945f91369a46 commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a commit c220ed303d9f3f36cc03c347a77b065a9362c0e7
* Merge pull request #185 from letouzey/no-BigNumPreludeXavier Leroy2017-06-071-1/+1
|\ | | | | Do not rely on the hints of BigNumPrelude
| * Alphabet.v compiles even without the hints of BigNumPreludePierre Letouzey2017-06-061-1/+1
|/ | | | | | | | BigNumPrelude will soon leave Coq stdlib with the rest of the bignum library (apart from Int31 files) to become a separate package. With this (very minor) patch, Compcert compiles with or without the hints declared in BigNumPrelude.
* Early optimization of redundant *& and &* addressingsXavier Leroy2017-05-293-8/+59
| | | | | | Particularly annoying was the `*&x` sequence where `x` is a local variable, which would force stack-allocation of `x` early, generating extra loads and stores that could not always be optimized later (in CSE and Deadcode). The `*&` sequences and, by symmetry, the `&*` sequences are now eliminated early during Clight generation, via smart constructors.
* Merge pull request #184 from letouzey/zify-fixXavier Leroy2017-05-271-1/+1
|\ | | | | Make proof script compatible with an improvement in the 'zify' tactic
| * Inliningspec made compatible with a coming fix of zifyletouzey2017-05-271-1/+1
|/ | | | See Coq pull request #673 (and original bug #5336). With the fixed version of zify, this proof could actually be shortened to `intros. unfold shiftpos. now zify.`, but the proposed patch has the advantage of being compatible with both the released versions of Coq, and the coming ones.
generated by cgit (git 2.34.1) at 2024-06-13 12:53:34 +0000