aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* timings for glpsolDavid Monniaux2019-06-063-0/+348
|
* GLPK 4.65David Monniaux2019-06-06281-0/+126536
|
* finish merging master branch (fixes problems in glpk colamd)David Monniaux2019-06-063-43/+0
|
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-065-9/+65
|\
| * Added Pfmovite to list of known mnemonic names.Bernhard Schommer2019-06-061-1/+1
| |
| * Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| | | | | | | | | | | | | | Sometimes the result of a void function is assigned to a variable. This can occur with C conditional expressions ?: at type void, e.g. the "assert" macro of MacOS. A similar relaxation was already there in RTLtyping.
| * If-conversion optimizationXavier Leroy2019-06-0610-75/+751
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
| * Type inference and type checking for CminorXavier Leroy2019-06-062-1/+798
| | | | | | | | | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
| * Additional simulation diagrams for determinate source languagesXavier Leroy2019-06-061-0/+173
| | | | | | | | | | If the source language is determinate, it can take several steps (not just one) before the "match_state" invariant is reinstated.
| * ARM: select is not supported at type TlongXavier Leroy2019-06-062-2/+11
| |
| * New additional check for void parameters. (#174)Bernhard Schommer2019-06-031-3/+5
| | | | | | | | There should only be one unnamed parameter of type void in the parameter list.
* | timingsDavid Monniaux2019-06-061-1/+16
| |
* | print clock infoDavid Monniaux2019-06-062-0/+27
| |
* | compiles and linksDavid Monniaux2019-06-061-1/+9
| |
* | for compiling cjpeg/djpegDavid Monniaux2019-06-062-308/+328
| |
* | fix measuresDavid Monniaux2019-06-061-7/+7
| |
* | some more benchmarksDavid Monniaux2019-06-069-27/+60
| |
* | attempt at -O1David Monniaux2019-06-061-1/+5
| |
* | add version.h, prims.cDavid Monniaux2019-06-063-1/+1160
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2019-06-051-1/+1
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Fix for #134 Pjumptable not recognizedCyril SIX2019-06-051-1/+1
| | |
* | | disable large benchmarks that rely on heap saturation and other limitsDavid Monniaux2019-06-052-10/+14
|/ /
* | fixed reservation table for cmoveDavid Monniaux2019-06-051-1/+5
| |
* | move with immediatesDavid Monniaux2019-06-042-1/+31
| |
* | osel immDavid Monniaux2019-06-048-23/+117
| |
* | begin osel immDavid Monniaux2019-06-043-3/+57
| |
* | added immediate cmoveDavid Monniaux2019-06-046-38/+80
| |
* | shortcuts for cmoveDavid Monniaux2019-06-043-21/+41
| |
* | shortcut cmove worksDavid Monniaux2019-06-042-89/+7
| |
* | why doesn't it work?David Monniaux2019-06-042-7/+265
| |
* | little restructuringDavid Monniaux2019-06-041-3/+4
| |
* | keep the .s filesDavid Monniaux2019-06-041-0/+2
| |
* | remove old "ternary" stuffDavid Monniaux2019-06-045-47/+10
| |
* | start to have whole path if-conversion?David Monniaux2019-06-043-3/+18
| |
* | Osel -> assembleurDavid Monniaux2019-06-043-104/+112
| |
* | Osel is output = 1st inputDavid Monniaux2019-06-041-0/+1
| |
* | Osel operation (not yet compiled)David Monniaux2019-06-043-31/+39
| |
* | rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-0314-914/+47
| |
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-03158-9521/+14486
|\ \ | | | | | | | | | mppa-if-conversion
| * | ARM: select is not supported at type TlongXavier Leroy2019-06-013-4/+14
| | |
| * | If-conversion optimizationXavier Leroy2019-05-3110-75/+746
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
| * | Type inference and type checking for CminorXavier Leroy2019-05-312-1/+799
| | | | | | | | | | | | | | | | | | | | | This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.
| * | Additional simulation diagrams for determinate source languagesXavier Leroy2019-05-311-0/+173
| |/ | | | | | | | | If the source language is determinate, it can take several steps (not just one) before the "match_state" invariant is reinstated.
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-3121-31/+31
| | | | | | | | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
| * Provide a float select operation for PowerPC. (#173)Bernhard Schommer2019-05-289-7/+101
| | | | | | | | | | | | The FP select for PowerPC stores both addresses in two subsequent stack slots and loads them using an offset created from the result of the comparison.
| * PowerPC: add SelectOp.select functionXavier Leroy2019-05-262-0/+31
| | | | | | | | | | This function and its proof should have been part of commit 43e7b67. They are already there for the other ports.
| * ARM: Fix expansion of FP conditional moveXavier Leroy2019-05-261-2/+2
| | | | | | | | | | The "vmov" instruction (Advanced SIMD) cannot be conditional. The "vmov.f64" instruction (VFPv2) can be conditional.
| * Coq 8.9.1 supportXavier Leroy2019-05-211-3/+3
| | | | | | | | It works fine with the current sources.
| * Csyntax.v: Fix a typo in a documentation comment (#292)Bart Jacobs2019-05-211-1/+1
| |
| * Add a check for the args of unprototyped calls.Bernhard Schommer2019-05-201-3/+8
| | | | | | | | | | | | The arguments that are passed to an unprototyped function must also be checked to be valid types passed to a function, i.e. they must be complete types after argument conversion.
generated by cgit (git 2.34.1) at 2024-07-12 02:21:28 +0000