aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockdeps.v
Commit message (Collapse)AuthorAgeFilesLines
* progress on cmoveDavid Monniaux2019-03-251-0/+1
|
* rm Pdiv / PdivuDavid Monniaux2019-03-221-29/+0
|
* Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-191-15/+82
|\
| * mul immediate beginDavid Monniaux2019-03-191-0/+2
| |
| * improve robustness of Asmblockdeps.arith_op_eq.Sylvain Boulmé2019-03-191-13/+29
| |
| * fix missing case in Asmblockdeps.arith_op_eqSylvain Boulmé2019-03-191-2/+2
| |
| * ça passe mais pas encore l'oracleDavid Monniaux2019-03-181-1/+50
| |
* | Pseudo instruction for 32 bits division, no code generation yetCyril SIX2019-03-191-0/+45
| |
* | Merge branch 'mppa_postpass' of ↵Cyril SIX2019-03-181-0/+8
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * orn / andn in asmDavid Monniaux2019-03-181-0/+8
| |
* | The parent frame pointer is now R17 instead of R14Cyril SIX2019-03-181-2/+2
|/
* long nand, nor, nxorDavid Monniaux2019-03-161-0/+6
|
* nxorDavid Monniaux2019-03-161-0/+2
|
* partial norwDavid Monniaux2019-03-161-0/+2
|
* nand is implementedDavid Monniaux2019-03-161-0/+2
|
* 32-bit rotate finishedDavid Monniaux2019-03-161-0/+1
|
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-131-20/+20
|
* 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-121-0/+8
|
* Refactorisation des load et des storeCyril SIX2019-03-081-27/+5
|
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patchCyril SIX2019-03-081-10/+14
|\
| * Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)Cyril SIX2019-03-071-10/+14
| |
* | Fixing Asmblockdeps proofsCyril SIX2019-03-081-147/+21
| |
* | remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-071-17/+8
| | | | | | | | | | | | TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible.
* | Experiment Patch of Memory ModelSylvain Boulmé2019-03-071-2/+2
|/
* fix eq sur OIncremPCSylvain Boulmé2019-03-061-7/+14
|
* quick fix of equalities issuesSylvain Boulmé2019-03-051-1/+6
|
* Added pretty printersCyril SIX2019-03-051-19/+208
|
* No more axioms remaining (scheduling completely proven), however error at ↵Cyril SIX2019-03-051-21/+3
| | | | extraction
* C'est moi qui avait fait des betises avec CoqIDE, ça remarcheCyril SIX2019-03-051-8/+26
|
* [BROKEN] error with the new is_constant and is_constant_correctCyril SIX2019-03-051-26/+8
|
* forward_simu_alt proof AsmblockdepsCyril SIX2019-03-051-1/+6
|
* remove cumbersome dependency on genv in bblock_eq_testSylvain Boulmé2019-03-051-6/+28
|
* No more axiom remaining in PostpassScheduling.v (but still a couple ↵Cyril SIX2019-03-051-1/+1
| | | | remaining in Asmblockdeps)
* bblock_equiv_reduce Asmblockdeps.vCyril SIX2019-03-041-4/+42
|
* (Unsafe) coercion of ??bool into boolSylvain Boulmé2019-03-021-0/+17
|
* Added double comparisonsCyril SIX2019-03-011-0/+1
|
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-011-0/+2
|
* Ointuofsingle doneCyril SIX2019-03-011-0/+1
|
* Float conversion fixes + some more conversionsCyril SIX2019-02-271-0/+6
|
* Proving the trans_block_header axiomsCyril SIX2019-02-271-0/+10
|
* Proving a few more lemmas AsmblockdepsCyril SIX2019-02-271-15/+38
|
* Proved forward_simu_stuck in Asmblockdeps.vCyril SIX2019-02-261-15/+132
|
* Finished trans_block_reverse_stuckCyril SIX2019-02-261-6/+26
|
* Proving two lemmas of trans_block_reverse_stuck AsmblockdepsCyril SIX2019-02-251-5/+46
|
* Splitting trans_block_reverse_stuck into smaller lemmasCyril SIX2019-02-251-8/+73
|
* Plugged Asmblockdeps into PostpassSchedulingCyril SIX2019-02-251-19/+98
|
generated by cgit (git 2.34.1) at 2024-07-12 09:46:11 +0000