aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | | Fixing Coq dependenciesCyril SIX2019-05-031-1/+1
| | | |
* | | | [FIX #101] PostpassSchedulingOracle:separate_opaque was not computing correctlyCyril SIX2019-05-031-9/+15
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workDavid Monniaux2019-05-0316-21/+308
|\| | | | |/ / |/| |
| * | -fcoalesce-memDavid Monniaux2019-05-035-7/+19
| | |
| * | use sq to save pairs of registersDavid Monniaux2019-05-035-11/+27
| | |
| * | it compilesDavid Monniaux2019-05-035-5/+65
| | |
| * | ça avanceDavid Monniaux2019-05-031-0/+27
| | |
| * | rm OfslowDavid Monniaux2019-05-031-1/+1
| | |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-0310-93/+61
| |\ \
| * | | getting stuck need to move offsetsDavid Monniaux2019-05-034-10/+40
| | | |
| * | | find consecutive writesDavid Monniaux2019-05-022-6/+83
| | | |
| * | | detect consecutive onesDavid Monniaux2019-05-021-2/+6
| | | |
| * | | example of spill peepholeDavid Monniaux2019-05-021-0/+21
| | | |
| * | | found peepholeDavid Monniaux2019-05-022-1/+24
| | | |
| * | | seems to workDavid Monniaux2019-05-022-2/+19
| | | |
* | | | Renaming "dumb" scheduling into "greedy"Cyril SIX2019-05-034-10/+5
| | | |
* | | | Fixing mppa_k1c/Chunks.v for Coq 8.9Cyril SIX2019-05-031-1/+3
| |/ / |/| |
* | | rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-0310-93/+61
|/ /
* | allow disabling + xx global symbolsDavid Monniaux2019-05-022-4/+9
| |
* | Merge branch 'mppa-xsaddr' into mppa-workDavid Monniaux2019-05-0223-55/+419
|\ \
| * | fix slow globals etc.David Monniaux2019-05-022-2/+2
| | |
| * | command line options (still incomplete)David Monniaux2019-05-026-11/+46
| | |
| * | forgot Chunks.vDavid Monniaux2019-05-022-1/+21
| | |
| * | fix targetprinter bug for .xsDavid Monniaux2019-05-011-4/+4
| | |
| * | load xs / store xs seem to workDavid Monniaux2019-05-011-1/+2
| | |
| * | does not yet work, arity mismatchDavid Monniaux2019-05-016-15/+15
| | |
| * | it compilesDavid Monniaux2019-05-0110-33/+164
| | |
| * | ça avanceDavid Monniaux2019-05-012-12/+85
| | |
| * | pass one proofDavid Monniaux2019-05-011-7/+2
| | |
| * | advancing (but broken)David Monniaux2019-05-012-0/+5
| | |
| * | translate load.xsDavid Monniaux2019-05-014-7/+30
| | |
| * | indexed2XS beginDavid Monniaux2019-05-013-3/+10
| | |
| * | begin load.xsDavid Monniaux2019-05-018-11/+85
| | |
* | | Merge branch 'dumb-scheduling' into mppa-workCyril SIX2019-04-305-7/+79
|\ \ \ | |/ / |/| |
| * | Setting fpostpass= optionCyril SIX2019-04-302-7/+9
| | |
| * | The scheduler selection works, but the argument is not optional yet ↵Cyril SIX2019-04-293-4/+13
| | | | | | | | | | | | (-fpostpass nameofscheduler)
| * | [BROKEN] Fixed the dumb scheduler, not yet properly integratedCyril SIX2019-04-292-3/+6
| | |
| * | [BUGGED] First attempt at a dumb scheduler ("accumulates" instructions)Cyril SIX2019-04-253-3/+61
| |/
* | rm unsupported int -> double signed/unsigned opsDavid Monniaux2019-04-294-17/+1
| |
* | removed fake ops for int32 -> doubleDavid Monniaux2019-04-296-24/+0
| |
* | float of int = float of long o long of intDavid Monniaux2019-04-292-4/+17
| |
* | float of intu = float of longu o longu of intuDavid Monniaux2019-04-292-4/+18
| |
* | srsdDavid Monniaux2019-04-292-16/+10
| |
* | forgot in oracleDavid Monniaux2019-04-291-0/+2
| |
* | begin using shrxDavid Monniaux2019-04-292-29/+10
| |
* | Srsd / SrswDavid Monniaux2019-04-297-5/+65
| |
* | Merge branch 'mppa-bitfields' into mppa-workDavid Monniaux2019-04-293-0/+105
|\ \
| * | test for long bitfieldsDavid Monniaux2019-04-291-0/+19
| | |
| * | insfl generationDavid Monniaux2019-04-292-0/+86
| | |
* | | Merge remote-tracking branch 'origin/mppa-bitfields' into mppa-workDavid Monniaux2019-04-2813-19/+270
|\| |