aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* 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.
* | bug 20956, print correct error message depending on architectureMichael Schmidt2017-05-031-2/+8
|/
* More asserts.Bernhard Schommer2017-05-031-1/+1
|
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-03107-1436/+3975
| | | | | | | | | | | | | 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.
* Tunnelingproof: Remove assumption destroyed_by_cond c = nil.Xavier Leroy2017-05-021-66/+210
| | | | Since commit e5b37a6 (useless conditional branch elimination), the proof of the Tunneling pass was assuming forall c, destroyed_by_cond c = nil. This is not true for architecture variants that we will support soon. This commit rewrites the proof so as to remove this assumption. The old proof was by memory and value equalities, the new one is by memory extensions and "lessdef" values.
* RISC-V vararg.S: a "sw" instruction should be "sptr"Xavier Leroy2017-04-291-1/+1
|
* Update Changelog with recent changesXavier Leroy2017-04-281-1/+7
|
generated by cgit (git 2.34.1) at 2024-07-03 01:01:30 +0000