aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Coloringaux.ml
Commit message (Collapse)AuthorAgeFilesLines
* Separate interference graphs for ints and floats, i.e. don't record ↵xleroy2012-12-201-13/+16
| | | | | | interference edges between nodes of different types: this is useless and falsifies the heuristics based on node degree. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a ↵xleroy2012-01-211-11/+28
| | | | | | | | | certain customer's code backend/Coloringaux: avoid spilling the dummy result registers for built-ins that have no result. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1799 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloringaux: better cost estimate for annotation builtinsxleroy2011-06-141-0/+2
| | | | | | | Regression: more tests for annotations git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1675 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-3/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-021-37/+56
| | | | | | | | | | | | - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-181-9/+18
| | | | | | | | | | | | | | | | | | | | | | - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inlined built-ins.xleroy2010-06-291-4/+6
| | | | | | | | | | | | | 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
* Improved coalescing heuristics based on Hailperin's paper.xleroy2010-05-081-32/+49
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1338 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compute spill costs.xleroy2010-05-021-8/+92
| | | | | | | Attempt coalescing between stack-allocated variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1331 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloring: allow to exclude user-specified registers from allocation.xleroy2010-04-101-25/+40
| | | | | | | CPragmas (PPC/EABI only): add #pragma reserve_register git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1314 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-261-60/+132
| | | | | | | | | | nodes a la Appel and George. Maps: in PTree.combine, compress useless subtrees. Lattice: more efficient implementation of LPMap. Makefile: build profiling version git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update spill costs when coalescingxleroy2009-08-161-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1121 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+626
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
generated by cgit (git 2.34.1) at 2024-07-02 23:26:36 +0000