Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 32-bit rotate finished | David Monniaux | 2019-03-16 | 1 | -1/+4 |
| | |||||
* | Added error message for Odivfs in Asmblockgen | Cyril SIX | 2019-03-08 | 1 | -0/+1 |
| | |||||
* | Rajout de commentaires sur les instructions non émises | Cyril SIX | 2019-03-08 | 1 | -8/+8 |
| | |||||
* | Fix minor proof | Cyril SIX | 2019-03-07 | 1 | -25/+37 |
| | |||||
* | Added double comparisons | Cyril SIX | 2019-03-01 | 1 | -20/+20 |
| | |||||
* | Ajouté la négation des comparateurs single | Cyril SIX | 2019-03-01 | 1 | -2/+2 |
| | |||||
* | Implemented float comparisons (no branching yet, and no negation) | Cyril SIX | 2019-03-01 | 1 | -28/+20 |
| | |||||
* | Ointuofsingle done | Cyril SIX | 2019-03-01 | 1 | -29/+11 |
| | |||||
* | Float conversion fixes + some more conversions | Cyril SIX | 2019-02-27 | 1 | -0/+24 |
| | |||||
* | Removing unused cases Asmblockgen | Cyril SIX | 2019-02-27 | 1 | -3/+0 |
| | |||||
* | Rajout d'opérateurs flottants, travail sur les tests --> à continuer | Cyril SIX | 2019-02-15 | 1 | -99/+43 |
| | |||||
* | Added Olongoffloat, Ofloatoflong and doubleconv test | Cyril SIX | 2019-02-12 | 1 | -0/+6 |
| | |||||
* | Added Ointofsingle + floatconv unit test | Cyril SIX | 2019-02-12 | 1 | -1/+4 |
| | |||||
* | Added Osingleofint | Cyril SIX | 2019-02-12 | 1 | -13/+12 |
| | |||||
* | Added Ofloatconst and Osingleconst (not integrated in scheduler yet) | Cyril SIX | 2019-02-12 | 1 | -10/+4 |
| | |||||
* | Added indirect tailcalls | Cyril SIX | 2019-02-08 | 1 | -2/+2 |
| | |||||
* | Oshrxlimm | Cyril SIX | 2019-02-08 | 1 | -1/+7 |
| | |||||
* | Rajouté des erreurs plus explicites dans Asmblockgen.v | Cyril SIX | 2019-01-30 | 1 | -13/+57 |
| | |||||
* | give meaningful "unhandled instr" messages | David Monniaux | 2019-01-29 | 1 | -11/+7 |
| | |||||
* | Adding indirect calls (icall instruction) | Cyril SIX | 2019-01-29 | 1 | -3/+3 |
| | |||||
* | Adding a predicate that a builtin must be alone in its basicblock | Cyril SIX | 2019-01-23 | 1 | -2/+6 |
| | |||||
* | Added sxwd and zxwd support | Cyril SIX | 2019-01-22 | 1 | -9/+4 |
| | |||||
* | Merge branch 'mppa_k1c' into mppa_postpass | Cyril SIX | 2019-01-17 | 1 | -13/+13 |
|\ | |||||
| * | Added an error message for 32-bits division and modulo | Cyril SIX | 2018-12-11 | 1 | -13/+13 |
| | | |||||
* | | Moving size_blocks from Asmblockgen to Asmblock | Cyril SIX | 2018-12-05 | 1 | -9/+0 |
|/ | |||||
* | Changed ABI to match GCC - interoperability not tested yet | Cyril SIX | 2018-11-23 | 1 | -11/+13 |
| | |||||
* | Mise à jour vis à vis de CompCert 3.4 | Cyril SIX | 2018-11-21 | 1 | -1/+2 |
| | |||||
* | Modified "Asmgen.*" error messages to "Asmblockgen.*" | Cyril SIX | 2018-11-16 | 1 | -12/+12 |
| | |||||
* | MBcond true proved (but a small change needs to be done to Asmblockgenproof1) | Cyril SIX | 2018-11-06 | 1 | -0/+5 |
| | |||||
* | Début de MBcond | Cyril SIX | 2018-11-05 | 1 | -2/+2 |
| | |||||
* | MBreturn done | Cyril SIX | 2018-11-05 | 1 | -3/+3 |
| | |||||
* | Setting ep to false when the basicblock has a header. MBgoto done. ↵ | Cyril SIX | 2018-10-31 | 1 | -3/+1 |
| | | | | MBgetparam needs fix | ||||
* | Enlèvement de Pnop inutiles pour le Pbuiltin | Cyril SIX | 2018-10-26 | 1 | -5/+8 |
| | |||||
* | Adding "proof irrelevance" to bblocks | Cyril SIX | 2018-10-25 | 1 | -5/+6 |
| | |||||
* | Commencé à réintroduire du "ep" qui a du sens | Cyril SIX | 2018-10-19 | 1 | -8/+8 |
| | |||||
* | transl_blocks de nouveau prouvé + Ltac exploreInst | Cyril SIX | 2018-10-16 | 1 | -9/+31 |
| | |||||
* | Réintroduction du Pnop, que si pas de body et d'exit. Réécriture du ↵ | Cyril SIX | 2018-10-15 | 1 | -4/+8 |
| | | | | transl_bblocks_distrib | ||||
* | Stuck on proving step_simu_body | Cyril SIX | 2018-10-12 | 1 | -3/+8 |
| | |||||
* | Preuve de MBcall et du exit=None dans le step_simu_control | Cyril SIX | 2018-10-10 | 1 | -2/+2 |
| | |||||
* | Un peu d'avancement dans exec_straight_control et cie | Cyril SIX | 2018-10-08 | 1 | -2/+2 |
| | |||||
* | Schéma de simulation + les Pnop sont maintenant implicites | Cyril SIX | 2018-10-03 | 1 | -3/+5 |
| | |||||
* | return_address suite | Sylvain Boulmé | 2018-09-19 | 1 | -5/+13 |
| | |||||
* | Rajout d'un return_address_offset. Besoin de changer forward_simu de mach ↵ | Cyril SIX | 2018-09-06 | 1 | -2/+2 |
| | | | | machblock | ||||
* | Asmblock -> Asm presque fini.. erreur sur driver/Compiler.v | Cyril SIX | 2018-09-06 | 1 | -1/+1 |
| | |||||
* | Asmblockgen: Added Pnop and Program Definitions | Cyril SIX | 2018-09-06 | 1 | -18/+15 |
| | |||||
* | Asmblock: Adding forward_simulation and determinism as axioms | Cyril SIX | 2018-09-06 | 1 | -19/+19 |
| | |||||
* | Asmblockgen.v finished (no proof yet) | Cyril SIX | 2018-09-06 | 1 | -112/+153 |
| | |||||
* | Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléter | Cyril SIX | 2018-09-06 | 1 | -0/+857 |
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. |