Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding copyrights | Cyril SIX | 2020-05-04 | 1 | -1/+1 |
| | |||||
* | Removed the assertion about prediction on ifso | Cyril SIX | 2020-04-09 | 1 | -2/+3 |
| | |||||
* | Some cleaning on Linearize and Duplicate | Cyril SIX | 2020-04-08 | 1 | -40/+49 |
| | |||||
* | Stopping traces at join points | Cyril SIX | 2020-04-01 | 1 | -2/+25 |
| | |||||
* | Linearize: Scheduling based on maxpc instead of dependencies | Cyril SIX | 2020-03-25 | 1 | -3/+9 |
| | |||||
* | Linearizeaux: Refining block selection in case of tie | Cyril SIX | 2020-03-24 | 1 | -19/+37 |
| | |||||
* | Removing store heuristic and more fine tuning loop heuristic | Cyril SIX | 2020-03-23 | 1 | -1/+1 |
| | |||||
* | More helpful debug info in linearize | Cyril SIX | 2020-03-13 | 1 | -1/+3 |
| | |||||
* | Correcting a few bugs in trace selection and expansion | Cyril SIX | 2020-03-12 | 1 | -7/+13 |
| | |||||
* | Adding info field for branching in RTL, LTL, XTL and all associated passes | Cyril SIX | 2020-03-11 | 1 | -5/+5 |
| | |||||
* | More debug info on Linearize and Duplicate | Cyril SIX | 2020-03-11 | 1 | -1/+1 |
| | |||||
* | Linearizeaux: dumb selector when cycling dependencies are found | Cyril SIX | 2020-03-10 | 1 | -4/+6 |
| | |||||
* | Linearizeaux, forgot to visit the rest of the nodes in dfs_visit | Cyril SIX | 2020-03-10 | 1 | -22/+26 |
| | |||||
* | Some dependencies were not taken into account in tracelinearize | Cyril SIX | 2020-03-10 | 1 | -15/+12 |
| | |||||
* | Linearize: More helpful message when tracelinearize fails | Cyril SIX | 2020-03-10 | 1 | -4/+12 |
| | |||||
* | Bug fix in ftracelinearize | Cyril SIX | 2020-03-10 | 1 | -4/+15 |
| | |||||
* | Linearizeaux: forgotten print | Cyril SIX | 2020-03-09 | 1 | -1/+1 |
| | |||||
* | Linearizeaux: Fixed bug where the output list was in reverse order | Cyril SIX | 2020-03-09 | 1 | -4/+20 |
| | |||||
* | Adding debug info in Linearizeaux | Cyril SIX | 2020-03-06 | 1 | -0/+12 |
| | |||||
* | [UNTESTED] Sequence ordering | Cyril SIX | 2020-03-06 | 1 | -3/+27 |
| | |||||
* | Linearize: Dependencies computing to decide which sequence to put first | Cyril SIX | 2020-03-03 | 1 | -31/+132 |
| | |||||
* | Linearizeaux: can_be_merged | Cyril SIX | 2020-02-21 | 1 | -13/+48 |
| | |||||
* | Linearizeaux: function try_merge | Cyril SIX | 2020-02-21 | 1 | -11/+20 |
| | |||||
* | WIP2 | Cyril SIX | 2020-02-20 | 1 | -16/+24 |
| | |||||
* | WIP | Cyril SIX | 2020-02-20 | 1 | -0/+26 |
| | |||||
* | First part of Hansen algorithm - build the sequences | Cyril SIX | 2020-02-19 | 1 | -1/+43 |
| | |||||
* | Added option -ftracelinearize which linearizes based on ifnot branches | Cyril SIX | 2020-02-12 | 1 | -3/+54 |
| | |||||
* | Compatibility with OCaml 4.08 (#302) | Xavier Leroy | 2019-07-08 | 1 | -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 | ||||
* | Deactivate warning 27 and added back removed code. | Bernhard Schommer | 2016-03-15 | 1 | -5/+5 |
| | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349 | ||||
* | Code cleanup. | Bernhard Schommer | 2016-03-10 | 1 | -8/+5 |
| | | | | | | 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. | ||||
* | Updated PR by removing whitespaces. Bug 17450. | Bernhard Schommer | 2015-10-20 | 1 | -2/+2 |
| | |||||
* | Change interface of Kildall solvers to avoid precomputing the map pc -> list ↵ | xleroy | 2013-08-12 | 1 | -2/+3 |
| | | | | | | of successors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 | 1 | -13/+15 |
| | | | | | | | | | 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 | ||||
* | Ported to Coq 8.4pl1. Merge of branches/coq-8.4. | xleroy | 2013-01-29 | 1 | -17/+4 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Support for inlined built-ins. | xleroy | 2010-06-29 | 1 | -0/+1 |
| | | | | | | | | | | | | | AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Added support for jump tables in back end. | xleroy | 2009-11-10 | 1 | -0/+2 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Cil2Csyntax: added goto and labels; added assignment between structs | xleroy | 2009-08-16 | 1 | -1/+2 |
| | | | | | | | | | | | | Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | New linearization heuristic | xleroy | 2009-02-27 | 1 | -32/+72 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1001 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive ↵ | xleroy | 2009-01-29 | 1 | -2/+1 |
| | | | | | | file systems. Replaced CList by CoqList and likewise for CString and CInt. Removed useless references to CList in hand-written Caml code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Elimination of "alloc" instruction in Caml files and test files. | xleroy | 2009-01-11 | 1 | -1/+0 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Reorganized the development, modularizing away machine-dependent parts. | xleroy | 2008-12-30 | 1 | -0/+85 |
Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |