aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* Removing unused cases AsmblockgenCyril SIX2019-02-271-3/+0
|
* Proving the trans_block_header axiomsCyril SIX2019-02-274-713/+719
|
* 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-253-572/+605
|
* Finished the forward_simu of Asmblockdeps.vCyril SIX2019-02-251-6/+90
|
* forward_simu_basic prouvé --> à prouver, trans_arith_correct (Asmblockdeps)Cyril SIX2019-02-221-2/+28
|
* forward_simu_basic proof until Pallocframe in Asmblockdeps.vCyril SIX2019-02-221-9/+94
|
* Complete proof of forward_simu_control in AsmblockdepsCyril SIX2019-02-221-1/+109
|
* Separated forward_simulation into body and exit (Asmblockdeps)Cyril SIX2019-02-211-5/+23
|
* Starting forward simulation Asmblock -> AsmblockdepsCyril SIX2019-02-211-22/+97
|
* PostpassScheduling: outcome' = option state'Cyril SIX2019-02-211-4/+4
|
* Finished the compilation of Asmblock to AbstractbbCyril SIX2019-02-201-31/+41
|
* Added compilation in abstractbb of most of the basic instructionsCyril SIX2019-02-201-6/+76
|
* Added compilation of control instructions to AbstractBBCyril SIX2019-02-201-3/+74
|
* Remove unnecessary and error prone FR constructor for pregsCyril SIX2019-02-204-11/+5
|
* Added useful operators for the control flow instructionsCyril SIX2019-02-201-3/+74
|
* Problème résolu en prenant les noms de resources comme étant des PosCyril SIX2019-02-201-4/+14
|
* Stuck at module IDTCyril SIX2019-02-201-1/+10
|
* Finished specialization of the Abstractbb languageCyril SIX2019-02-201-89/+253
|
* WIP sur Asmblockdeps.vCyril SIX2019-02-201-0/+168
|
* [BROKEN] trying to generalize Sylvain's abstract bb to include a genv.Cyril SIX2019-02-207-87/+133
| | | | FIXME - DepExampleDemo.v
* use a Pfsd (store double) and not a Pfss (store single) for storing doublesDavid Monniaux2019-02-181-1/+1
|
* reversed the register allocation ordering between float and int registers, ↵David Monniaux2019-02-181-2/+2
| | | | to avoid contention
* Rajout d'opérateurs flottants, travail sur les tests --> à continuerCyril SIX2019-02-155-114/+169
|
* FIX axiom to be realized issueCyril SIX2019-02-152-2/+35
|
* Generalizing state' in PostpassSchedulingCyril SIX2019-02-141-32/+23
|
* More lemmas in PostpassSchedulingCyril SIX2019-02-141-6/+26
|
* Some more lemma proving in PostpassSchedulingCyril SIX2019-02-141-10/+73
|
* Proving verify_schedule_correct with axiomsCyril SIX2019-02-142-17/+132
|
* Merge branch 'mppa_postpass' of ↵David Monniaux2019-02-1332-117/+5049
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
| * Added AbstractBasicBlock files to the Coq build processCyril SIX2019-02-1325-0/+4692
| |
| * Added Olongoffloat, Ofloatoflong and doubleconv testCyril SIX2019-02-125-3/+25
| |
| * Added Ointofsingle + floatconv unit testCyril SIX2019-02-126-6/+17
| |
| * Added OsingleofintCyril SIX2019-02-126-16/+28
| |
| * Added Pmakefs and Pmakef to the schedulerCyril SIX2019-02-121-3/+9
| |
| * Added Ofloatconst and Osingleconst (not integrated in scheduler yet)Cyril SIX2019-02-125-10/+53
| |
| * Minor refactorizationCyril SIX2019-02-122-12/+12
| |
| * Proof of axiom verified_schedule_headerCyril SIX2019-02-122-59/+133
| |
| * Proving the axiom verified_schedule_single_instCyril SIX2019-02-122-5/+35
| |
| * Proving verified_schedule_size axiomCyril SIX2019-02-112-16/+58
| |
* | We have one example that exceeds a total latency of 5000, better simply not ↵David Monniaux2019-02-131-1/+1
|/ | | | constrain this limit.
* Fix for immediate size miscomputation in postpass oracle.Cyril SIX2019-02-081-12/+11
|
* Added indirect tailcallsCyril SIX2019-02-086-6/+38
|
* OshrxlimmCyril SIX2019-02-082-17/+24
|
* Un peu de refactorisationCyril SIX2019-02-072-82/+67
|
* Removing the low_half axiomCyril SIX2019-02-054-53/+46
|
generated by cgit (git 2.34.1) at 2024-07-12 05:21:10 +0000