aboutsummaryrefslogtreecommitdiffstats
path: root/tools
Commit message (Collapse)AuthorAgeFilesLines
* [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-011-3/+3
|\
| * Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-103-12/+15
| |\
| * | Dupmap bugfix and some advance in LivegenLéo Gourdin2021-05-311-1/+1
| | |
| * | todosLéo Gourdin2021-05-181-1/+1
| | |
| * | preparing compiler passes and ml oraclesLéo Gourdin2021-05-171-3/+3
| | |
* | | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-171-1/+1
| | | | | | | | | | | | To respect the symmetry between RTL- and LTL-Tunneling
* | | Move rtl_tunneling to a more interesting placePierre Goutagny2021-06-151-1/+1
| | |
* | | Factorise RTL Tunneling pass in compiler_expandPierre Goutagny2021-06-151-1/+3
| | |
* | | Add RTL Tunneling as a passPierre Goutagny2021-06-141-1/+2
| |/ |/|
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-013-12/+15
|/ | | | cfrontend/C2C.ml
* insert CSE after constant propagation and before CSE2Sylvain Boulmé2021-02-101-0/+1
| | | | => useful to have a nice generated code for || (and also probably &&)
* Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-4/+7
|\ | | | | | | | | | | Conflicts: Makefile configure
| * Slight perf improvementCyril SIX2020-12-021-2/+2
| |
| * merge nouveau tunnelingDavid Monniaux2020-11-191-1/+1
| |
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-191-1/+1
| |\
| | * 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 remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-051-2/+3
| |\|
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-031-1/+3
| |\ \
| * \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-271-43/+54
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-2/+3
| |\ \ \ \
| * \ \ \ \ Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-282-0/+183
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework
* | \ \ \ \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-1/+1
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | |
| * | | | | | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* | | | | / move loop rotate downDavid Monniaux2020-11-041-4/+5
| |_|_|_|/ |/| | | |
* | | | | Loop Rotate with -flooprotateCyril SIX2020-11-031-0/+2
| |_|_|/ |/| | |
* | | | Splitting Duplicate in several passesCyril SIX2020-10-271-40/+51
| |_|/ |/| |
* | | reorder phasesDavid Monniaux2020-10-161-2/+3
| | |
* | | Changing duplicate verifier to be non optionalCyril SIX2020-10-091-1/+1
| |/ |/|
* | automatic date in the html indexSylvain Boulmé2020-05-281-0/+8
| |
* | add a renumber phaseDavid Monniaux2020-04-301-0/+1
| |
* | run a separate CSE3 for LICMDavid Monniaux2020-04-241-1/+3
| |
* | sync with licmDavid Monniaux2020-04-231-1/+1
| |
* | cbn and copyrightDavid Monniaux2020-04-221-0/+10
| |
* | use cbn in T instead of simpl in TDavid Monniaux2020-04-221-1/+1
| |
* | automated writing Compiler.vDavid Monniaux2020-04-221-8/+79
| |
* | generate mkpassDavid Monniaux2020-04-211-1/+13
| |
* | Require autogenDavid Monniaux2020-04-211-8/+22
| |
* | begin scripting the Compiler.v fileDavid Monniaux2020-04-211-0/+62
|/
* Revise the "bench" entries of the test suiteXavier Leroy2019-09-171-0/+101
| | | | | | | | Initially, the "bench" entries of the test suite used a "xtime" utility developed in-house and not publically available. This commit adds a version of "xtime" written in OCaml (tools/xtime.ml) and updates the "bench" entries of the test/*/Makefile to use it.
* ndfun: add support for guards on patternsXavier Leroy2019-08-071-5/+16
| | | | | | Syntax is "pat ?? bexpr => action". The whole case is selected only when "pat" matches and then "bexpr" evaluates to "true".
* Extend the modorder tool to handle Coq files as well (#54)Bernhard Schommer2018-02-081-7/+9
| | | | | | This is useful to e.g. identify the .vo files from CompCert that a clightgen-generated .v file needs. Also: the "result" field of the record type is now initialized with the LHS of the dependency, not the RHS. It doesn't matter because the result field is unused, but it makes more sense now.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-3/+3
|
* Removed the recdepend again and replaced it by a builtin Make function.Bernhard Schommer2015-02-271-206/+0
|
* Updated the recdepend tool to avoid printing of ./ at the begining and ↵Bernhard Schommer2015-02-251-50/+46
| | | | printing duplicated -I flags.
* Added a small ocamlfile that calls ocamlfind recursivly over a given directory.Bernhard Schommer2015-02-241-0/+210
|
* Use String.map instead of reimplementing it ourselves.Xavier Leroy2014-11-221-5/+18
| | | | Avoids warnings with 4.02.
* Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵Xavier Leroy2014-11-221-0/+112
| | | | | | produce the executables. configure: add check for GNU make.
* Merge of the nonstrict-ops branch:xleroy2012-01-141-0/+231
- Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-09 18:32:49 +0000