aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-122-3/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-4/+4
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-176-93/+145
| | | | | | | | | | | | | | | | | | | * Outgoing stack slots are set to Vundef on return from a function call, modeling the fact that the callee could write into those stack slots. (CompCert-generated code does not do this, but code generated by other compilers sometimes does.) * Adapt Stackingproof to this new semantics. This requires tighter reasoning on how Linear's locsets are related at call points and at return points. * Most of this reasoning was moved from Stackingproof to Lineartyping, because it can be expressed purely in terms of the Linear semantics, and tracked through the wt_state predicate. * Factor out and into Conventions.v: the notion of callee-save locations, the "agree_callee_save" predicate, and useful lemmas on Locmap.setpair. Now the same "agree_callee_save" predicate is used in Allocproof and in Stackingproof.
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-018-8/+79
| | | | | | | | | | The semantics of external function calls in LTL, Linear, Mach and Asm now consider that all caller-save registers are set to Vundef by the call. This models that fact that the external function can modify those registers arbitrarily. Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes accordingly.
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
| | | | | | | This should avoid cluttering the assembler output with .ascii "\n" lines if the annotation ends with a string and make for a better readability. Bug 23169
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
| | | | | | It seems necessary that the mulitplication for the high part of split registers is put into brackets. Bug 23169
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-121-3/+1
| | | | | | This will soon be deprecated by Coq. Manual merge of pull request #224 by vbgl. Closes: #224
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
|
* Do not use default printer for variable names.Bernhard Schommer2018-03-091-2/+8
| | | | | | Printing variable names with the default expression printer results in newlines in the outputed error message. Bug 23169
* Perform quoting for json.Bernhard Schommer2018-03-081-1/+8
| | | | | | The strings for json need quoting of special characters such as \" and \\. Bug 22438
* Print symbols as symbols.Bernhard Schommer2018-03-082-4/+26
| | | | | | This allows us to replacing them by their address in valex and additionally checking them. Bug 22438
* Improve error messages.Bernhard Schommer2018-03-071-16/+14
| | | | | | | | Include the format specifier in error message when available in order to make it easier to spot the broken ais parameter. Futhermore introduce a new warning for unused ais parameters. Bug 22464
* Reword error message. Fix 22464Bernhard Schommer2018-03-071-2/+2
|
* Improve wording.Bernhard Schommer2018-03-071-1/+1
| | | | | Mention that it is a global memory cell. Fix 22464
* Improve and simplify error messages.Bernhard Schommer2018-03-072-31/+54
| | | | | | | | The checks on the argument and format arguments are now performed during C2C translation by calling the validate_ais_annotations function and result in an error instead of a warning in the backend to be more consistent with the rest of the builtin functions.
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-064-22/+204
| | | | | | | | | | | | | | | | | | The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-1/+33
|
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-053-0/+249
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2
| | | The lemma is now in lib/Coqlib.v.
* Introduce and use C2C.atom_inline function with 3-valued resultXavier Leroy2017-12-081-3/+6
| | | | | | Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single C2C.atom_inline function that returns one of the three possible values stored in the the a_inline field.
* Remove unused code. BUg 22642Bernhard Schommer2017-12-081-2/+2
|
* Store the different inlining cases.Bernhard Schommer2017-12-081-2/+2
| | | | | | | In order to correctly support the noinline attribute we must store whether the function was specified with an inline specifer, had a noinline attribute or nothing. Bug 22642
* Do not inline varag functions. Bug 22642Bernhard Schommer2017-12-071-3/+3
|
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-073-12/+93
| | | | | | | | | New inlining heuristic for static functions. Static functions that are only called once can always be inlined, since they can be removed safely after inlining and no call prologue, epilogue, as well as register saving and needs to be generated.
* Issue #208: make value analysis of comparisons more conservative w.r.t. ↵Xavier Leroy2017-11-241-8/+12
| | | | | | | pointers (#209) Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior in CompCert but their status in ISO C is unclear and they may occur in real-world code. Make sure they are statically analyzed as Btop.
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-102-2/+0
|
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-1/+0
|
* Use address for printing address constant. Bug 22525Bernhard Schommer2017-11-091-2/+3
|
* Generalize print_init.Bernhard Schommer2017-11-091-1/+40
| | | | | | The powerpc version of print_init can be used without problems for all backends. Bug 22525
* Fix jumptable issue.Bernhard Schommer2017-11-081-2/+5
| | | | | | Instead of using reset_constants use reset_literals which avoids emptying the jumptables. Bug 22525
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-081-6/+21
| | | | | | Instead of just storing the constants in a list, they are now stored in a hashtable. This avoids printing of duplicates. Bug 22525
* Remove superfluous function.Bernhard Schommer2017-11-062-3/+2
| | | | | The new_label function is alway equal to PrintAsmaux.new_label. Bug 22472
* Also quote \a.Bernhard Schommer2017-10-261-0/+2
| | | | | | This allows for an easier replacement of the binary address and avoids that the user specifies his own binary addresses. Bug 22468
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-205-0/+5
|\ | | | | | | Ensure FunInd or Recdef is imported if functional induction is used. This is necessary for Coq 8.7.0.
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-205-0/+5
| | | | | | | | | | | | Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-197-9/+37
| | | | | | | | | | | | | | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* | Distinguish between long and int for cases.Bernhard Schommer2017-10-131-7/+7
| |
* | Remove coq warnings (#28)Bernhard Schommer2017-09-2225-179/+179
| | | | | | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* | Deadcode: eliminate trivial Icond instructionsXavier Leroy2017-09-182-2/+9
| | | | | | | | | | | | These are conditionals where the "ifso" and the "ifnot" successors are the same. By eliminating them here and not later, we can also eliminate the instructions that compute the arguments to the condition, if any. There is another, later point where these trivial conditional instructions are eliminated: in the Tunneling phase. The elimination done in Tunneling is more powerful in that it works not just for conditionals whose two successors are the same, but also for conditionals whose two successors lead to the same point after a series of nops. The elimination done in Deadcode is more powerful in that it eliminates the instructions that compute the arguments to the condition. Hence it is worth having both eliminations.
* | Prefixed runtime functions.Bernhard Schommer2017-08-252-45/+45
| | | | | | | | | | | | | | The runtime functions are prefixed with compcert in order to avoid potential clashes with runtime/builtin functions of other compilers. Bug 22062
* | Asmgenproof0: some more useful lemmasXavier Leroy2017-08-171-0/+29
| | | | | | | | Next commit uses those lemmas in the ARM port.
* | 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.
generated by cgit (git 2.34.1) at 2024-06-29 23:16:01 +0000