aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Compiler.v
Commit message (Collapse)AuthorAgeFilesLines
* begin scripting the Compiler.v fileDavid Monniaux2020-04-211-568/+0
|
* Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-22/+46
|\
| * reordering passesDavid Monniaux2020-04-011-8/+8
| |
| * fix Compiler.vDavid Monniaux2020-04-011-12/+16
| |
| * attempt at compilingDavid Monniaux2020-04-011-12/+24
| |
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-licmDavid Monniaux2020-04-011-5/+5
| |\
| * | nop insertion at entrypointDavid Monniaux2020-03-291-15/+23
| | |
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-13/+31
|\ \ \
| * | | reloading and exploiting seems to workDavid Monniaux2020-04-081-12/+21
| | | |
| * | | installed Profiling (not finished)David Monniaux2020-04-081-12/+21
| | |/ | |/|
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-04-011-5/+5
|\| | | |/ |/|
| * -fduplicate -1 really desactivates the pass in Coq nowCyril SIX2020-04-011-5/+5
| |
* | typing and store stuffDavid Monniaux2020-03-121-3/+3
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-111-5/+5
|\|
| * [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-091-5/+5
| | | | | | | | To control the threshold for duplication
* | starts compiling but still fakeDavid Monniaux2020-03-101-9/+17
| |
* | CSE3 generate lists of killableDavid Monniaux2020-03-051-1/+1
| |
* | streamlined lattice codeDavid Monniaux2020-03-051-0/+1
|/
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-5/+6
|\
| * Added a flag to desactivate tail duplicationCyril SIX2020-01-271-5/+6
| |
* | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-9/+18
|\ \ | |/ |/|
| * connected (just a silly problem)David Monniaux2020-01-281-4/+32
| |
* | connect forward-moves to compilerDavid Monniaux2020-01-081-5/+14
| |
* | finish mergeDavid Monniaux2019-12-021-31/+19
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-5/+25
|\ \
| * \ Merge branch 'mppa-work' into mppa-duplicate-rtlCyril SIX2019-10-021-1/+1
| |\ \
| * | | Stubs for Duplicate passCyril SIX2019-09-031-28/+36
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-201-1/+1
|\ \ \ \ | | |/ / | |/| |
| * | | Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-181-1/+1
| |/ /
* / / -fall-loads-nontrapDavid Monniaux2019-09-091-2/+11
|/ /
* | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-271-1/+1
| |
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-261-1/+1
| |
* | Rajout d'un return_address_offset. Besoin de changer forward_simu de mach ↵Cyril SIX2018-09-061-1/+1
|/ | | | machblock
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-6/+6
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Strengthen the main compiler correctness results to account for separate ↵Xavier Leroy2016-03-061-149/+250
| | | | | | compilation and linking Define a "match_prog" relation corresponding to the composition of CompCert's passes. Use it to show semantic preservation (backward/forward simulations) not just for the compilation of whole programs, but also for the separate compilation of multiple units followed by linking.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-24/+24
|
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-1/+7
| | | | | | | | | | | | | | SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.
* Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-241-1/+8
| | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* Add flags to control individual optimization passes + flag -O0 for turning ↵Xavier Leroy2014-11-161-24/+74
| | | | them off.
* Merge of branch linear-typing:xleroy2014-04-061-22/+25
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-12/+9
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch value-analysis.xleroy2013-12-201-1/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-42/+9
| | | | | | | | | 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
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-031-1/+2
| | | | | | | | trick prevents a future mapping of the Mach/Asm call stack as a single block. IA32 is fixed, PowerPC and ARM remains to be done. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2136 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-5/+0
| | | | | | | | | | - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-6/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Remove some useless "Require".xleroy2012-12-301-3/+0
| | | | | | | Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the clightgen branch:xleroy2012-12-291-4/+9
| | | | | | | | | | | | | | | | | | - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-97/+0
| | | | | | | | | | | function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-06 14:57:28 +0000