aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
...
* | Added interface for the Asmexpansion.Bernhard Schommer2016-03-161-4/+4
| | | | | | | | | | | | Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394
* | Change atom printer to use the common function.Bernhard Schommer2016-03-161-1/+1
| | | | | | | | | | | | The printer for atom constants should also use the printer for singleton objects. Bug 18394
* | Cleanup of AsmToJSON.Bernhard Schommer2016-03-163-126/+104
| | | | | | | | | | | | Removed unused code, factored out common functions and added an interface file. Bug 18394
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-153-40/+40
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-155-23/+25
| | | | | | | | This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
* | Removed unused parameter from is_small/rel_data.Bernhard Schommer2016-03-115-25/+23
| | | | | | | | | | | | The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394
* | Code cleanup.Bernhard Schommer2016-03-103-58/+49
|/ | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* Also print braces around the registers.Bernhard Schommer2016-02-041-2/+7
|
* Fixed missing \" in json printing for registers.Bernhard Schommer2016-02-041-2/+2
|
* Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-251-66/+70
|
* Started implementing a printer for Clflags.Bernhard Schommer2016-01-251-12/+5
|
* The return type of __builtin_clz() et al is "int", as documented and for GCC ↵v2.6Xavier Leroy2015-12-211-3/+3
| | | | compatibility, and not "unsigned int", as previously implemented.
* powerpc/Asmexpand: fix expansion of __builtin_clzllXavier Leroy2015-12-201-2/+2
| | | | The original code produces wrong results if res and al are the same register.
* bug 17752, fix semantics of builtin_set_spr64Michael Schmidt2015-12-161-1/+1
|
* bug 17752, fix tab-indentation in assembly outputMichael Schmidt2015-12-151-1/+1
|
* bug 17752, check target architecture for 64bit-builtinsMichael Schmidt2015-12-151-7/+13
|
* Print cfi_sections only if cfi is supported.Bernhard Schommer2015-12-151-3/+3
| | | | | | On older version of the binutils the cfi directives are not always supported so we only print cfi_sections if the corresponding .ini setting is set to true.
* bug 17752, add constant propagation for builtinsMichael Schmidt2015-12-151-1/+3
|
* bug 17752, rename builtin64_X to __builtin_X64Michael Schmidt2015-12-152-8/+8
|
* bug 17752, add builtin64_set_spr and builtin64_get_spr for PowerPCMichael Schmidt2015-12-153-3/+24
|
* Bug 17752, add rldicr instruction for PowerPCMichael Schmidt2015-12-153-2/+8
|
* bug 17752, add builtin_mr for PowerPCMichael Schmidt2015-12-141-1/+1
|
* bug 17752, add builtin_mr for PowerPCMichael Schmidt2015-12-143-6/+31
|
* bug 17752, add builtin_clzl and builtin_clzll for PowerPCMichael Schmidt2015-12-112-1/+16
|
* bug 17752, add builtin_nop for PowerPCMichael Schmidt2015-12-112-0/+0
|
* bug 17752, add builtin_nop for PowerPCMichael Schmidt2015-12-112-0/+6
|
* bug 17752, add builtin_uisel as unsigned version of builtin_iselMichael Schmidt2015-12-092-2/+5
|
* bug 17544, use json-printer function for mfcr instructionMichael Schmidt2015-11-091-3/+2
|
* Removed unused p_char_list function. Bug 17544.Bernhard Schommer2015-11-031-2/+0
|
* Changed the name of a few ppc instructions. Bug 17544Bernhard Schommer2015-11-031-3/+3
|
* Simplify the Json export.Bernhard Schommer2015-11-031-166/+183
| | | | | | Instead of having a function for each instruction we now use a generic function to print the arguments. Bug 17544.
* Few simple rewrite for the AsmToJSON printer.Bernhard Schommer2015-10-291-155/+147
| | | | | | In a first step all the print commands for the names are replaced by a more safe variant that avoids missing \". Bug 17328
* Another typo in AsmToJson.Bernhard Schommer2015-10-291-1/+1
| | | | Bug 17473
* Fixed some minor types in the asm printer.Bernhard Schommer2015-10-291-1/+1
| | | | Bug 17473
* Fixed typo in AsmToJson.Bernhard Schommer2015-10-261-1/+1
| | | | Bug 17473.
* Added special treatment for large stack size for ppc.Bernhard Schommer2015-10-231-3/+3
| | | | | | Since the stacksize is casted to signed int in the alloc frame function large stacksize lead to assembler containing overflows. Bug 17473.
* Added not merged destruction of Archi. Bug 17450Bernhard Schommer2015-10-201-0/+2
|
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-2014-33/+193
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/TargetPrinter.ml backend/CMparser.mly backend/SelectLongproof.v backend/Selectionproof.v cfrontend/C2C.ml checklink/Asm_printers.ml checklink/Check.ml checklink/Fuzz.ml common/AST.v debug/DebugInformation.ml debug/DebugInit.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli debug/Dwarfgen.ml exportclight/ExportClight.ml ia32/TargetPrinter.ml powerpc/Asm.v powerpc/SelectOpproof.v powerpc/TargetPrinter.ml
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-162-0/+3
| | | | | | | | | | | | | | | | | | | | The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392.
| * First step to implemente address ranges for the gnu backend.Bernhard Schommer2015-10-151-8/+1
| | | | | | | | | | | | | | | | | | In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392.
| * Reworked the section interface for the debug information.Bernhard Schommer2015-10-141-6/+7
| | | | | | | | | | | | Instead of pushing strings around use the actual section. However the string is still used in the Hashtbl. Bug 17392.
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1415-620/+620
| |
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-57/+57
| |
| * Changed the type of the debug sections with additional string.Bernhard Schommer2015-10-131-5/+11
| | | | | | | | | | | | | | | | Instead of using a string they now take an optional string, which should be none if the backend is not the diab backend and the corresponding section is the text section and Some s with s being the custom section name else. Bug 17392.
| * Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-132-2/+5
| | | | | | | | | | | | | | | | GCC prints all string larger than 3 characters in the debug_str section which reduces the size of the debug information since entries containing the same string now map to the same string in the debug_str sections. Bug 17392.
| * Fix minor typo introduced by refactoring of debug information.Bernhard Schommer2015-10-121-1/+1
| | | | | | | | | | The base register for the stack allocated variables should be r1 and not r2 under powerpc. Bug 17392
| * Merge branch 'master' into ppc64Xavier Leroy2015-10-115-107/+207
| |\ | | | | | | | | | Resolved conflicts in:configure powerpc/Asmexpand.ml
| * | Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-1314-14/+170
| | | | | | | | | | | | | | | | | | Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
* | | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2018-674/+674
| | |
* | | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-113-25/+14
| |/ |/| | | | | | | | | | | | | | | | | The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
generated by cgit (git 2.34.1) at 2024-07-02 19:26:16 +0000