aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* Psemi manquant dans l'expansion de PallocframeCyril SIX2019-03-191-0/+2
|
* Merge branch 'mppa_postpass' of ↵Cyril SIX2019-03-1814-18/+257
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * bug de pretty printingDavid Monniaux2019-03-181-2/+2
| |
| * andn / orn long complete I thinkDavid Monniaux2019-03-181-0/+3
| |
| * selection of andn/orn on longDavid Monniaux2019-03-182-0/+10
| |
| * some more andn / ornDavid Monniaux2019-03-183-0/+28
| |
| * andn/orn start being generatedDavid Monniaux2019-03-183-8/+22
| |
| * andn / orn suiteDavid Monniaux2019-03-186-7/+34
| |
| * orn / andn in asmDavid Monniaux2019-03-184-4/+50
| |
| * some more about andn/ornDavid Monniaux2019-03-182-0/+24
| |
| * begin andn ornDavid Monniaux2019-03-183-0/+87
| |
* | The parent frame pointer is now R17 instead of R14Cyril SIX2019-03-187-27/+21
|/
* long nand, nor, nxorDavid Monniaux2019-03-1611-7/+144
|
* nxorDavid Monniaux2019-03-1612-3/+59
|
* nor implementeDavid Monniaux2019-03-167-0/+39
|
* partial norwDavid Monniaux2019-03-165-9/+26
|
* nand is implementedDavid Monniaux2019-03-166-2/+28
|
* some more nandDavid Monniaux2019-03-163-3/+45
|
* nand debutDavid Monniaux2019-03-163-0/+18
|
* fix problem with ALU reservation tablesDavid Monniaux2019-03-161-1/+3
|
* 32-bit rotate finishedDavid Monniaux2019-03-166-6/+17
|
* select rotate ops 32-bitDavid Monniaux2019-03-163-2/+74
|
* some more progress on rotateDavid Monniaux2019-03-162-0/+6
|
* ValueAOp rotate 32-bitDavid Monniaux2019-03-161-0/+1
|
* instruction rotateDavid Monniaux2019-03-162-0/+3
|
* Removing SelectLong.v from the git repo (compiled from SelectLong.vp)Cyril SIX2019-03-152-800/+1
|
* better robustness wrt exceptionsDavid Monniaux2019-03-141-5/+9
|
* Corrigé certaines latences (Store -> 1 i/o 3, Set -> 4 i/o 3)Cyril SIX2019-03-131-4/+3
|
* Fix for CompCert 3.5Cyril SIX2019-03-131-0/+1
|
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-133-25/+25
|
* for using CPlexDavid Monniaux2019-03-131-1/+12
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-03-122-109/+134
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Added cascaded_scheduler but the flag does not workCyril SIX2019-03-121-1/+1
| |
| * Added a flag for changing the scheduler (not any choice available right now)Cyril SIX2019-03-121-2/+3
| |
| * Proof of exec_trans_pcincr solvedCyril SIX2019-03-121-7/+31
| |
| * Merge remote-tracking branch 'origin/mppa_parcheck' into mppa_parcheckCyril SIX2019-03-121-12/+12
| |\
| | * fix trans_pcincr for parcheck. (Proof is broken. cf FIXME)Sylvain Boulmé2019-03-121-12/+12
| | |
| * | Simplification des preuves "de discrimination" dans AsmblockdepsCyril SIX2019-03-121-94/+77
| |/
| * [BROKEN] Added parallelizability check - breaks all the conditional jumpsCyril SIX2019-03-122-1/+19
| |
* | -fpostpass-ilpDavid Monniaux2019-03-121-2/+4
| |
* | better tracing for ILP + make cleanDavid Monniaux2019-03-122-3/+7
|/
* Fix for frame pointer being destroyedCyril SIX2019-03-121-5/+10
|
* volatile storesDavid Monniaux2019-03-101-43/+40
|
* volatile loadDavid Monniaux2019-03-101-37/+37
|
* Added error message for Odivfs in AsmblockgenCyril SIX2019-03-081-0/+1
|
* Rajout de commentaires sur les instructions non émisesCyril SIX2019-03-081-8/+8
|
* Fix for the compw immediate problemCyril SIX2019-03-081-7/+17
|
* Minor fix on TargetPrinter (coqint instead of coqint64 for adequate types)Cyril SIX2019-03-081-8/+8
|
* Refactorisation des load et des storeCyril SIX2019-03-083-62/+40
|
* Reverting the hack introduces on Pcompw etc..Cyril SIX2019-03-081-14/+3
|