aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintLTL.ml
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-2/+2
|\ | | | | | | | | | | Conflicts: Makefile configure
| * Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-161-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, the elimination of useless conditions done in the 2nd pass of the tunneling introduced some new "nop" instructions that were not eliminated. This commit solves this issue by anticipating the elimination of conditions in the 1st pass of the tunneling, the 2nd pass being unchanged. In case of cycles in the CFG, the full elimination of useless conditions may require several iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass. Hence, this measure results from a quite complex fixpoint computation: proving its properties would be very difficult. This leads us to introduce an oracle, implementing the first pass and producing the expected measure. A certified verifier directly checks that the measure provided by the oracle satisfies the properties expected by the simulation proof. Introducing this oracle/verifier pair has here the following advantage: - the proof is simpler than the original one (e.g. having a certified union-find structure is no more necessary for this pass). - the oracle is very efficient, by using imperative data-structure to compute memoized fixpoints. At runtime, the overhead induced by the verifier computations (and the actual computation of the measure) seems largely compensated by the gains obtained through the imperative oracle.
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-1/+1
|\ \ | |/ |/|
| * Move shared code in new file.Bernhard Schommer2020-06-281-1/+1
| | | | | | | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* | Added prediction info in the printersCyril SIX2020-03-131-2/+3
| |
* | Adding info field for branching in RTL, LTL, XTL and all associated passesCyril SIX2020-03-111-1/+1
| |
* | ONE "admitted" and things compileDavid Monniaux2019-09-061-3/+4
|/
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-1/+1
| | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
* Remove open Locations.Bernhard Schommer2017-02-061-6/+5
| | | | The Locations are only used in one function.
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-2/+2
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Code cleanup.Bernhard Schommer2016-03-101-4/+3
| | | | | | 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.
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-4/+3
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-2/+2
|
* Do not use Format for faster printing of RTL, XTL, LTL, Machxleroy2013-09-261-30/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Hunting stack overflows again:xleroy2013-05-271-1/+1
| | | | | | | | PrintLTL: List.map -> List.rev_map IRC: @ -> List.rev_append + don't maintain "extra" lists on precolored nodes. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2262 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-67/+92
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of annotation statements, and more generally built-in ↵xleroy2011-06-131-2/+5
| | | | | | functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Pretty-printers for RTL and LTL. Not yet well integrated.xleroy2010-05-021-0/+117
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1332 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 08:24:06 +0000