aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Deadcode.v
Commit message (Collapse)AuthorAgeFilesLines
* Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-2/+2
|
* avancement (il faut utiliser Vundef visiblement)David Monniaux2019-09-021-2/+2
|
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-1/+1
| | | | | | | | | | | | 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.
* Deadcode: eliminate trivial Icond instructionsXavier Leroy2017-09-181-1/+4
| | | | | | These are conditionals where the "ifso" and the "ifnot" successors are the same. By eliminating them here and not later, we can also eliminate the instructions that compute the arguments to the condition, if any. There is another, later point where these trivial conditional instructions are eliminated: in the Tunneling phase. The elimination done in Tunneling is more powerful in that it works not just for conditionals whose two successors are the same, but also for conditionals whose two successors lead to the same point after a series of nops. The elimination done in Deadcode is more powerful in that it eliminates the instructions that compute the arguments to the condition. Hence it is worth having both eliminations.
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+2
| | | | | | This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses. Current status: x86 port only, the only new addressing mode handled is reg + offset.
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-21/+6
|
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-2/+2
|
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-1/+1
| | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-27/+38
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-271-0/+13
| | | | | | | | | | 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.
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-021-20/+33
| | | | | | | | NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-201-0/+192
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e