Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong. | Xavier Leroy | 2015-08-22 | 15 | -50/+55 |
| | | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small. | ||||
* | Simplify the handling of extended inline asm, taking advantage of the new, ↵ | Xavier Leroy | 2015-08-21 | 1 | -5/+24 |
| | | | | structured builtin arguments and results. | ||||
* | Refactoring of builtins and annotations in the back-end. | Xavier Leroy | 2015-08-21 | 51 | -1472/+1718 |
| | | | | | | | | | | | | | | | | | | | | | | | | Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations. | ||||
* | Merge pull request #46 from AbsInt/asmexpand | Xavier Leroy | 2015-08-17 | 1 | -0/+57 |
|\ | | | | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert | ||||
| * | Merge branch 'master' into asmexpand | Bernhard Schommer | 2015-07-14 | 2 | -2/+2 |
| |\ | |||||
| * | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert | Bernhard Schommer | 2015-06-26 | 1 | -0/+57 |
| | | | |||||
| * | | Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert" | Bernhard Schommer | 2015-06-26 | 1 | -57/+0 |
| | | | | | | | | | | | | | | | This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1. | ||||
| * | | Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵ | Bernhard Schommer | 2015-06-10 | 1 | -0/+57 |
| | | | | | | | | | | | | the same way as it is done for PPC. | ||||
* | | | ValueDomain: add some documentation comments. | Xavier Leroy | 2015-07-19 | 1 | -20/+32 |
| | | | |||||
* | | | Value analysis: keep track of pointer values that leak through small ↵ | Xavier Leroy | 2015-07-19 | 3 | -161/+179 |
| | | | | | | | | | | | | | | | | | | 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 Leroy | 2015-07-19 | 2 | -156/+164 |
| | | | | | | | | | | | | | | | | | | 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. | ||||
* | | | ValueDomain.aptr_of_aval: be more conservative with pointers synthesized ↵ | Xavier Leroy | 2015-07-18 | 2 | -6/+14 |
| | | | | | | | | | | | | | | | | | | from numbers. For example: *((int *) 0x10000) = 0. This write used to be treated as not interfering with any load. With this change, in relaxed value analysis mode, it is treated as interfering with any load except those from the current stack frame. | ||||
* | | | Missing cases in ValueDomain.vnormalize, causing overapproximation. | Xavier Leroy | 2015-07-18 | 1 | -2/+2 |
| | | | |||||
* | | | Missing case in ValueDomain.pincl, causing incompleteness. | Xavier Leroy | 2015-07-18 | 1 | -0/+9 |
| | | | |||||
* | | | Introduce tolerance for casts of pointer values to/from 64-bit integers. | Xavier Leroy | 2015-07-15 | 1 | -3/+12 |
| |/ |/| | |||||
* | | Do not search for high and low pc of inlined functions. | Bernhard Schommer | 2015-07-02 | 1 | -1/+1 |
| | | |||||
* | | Removed the version from the compcert.ini file and add it again in a ↵ | Bernhard Schommer | 2015-07-01 | 1 | -1/+1 |
|/ | | | | separate file. | ||||
* | Merged PrintAnnot into PrintAsmaux. | Bernhard Schommer | 2015-05-14 | 3 | -185/+163 |
| | |||||
* | Extended inline asm: revised treatment of clobbered registers. | Xavier Leroy | 2015-05-09 | 2 | -10/+3 |
| | | | | | | | | | | - 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 | ||||
* | Use globl also for global variables. | Bernhard Schommer | 2015-05-07 | 1 | -1/+1 |
| | |||||
* | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵ | Xavier Leroy | 2015-04-30 | 6 | -63/+63 |
| | | | | Val.lessdef, etc. | ||||
* | Take asm clobbers into account for determining callee-save registers used. | Xavier Leroy | 2015-04-23 | 1 | -1/+6 |
| | |||||
* | Cleanups and updates for extended asm. | Xavier Leroy | 2015-04-21 | 1 | -1/+1 |
| | |||||
* | Support for GCC-style extended asm, continued: | Xavier Leroy | 2015-04-21 | 2 | -2/+18 |
| | | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml | ||||
* | Experiment: support a subset of GCC's extended asm statements. | Xavier Leroy | 2015-04-17 | 3 | -3/+25 |
| | |||||
* | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-14 | 3 | -1/+5 |
|\ | |||||
| * | Harmless typo ('__' instead of '_') causing a warning at extraction time. | Xavier Leroy | 2015-04-06 | 1 | -1/+1 |
| | | |||||
| * | Missing case for the new 'annot' instruction. | Xavier Leroy | 2015-04-06 | 2 | -0/+4 |
| | | |||||
* | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-02 | 47 | -330/+1337 |
|\| | |||||
| * | Merge pull request #34 from AbsInt/extended-annotations | Xavier Leroy | 2015-04-01 | 46 | -327/+1332 |
| |\ | | | | | | | Extended annotations | ||||
| | * | Updated the Caml part. Added some more tests in annot1.c. | Xavier Leroy | 2015-03-27 | 10 | -73/+88 |
| | | | |||||
| | * | Extended arguments to annotations, continued: | Xavier Leroy | 2015-03-27 | 3 | -257/+133 |
| | | | | | | | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec. | ||||
| | * | Extend annotations so that they can keep track of global variables and local ↵ | Xavier Leroy | 2015-03-27 | 40 | -281/+1395 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet. | ||||
| * | | Revised semantics of comparisons between a pointer and 0. | Xavier Leroy | 2015-03-15 | 2 | -3/+5 |
| |/ | | | | | | | | | | | | | | | | | | | | | It used to be that a pointer value (Vptr) always compare unequal to the null pointer (Vint Int.zero). However, this may not be true in the final machine code when pointer addition overflows and wraps around to the bit pattern 0. This patch checks the validity of the pointer being compared with 0, and makes the comparison undefined if the pointer is out of bounds. Note: only the IA32 back-end was updated, ARM and PowerPC need updating. | ||||
* | | Print all files ever encountered in the filenum. | Bernhard Schommer | 2015-04-01 | 1 | -0/+7 |
| | | |||||
* | | Added translation fucntion for declarations and fundefinitions. | Bernhard Schommer | 2015-03-23 | 1 | -4/+38 |
| | | |||||
* | | Activating the printing of the debug information for supported architecture. | Bernhard Schommer | 2015-03-19 | 1 | -2/+6 |
| | | |||||
* | | Added function to convert C types into their dwarf represnation. | Bernhard Schommer | 2015-03-18 | 2 | -4/+2 |
| | | |||||
* | | Started implementing the printing functions for the debug info. Added a ↵ | Bernhard Schommer | 2015-03-16 | 2 | -1/+11 |
| | | | | | | | | global target dependend option to activate the printing only for targets wher it works. | ||||
* | | Started integrating the debug printing in the common backend_printer. | Bernhard Schommer | 2015-03-11 | 2 | -0/+4 |
| | | |||||
* | | Merge remote-tracking branch 'github/backend_printer' into dwarf | Bernhard Schommer | 2015-03-10 | 3 | -0/+251 |
|\| | | | | | | | | | | | | | Conflicts: arm/PrintAsm.ml ia32/PrintAsm.ml powerpc/PrintAsm.ml | ||||
| * | Removed unused sel_target, changed cygwin symbol names and changed the ↵ | Bernhard Schommer | 2015-02-19 | 2 | -3/+2 |
| | | | | | | | | default function aligment to be target dependent. | ||||
| * | Added an elf prefix to all common elf functions in PrintAsmaux. | Bernhard Schommer | 2015-02-18 | 2 | -17/+15 |
| | | |||||
| * | Changed print_fun/var_info to be functions instead of booleans. | Bernhard Schommer | 2015-02-18 | 2 | -6/+4 |
| | | |||||
| * | Removed some style issues. | Bernhard Schommer | 2015-02-18 | 1 | -65/+71 |
| | | |||||
| * | Changed arm backend to the common backend printer. | Bernhard Schommer | 2015-02-09 | 2 | -2/+2 |
| | | |||||
| * | Changed the ia32 backend to the new Printer. | Bernhard Schommer | 2015-02-06 | 1 | -0/+5 |
| | | |||||
| * | Changed the ASM printer of the powerpc to the generalized backend. | Bernhard Schommer | 2015-02-05 | 3 | -2/+119 |
| | | |||||
| * | Moved more common functions into a seperate file. | Bernhard Schommer | 2015-02-04 | 1 | -2/+46 |
| | | |||||
| * | Started moving common backend functions into one file. | Bernhard Schommer | 2015-02-03 | 1 | -0/+84 |
| | |