aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
* Add missing tab character, bug 23541Michael Schmidt2018-05-021-1/+1
|
* Add new powerpc builtins.Michael Schmidt2018-04-275-4/+44
| | | | | | New builtin for 64-bit load/store with byte reversal and 64-bit mul-high. Bug 23541
* Print symbols as symbols.Bernhard Schommer2018-03-081-16/+19
| | | | | | This allows us to replacing them by their address in valex and additionally checking them. Bug 22438
* Use binary output.Bernhard Schommer2018-03-071-1/+1
| | | | | | This should avoid problems when newlines are used in string constants etc. Bug 23172
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-061-9/+10
| | | | | | | | | | | | | | | | | | 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.
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-162-6/+55
| | | | | | | | | | | | | | | | | | | When x is known to be either 0 or 1, comparisons such as x == 0 x != 0 x == 1 x != 1 can be optimized away. This optimization was already performed for signed comparisons. This commit extends the optimization to unsigned comparisons as well. Additionally, for PowerPC only, some unsigned (dis)equality comparisons are turned into signed comparisons when we know it makes no difference, i.e. when both arguments are guaranteed not to be pointers. The reason is that Asmgen can produce shorter instruction sequences for some signed equality comparisons than for the corresponding unsigned comparisons. It's important to optimize unsigned integer comparisons because casts to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons. In particular, cascades of casts to _Bool are now reduced to a single cast much more often than before.
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-1/+1
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-5/+17
|
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
| | | | | | | | | | | 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/
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-052-6/+13
| | | | Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
* New json printing interface.Bernhard Schommer2017-11-141-143/+18
| | | | | The common json export functionallity is moved into an own File. Bug 22472
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-101-2/+0
|
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-30/+0
|
* Fix jumptable issue.Bernhard Schommer2017-11-081-1/+1
| | | | | | Instead of using reset_constants use reset_literals which avoids emptying the jumptables. Bug 22525
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-081-20/+14
| | | | | | 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-061-2/+0
| | | | | The new_label function is alway equal to PrintAsmaux.new_label. Bug 22472
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-0/+1
|\ | | | | | | 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-201-0/+1
| | | | | | | | | | | | 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-194-13/+29
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Make the list unique. Bug 22239Bernhard Schommer2017-09-261-177/+22
| |
* | Moved common buitlins to C2C gernic_builtins.Bernhard Schommer2017-09-261-8/+0
| |
* | Added dump-mnemonics option.Bernhard Schommer2017-09-252-0/+186
| | | | | | | | | | | | This option allows it to dump a list of all used mnemonics into a file. Bug 22239
* | Remove coq warnings (#28)Bernhard Schommer2017-09-225-23/+23
| | | | | | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* | Disallow usage of default pattern for AsmToJSON.Bernhard Schommer2017-09-221-2/+11
| | | | | | | | | | | | | | In order to ensure that no new instruction is added without adding it to the Json export we enforce warning 4 for the instruction printer and removed all default pattern matchings. Bug 22239
* | Fixed typo.Bernhard Schommer2017-08-241-1/+1
| |
* | Added annot to json dump.Bernhard Schommer2017-07-241-3/+20
| |
* | Print_annot should produce a string.Bernhard Schommer2017-07-191-5/+5
|/
* Constprop strength reduction (#17)Bernhard Schommer2017-07-123-16/+304
| | | | | | | 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.
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-065-87/+179
| | | | | | | | - 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
* Issue #16P: wrong rlwinm instruction generated by constant propagationXavier Leroy2017-07-052-11/+26
| | | | This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
* Adopted section names in AsmToJson.Bernhard Schommer2017-06-291-10/+23
|
* Formatted json printing.Bernhard Schommer2017-06-282-315/+307
| | | | | | | | | 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 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
* Print 64bit constants for rldimn and rldimi.Bernhard Schommer2017-05-051-2/+2
|
* 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-0322-189/+2378
| | | | | | | | | | | | | 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.
* RISC-V port and assorted changesXavier Leroy2017-04-282-0/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 functions (continued)Xavier Leroy2017-04-283-159/+116
| | | | | | - Avoid reloading LR before a tail call if we're in a leaf function - Factor out the code that reloads LR if necessary (function Asmgen.transl_epilogue) - Factor out the corresponding parts of the proof (Asmgenproof1.transl_epilogue_correct, Asmgenproof.step_simulation)
* Modest optimization of leaf functionsXavier Leroy2017-04-283-44/+166
| | | | | | | | | | 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.
* Assert instead of unit.Bernhard Schommer2017-04-101-6/+6
| | | | | | Instructions expanded by Asmexpand should never end up in AsmToJSON. Bug 21345
* Filter out functions earlier. Bug 21343Bernhard Schommer2017-04-101-24/+27
|
* Fix name of function. Bug 21378Bernhard Schommer2017-04-071-1/+1
|
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-071-21/+23
| | | | | | | | | 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
* Replace 'decide equality' in powerpc/Op.v. Bug 21332Bernhard Schommer2017-04-031-4/+5
|
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-4/+6
| | | | Without scopes Coq 8.6 warns, probably rightly so.
* Use "Local" as prefixXavier Leroy2017-02-133-4/+4
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* ARM, PowerPC: update Asmgenproof for Coq 8.6Xavier Leroy2017-02-131-6/+13
|
* Remove unused openBernhard Schommer2017-02-061-1/+0
|
* Added warning for inline asm in sdump. Bug 20593Bernhard Schommer2016-12-141-1/+6
|
generated by cgit (git 2.34.1) at 2024-06-29 05:55:02 +0000