aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
...
| * Preuve du internal_function (step_simulation)Cyril SIX2018-09-283-36/+90
| |
| * storeind_ptr_correct un peu d'avancéeCyril SIX2018-09-273-22/+33
| |
| * Avancement dans exec_straight_throughCyril SIX2018-09-271-9/+51
| |
| * Enlèvement du "no_builtin" condition; exec_control sur les option control; ↵Cyril SIX2018-09-264-55/+120
| | | | | | | | exec_straight_blocks
| * AB: removing bregsCyril SIX2018-09-265-97/+73
| |
| * MB2AB - Adding Asmblockgenproof1.vCyril SIX2018-09-261-0/+1595
| |
| * MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-253-14/+214
| |
| * MB2AB - Proof of external function stepCyril SIX2018-09-253-13/+85
| |
| * add an example on depfreeSylvain Boulmé2018-09-251-1/+19
| |
| * relectureSylvain Boulmé2018-09-242-27/+148
| |
| * Some definitions in AsmbundleCyril SIX2018-09-241-0/+98
| |
| * a few stubs for bundlingSylvain Boulmé2018-09-244-194/+334
| |
| * one step toward "bundle_step"Sylvain Boulmé2018-09-241-6/+55
| |
| * relectureSylvain Boulmé2018-09-241-12/+1
| |
| * MB2AB - changement du lock-step en star, cas du Returnstate faitCyril SIX2018-09-211-10/+27
| |
| * MB2AB - Trois premières parties du lock-stepCyril SIX2018-09-212-17/+322
| |
| * return_address_exists -> doneSylvain Boulmé2018-09-203-25/+92
| |
| * avancement return_addressSylvain Boulmé2018-09-201-45/+64
| |
| * return_address suiteSylvain Boulmé2018-09-194-17/+137
| |
| * proof sketch for Asmgenproof.return_address_exists ?Sylvain Boulmé2018-09-192-3/+21
| |
| * premier jet Asmblockgenproof.return_address_offsetSylvain Boulmé2018-09-183-9/+97
| |
| * Rebase avec le commit qui fixe les tests + librairiesCyril SIX2018-09-063-7/+15
| |
| * Asmblock & cie - ça compileCyril SIX2018-09-064-112/+101
| |
| * Extraction issueCyril SIX2018-09-063-3/+18
| |
| * une solution pour le rao -> on fait remonter dans AsmblockgenproofSylvain Boulmé2018-09-061-5/+5
| |
| * Rajout d'un return_address_offset. Besoin de changer forward_simu de mach ↵Cyril SIX2018-09-065-19/+50
| | | | | | | | machblock
| * resoud pb du TransfLinkSylvain Boulmé2018-09-061-0/+2
| |
| * Remplacement de match_prog par un plus classiqueCyril SIX2018-09-063-42/+70
| |
| * Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-068-3391/+753
| |
| * Asmblockgen: Added Pnop and Program DefinitionsCyril SIX2018-09-062-56/+22
| |
| * Example of Program use...Sylvain Boulmé2018-09-061-0/+16
| |
| * Asmblock: Adding forward_simulation and determinism as axiomsCyril SIX2018-09-063-19/+1145
| |
| * Asmblockgen.v finished (no proof yet)Cyril SIX2018-09-062-127/+199
| |
| * Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléterCyril SIX2018-09-062-12/+899
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Asmblock.v: - Rajout de "header" dans wf_bblock - Remplacer "code" par "bblocks". Pour la suite, je trouve plus clair de manipuler des bblocks, plutôt qu'un "code constitué de bblocks". ça permet de minimiser les modifications dans Asmblockgen.v - fn_code --> fn_blocks . fn_code ne devrait pas être utilisé dans le code OCaml de toute façon (vu la translation Asmblock -> Asm) - Rajout d'un type instruction qui regroupe les basic et les control ; facilite certaines définitions Asmblockgen.v: - Copie conforme de Asmgen.v, avec quelques changements (pas fini). Ce vers quoi je m'oriente : garder les fonctions existantes de génération de code ; on leur donne à manger la liste de basics de Machblock. On traduit le exit (qui peut spiller sur la liste de basics déjà traduite), et on met la dernière instruction de la trad du exit (qui doit être un control) dans le exit du bblock. - Pour le prologue : chaque instruction rajoutée "à la main" est dans son propre bblock. Voir la notation ::b pour le faire. A terme, il devrait y avoir moyen "d'accumuler" l'instruction au code généré ; pour l'instant je préfère ne pas compliquer la génération.
| * deplacement allocframe/freeframe/loadsymbolSylvain Boulmé2018-09-061-41/+37
| | | | | | | | dans instructions basiques des blocs.
| * Name changing + introducing Pbuiltin (alone in a block)Cyril SIX2018-09-061-91/+67
| |
| * Some renaming on asmblockCyril SIX2018-09-061-11/+11
| |
| * add comments (TODO/FIXME)Sylvain Boulmé2018-09-061-11/+28
| |
| * notation changeSylvain Boulmé2018-09-061-21/+21
| |
| * a version of Asmblock syntax and semanticsSylvain Boulmé2018-09-061-0/+1376
| | | | | | | | mixed between Machblock style and Asm...
| * Machblock: some renaming and proof simplificationsCyril SIX2018-09-062-221/+144
| |
| * Machblock: adaptation to the generalized ForwardSimulationBlockSylvain Boulmé2018-09-063-344/+292
| |
| * Machblock: some cleaningCyril SIX2018-09-063-196/+146
| |
| * Machblock: Mach language with basic blocksCyril SIX2018-09-063-0/+1741
| |
* | Added all the working builtins for ALU. Added BCU and LSU without testingCyril SIX2018-08-014-14/+372
|/
* MPPA - Added Builtins support. Starting with clzll and stsudCyril SIX2018-06-052-61/+6
|
* WIP - Trying to add builtins support. They are not detected for now :(Cyril SIX2018-05-304-38/+34
|
* MPPA - Added modulo and division 64 bits. Non certifiedCyril SIX2018-05-215-30/+25
| | | | | | | 32 bits version are not yet there. Right now the code is directly from libgcc, compiled with k1-gcc because of builtins.
* MPPA - refactored instructionsCyril SIX2018-05-116-500/+549
|
* Code cleaningCyril SIX2018-05-093-153/+99
|
generated by cgit (git 2.34.1) at 2024-07-12 04:51:49 +0000