aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
* Reverted name for entry back to the old one.Bernhard Schommer2016-03-211-1/+1
| | | | | Valex expects Fun Section Literals and not Fun Section Literal. Bug 18394
* Merge branch 'master' into cleanupBernhard Schommer2016-03-213-61/+36
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-202-59/+34
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This pull request implements "approach A" to separate compilation in CompCert from the paper Lightweight verification of separate compilation by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis, POPL 2016, pages 178-190 In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program. This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
| | * Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-58/+33
| | |
| | * Add support for EF_runtime externalsXavier Leroy2016-03-061-1/+1
| | | | | | | | | | | | Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
| |/ | | | | | | | | | | As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always). Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing.
* | 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.
generated by cgit (git 2.34.1) at 2024-06-29 04:51:20 +0000