aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | 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.
* Issues with invalid x86 addressing modes (Github issue #183)Xavier Leroy2017-05-173-18/+27
| | | | | - x86/Op: in 32-bit mode all addressings are valid because offsets are always interpreted as 32-bit signed integers in Asmgen. - x86/ConstpropOp: in addr_strength_reduction, make sure no invalid addressing mode is generated.
* Make redefinition of composite a fatal error.Bernhard Schommer2017-05-091-2/+1
| | | | | | | The redefinition of a composite with a different tag type is now a fatal error. This should avoid problems when the composite is used. Bug 21542
* Print 64bit constants for rldimn and rldimi.Bernhard Schommer2017-05-051-2/+2
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-05-051-2/+4
|\
| * Bring RISC-V port up to dateXavier Leroy2017-05-051-2/+4
| | | | | | | | Commit 7873af3 introduced changes in the Conventions1.v interface. This commit implements those changes for RISC-V.
generated by cgit (git 2.34.1) at 2024-07-18 19:30:59 +0000