aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Collapse)AuthorAgeFilesLines
* Revert "Startet implementation of new Debug interface."Bernhard Schommer2015-09-101-3/+2
| | | | This reverts commit 861292a6c5e58b4f78bef207c717b801b3fc1fed.
* Startet implementation of new Debug interface.Bernhard Schommer2015-09-061-2/+3
| | | | | | Added a new file debug/Debug.ml which will be the interface between for generating and printing the debuging information. Currently it contains only the code for the line directived.
* XBernhard Schommer2015-09-0610-280/+429
|\ | | | | | | Merge branch 'master' into debug_locations
| * Fixed typo in AsmToJSON for instruction Pstfdu.Bernhard Schommer2015-09-041-1/+1
| |
| * Added json printing of Pbctr.Bernhard Schommer2015-09-031-1/+1
| |
| * Fixed minor typo in printing of the Plbzx instruction in AsmToJSON.Bernhard Schommer2015-09-031-1/+1
| |
| * Fixed minor typo in AsmToJSON.Bernhard Schommer2015-09-031-1/+1
| |
| * Added builtin for mbar instruction.Bernhard Schommer2015-09-036-0/+15
| | | | | | | | This commit adds a builtin function for the mbar instruction.
| * New builtin for dcbz instruction.Bernhard Schommer2015-09-035-24/+33
| | | | | | | | | | | | This commit adds a builtin for the dcbz instructions. Additionally the dcbt,dcbtst,dcbtls and icbtls instruction are changed to their actually form all taking one additional register in Asm.v.
| * Added builtin for the icbtls instruction.Bernhard Schommer2015-09-026-0/+19
| | | | | | | | This commit adds a builtin for the icbtls instruction.
| * Allow only CT values of 0 and 2 in dcbtls instruction.Bernhard Schommer2015-09-022-4/+4
| | | | | | | | | | The dcbtls instruction allows only the values 0 and 2 according to the PPC Isa.
| * Print p_int_constant instead of p_int in AsmToJSON.Bernhard Schommer2015-09-021-5/+5
| |
| * Added builtin for dcbtlsBernhard Schommer2015-09-026-13/+63
| | | | | | | | | | | | THis commit adds a builtin function for the dcbtls instruction. Additionaly it changes the printing of the dcbt and dcbtst instruction to embedded mode and adds support for different address variants.
| * Added the gcc builtin prefetch.Bernhard Schommer2015-09-016-0/+25
| | | | | | | | | | | | This commit implements the gcc __builtin_prefetch in a form with all arguments for the powerpc architecture. The resulting instructions are the dcbt and dcbtst instructions in Server Category.
| * Improve error reporting in Asmexpand.Xavier Leroy2015-08-241-19/+32
| |
| * Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-224-33/+24
| | | | | | | | | | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
| * Adapt the PowerPC port to the new builtin representation.Xavier Leroy2015-08-2110-258/+285
| | | | | | | | | | | | | | __builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating.
* | Added symbol functions for printing of the location for global variables.Bernhard Schommer2015-08-211-0/+9
|/
* Added builtin for the dcbf instructionBernhard Schommer2015-08-175-0/+9
|
* Merge pull request #46 from AbsInt/asmexpandXavier Leroy2015-08-171-44/+11
|\ | | | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert
| * Merge branch 'master' into asmexpandBernhard Schommer2015-07-144-17/+419
| |\
| * | Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-261-44/+11
| | |
| * | Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"Bernhard Schommer2015-06-261-11/+44
| | | | | | | | | | | | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
| * | Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-261-44/+11
| |\ \
| | * | Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵Bernhard Schommer2015-06-101-44/+11
| | | | | | | | | | | | | | | | the same way as it is done for PPC.
* | | | Added builtin for the dcbi instruction.Bernhard Schommer2015-08-175-4/+11
| | | |
* | | | Added builitin for the icbi instruction.Bernhard Schommer2015-08-145-1/+11
| | | |
* | | | Added builtin for the lwsync barrier.Bernhard Schommer2015-08-145-3/+12
| | | |
* | | | Value analysis: keep track of pointer values that leak through small ↵Xavier Leroy2015-07-192-21/+21
| | | | | | | | | | | | | | | | | | | | | | | | integers with Uns or Sgn abstract values. This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
* | | | Value analysis: keep track of pointer values that leak through arithmetic ↵Xavier Leroy2015-07-191-2/+2
| |_|/ |/| | | | | | | | | | | | | | operations with undefined behaviors. Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
* | | Set/clear CR6 before calling an unprototyped function.Xavier Leroy2015-07-071-3/+4
| | | | | | | | | | | | | | | | | | A function declared without a prototype could be implemented by a vararg function (even though this is undefined behavior in C99). Be nice in this case.
* | | Use the functions from C2C to extract the information for the atoms. ↵Bernhard Schommer2015-07-061-17/+18
| | | | | | | | | | | | Simplified printing of storage class.
* | | Merge branch 'master' into json_exportBernhard Schommer2015-07-064-15/+54
|\ \ \ | | | | | | | | | | | | | | | | Conflicts: driver/Driver.ml
| * | | Corrected little typo in __builtin_clz function.Bernhard Schommer2015-07-063-5/+5
| | | |
| * | | Simple path for problems whith diab assembler in the case of functions in ↵Bernhard Schommer2015-07-031-9/+48
| |/ / | | | | | | | | | different sections.
* | | Print bit representation of floats.Bernhard Schommer2015-06-241-5/+6
| | |
* | | Fixed typo also in json export.Bernhard Schommer2015-06-221-1/+1
| | |
* | | Merge branch 'master' into json_exportBernhard Schommer2015-06-223-5/+5
|\| |
| * | Changed a minor typo: Pstwxu should be PstwuxBernhard Schommer2015-06-223-5/+5
| |/
* | Merged instructions that are printed as same instruction already in printer.Bernhard Schommer2015-05-291-26/+26
| |
* | Updated the printing of iniline asm and simplified some structures.Bernhard Schommer2015-05-181-136/+118
| |
* | Merge branch 'master' into json_exportBernhard Schommer2015-05-185-41/+65
|\|
| * Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-141-6/+6
| |
| * Updated PrintOp for the single-precision FP operations.Xavier Leroy2015-05-091-0/+8
| |
| * Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-093-35/+51
| | | | | | | | | | | | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* | Moved the information needed from the atoms to the ASM printer and removed ↵Bernhard Schommer2015-05-061-26/+48
| | | | | | | | unused information from the json dump.
* | Removed printing of information for internals and externals that should be ↵Bernhard Schommer2015-05-051-49/+28
| | | | | | | | folded away prior.
* | Merge branch 'master' into json_exportBernhard Schommer2015-05-051-35/+35
|\|
| * Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-301-35/+35
| | | | | | | | Val.lessdef, etc.
* | Added the first version of the sdump export to json.Bernhard Schommer2015-04-271-0/+377
|/
generated by cgit (git 2.34.1) at 2024-07-05 08:14:31 +0000