aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Print_annot should produce a string.Bernhard Schommer2017-07-191-26/+25
|
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+2
| | | | | | | | - 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-0618-10/+95
| | | | | | 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.
* 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.
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-0327-342/+711
| | | | | | | | | | | | | 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 port and assorted changesXavier Leroy2017-04-284-43/+117
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Modest optimization of leaf functionsXavier Leroy2017-04-281-2/+75
| | | | | | | | | | Leaf functions are functions that do not call any other function. For leaf functions, it is not necessary to save the LR register on function entry nor to reload LR on function return, since LR contains the correct return address throughout the function's execution. This commit suppresses the reloading of LR before returning from a leaf function. LR is still saved on the stack on function entry, because doing otherwise would require extensive changes in the Stacking pass of CompCert. However, preliminary experiments indicate that we get good speedups by avoiding to reload LR, while avoiding to save LR makes little difference in speed. To support this optimization and its proof: - Mach is extended with a `is_leaf_function` Boolean function and a `wf_state` predicate to provide the semantic characterization. - Asmgenproof* is extended with a `important_preg` Boolean function that means "data register or LR". A number of lemmas that used to show preservation of data registers now show preservation of LR as well.
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-071-1/+3
| | | | | | | | | ISO C99 states that "inline defintions", functions with inline specifier that are not extern, does not provide an external definition and another compilation unit can contain an external definition. Thus in the case of non-static inline functions no code should be generated. Bug 21343
* Add optimization option finline.Bernhard Schommer2017-04-071-1/+1
| | | | | | The new option f(no-)inline controlls whether inlining is active or not. Bug 21343.
* Another optimization of empty if/else and other useless conditional branchesXavier Leroy2017-04-062-31/+41
| | | | | | | | | | This commit eliminates useless conditional branches during the branch tunneling pass over LTL. Conditional branches where both successors go to the same LTL node are turned into unconditional branches, which will stay or be eliminated by the subsequent Linear pass. One code pattern that triggers this optimization is an empty if/else at the C source level. Commit 4d7a459 eliminates these empty if/else statements early, during the Compcert C -> Clight translation. I think it's good to have both optimizations: - Early elimination makes sure these empty if/else cause no overhead whatsoever, and in particular cannot degrade the precision of later static analyses. - Late elimination catches the case where a nonempty if/else in the source becomes empty as a consequence of optimizations. Future work? If the optimization in Tunneling triggers, it might be worth re-running the Tunneling pass once more, to make sure that the "Lgoto" introduced by the optimization is properly tunneled / skipped over when appropriate.
* use 'f' as generic function-identifier instead of arbitraty identifier 1 for ↵Michael Schmidt2017-03-231-1/+1
| | | | alloctrace debug-output
* Removed CMinor import. Bug 20992Bernhard Schommer2017-02-145-1298/+0
|
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-3/+5
| | | | Without scopes Coq 8.6 warns, probably rightly so.
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-131-2/+2
| | | | | This silences a warning of Coq 8.6. Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
* Use "Local" as prefixXavier Leroy2017-02-135-6/+6
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into ↵Xavier Leroy2017-02-134-6/+7
|\ | | | | | | maximedenes-coq-8.6
| * Fix broken fragile automation.Maxime Dénès2017-01-091-1/+2
| |
| * Subst's behavior on let-ins has changed.Maxime Dénès2017-01-091-2/+2
| |
| * The subst tactic has become more powerful.Maxime Dénès2017-01-092-3/+3
| |
* | Inlined open of ErrorsBernhard Schommer2017-02-061-10/+9
| |
* | Datatypes no longer shadows fst and sndBernhard Schommer2017-02-061-1/+1
| |
* | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
| | | | | | | | | | Locations are only used in two functions and can be referenced there directly.
* | Remove open Locations.Bernhard Schommer2017-02-061-6/+5
| | | | | | | | The Locations are only used in one function.
* | Remove unused openBernhard Schommer2017-02-061-1/+0
|/
* Use 64 bit address in debug information.Bernhard Schommer2016-11-102-0/+2
| | | | | Address constants need to be 64bit also in the debug information. Bug 20335
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-6/+6
| | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
* SplitLong: propagate constants through "longofint"Xavier Leroy2016-10-252-4/+8
| | | | | This can make a big difference in which optimizations are triggered later. Constants were already propagated by "longofintu".
* Update ARM port. Not tested yet.Xavier Leroy2016-10-253-7/+8
|
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-046-17/+337
| | | | | | This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+1
|
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-027-132/+256
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-0138-1197/+1624
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-211-4/+4
|\ | | | | | | | | | | Fix minor issues in some proofs and tactics. Patch by Maxime Dénès.
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-211-4/+4
| | | | | | | | | | These minor problems were revealed by porting CompCert to Coq 8.6, where they trigger errors.
* | Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+4
| | | | | | | | | | | | Avoids problems with overwritting the registe containing the function address. Bug 19779
* | Removed some implict arguments.Bernhard Schommer2016-09-051-15/+6
| | | | | | | | Also changed Local Open to Open Local.
* | Merge pull request #118 from AbsInt/armebXavier Leroy2016-08-241-4/+7
|\ \ | | | | | | Support for ARM Big Endian
| * | Implement support for big endian arm targets.Bernhard Schommer2016-08-051-4/+7
| |/ | | | | | | | | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* / PR#113, PR#122: Unspillable temporaries causing register allocation to failXavier Leroy2016-08-241-1/+6
|/ | | | | | The spilling strategy for 2-address operations was strange in the case where the first argument needs spilling but not (yet) the result: a Xreload instruction was generated which prevented future spilling of the result. Fixed by generating Xmove instead of Xreload in this case.
* Merge pull request #105 from m-schmidt/masterXavier Leroy2016-07-112-0/+5
|\ | | | | Fix parsing and handling of CMinor files
| * add 'runtime' token to lexerMichael Schmidt2016-07-011-0/+1
| |
| * extend cminor parser to accept "extern runtime" declarationsMichael Schmidt2016-07-011-0/+4
| |
* | Port to Coq 8.5pl2Xavier Leroy2016-07-086-39/+36
|/ | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-281-3/+3
| | | | | | The configuration advanced debug is removed and now full debug information is also generated for ia32 and arm. Bug 17609
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-223-2/+28
| | | | As suggested by Lennart Beringer, this commits strengthens memory injections and extensions so as to guarantee that the permissions of existing memory locations are not increased by the injection/extension. The only increase of permissions permitted is empty locations in the source memory state of the injection/extension being mapped to nonempty locations.
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-222-35/+63
| | | | | | | | - Values: "rol" and "ror" are defined even if their second argument is not in the [0,31] range (for consistency with "rolm" and because the semantics is definitely well defined in this case). - NeedDomain: more precise analysis of "rol" and "rolm", could benefit the PowerPC port.
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-1718-379/+438
| | | | | | | | | | | | | This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations. In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves. Summary of changes: - AST: introduce the type "rpair A" of register pairs - Conventions1, Conventions: use it when describing calling conventions - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls - Events: suppress external_call', no longer useful - All passes from Allocation to Asmgen: adapt accordingly.
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of ↵Xavier Leroy2016-05-071-111/+61
| | | | | | | | memory blocks Trees are slightly more efficient than Maps, and avoid maintaining the invariant on the default value. lib/Maps: add a generic construction of a (partial) Tree module from an indexed type; use it to define ZTrees (trees indexed by Z integers).
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-279-1974/+1344
| | | | | | | | | | | | | | | | | | | architectures The original Stacking pass and its proof hard-wire assumptions about the processor and the register allocation, namely that integer registers are 32 bit wide and that all stack slots have natural alignment 4, which precludes having stack slots of type Tlong. Those assumptions become false if the target processor has 64-bit integer registers. This commit makes minimal adjustments to the Stacking pass so as to lift these assumptions: - Stack slots of type Tlong (or more generally of natural alignment 8) are supported. For slots produced by register allocation, the alignment is validated a posteriori in Lineartyping. For slots produced by the calling conventions, alignment is proved as part of the "loc_argument_acceptable" property in Conventions1. - The code generated by Stacking to save and restore used callee-save registers no longer assumes 32-bit integer registers. Actually, it supports any combination of sizes for registers. - To support the new save/restore code, Bounds was changed to record the set of all callee-save registers used, rather than just the max index of callee-save registers used. On CompCert's current 32-bit target architectures, the new Stacking pass should generate pretty much the same code as the old one, modulo minor differences in the layout of the stack frame. (E.g. padding could be introduced at different places.) The bulk of this big commit is related to the proof of the Stacking phase. The old proof strategy was painful and not obviously adaptable to the new Stacking phase, so I rewrote Stackingproof entirely, using an approach inspired by separation logic. The new library common/Separation.v defines assertions about memory states that can be composed using a separating conjunction, just like pre- and post-conditions in separation logic. Those assertions are used in Stackingproof to describe the contents of the stack frames during the execution of the generated Mach code, and relate them with the Linear location maps. As a further simplification, the callee-save/caller-save distinction is now defined in Conventions1 by a function is_callee_save: mreg -> bool, instead of lists of registers of either kind as before. This eliminates many boring classification lemmas from Conventions1. LTL and Lineartyping were adapted accordingly. Finally, this commit introduces a new library called Decidableplus to prove some propositions by reflection as Boolean computations. It is used to further simplify the proofs in Conventions1.
generated by cgit (git 2.34.1) at 2024-06-30 23:14:26 +0000