aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
...
* | | | Optimizing Asmblockdeps proofLéo Gourdin2020-11-281-58/+92
|/ / / | | | | | | Proof is now two times faster (from 60 to 30 seconds)
* | | Merge branch 'aarch64_Pfmovimm_tuning' into aarch64-postpassLéo Gourdin2020-11-265-259/+143
|\ \ \
| * | | Proof of Pfmovimm fine tuned OK, moving float checks in AsmLéo Gourdin2020-11-265-288/+148
| | | | | | | | | | | | Also some simplifications in Asmblockdeps
| * | | Fine tuning for PfmovimmLéo Gourdin2020-11-264-27/+51
| | | | | | | | | | | | | | | | - Functions to check a float logical immediate were translated from ocaml target printer in coq Asmblock - Some proof are admitted for now (we'll see if it is a good idea after some tests)
* | | | finish Asmgenproof.transf_program_correctSylvain Boulmé2020-11-261-5/+15
| | | |
* | | | Fixing a generation bug on shrx in AsmblockgenLéo Gourdin2020-11-261-0/+6
|/ / / | | | | | | I forgot this one and the gen test script reminds me
* | | This commit fix the issue #226Léo Gourdin2020-11-261-50/+57
| | | | | | | | | | | | - adding two functions to manage special bblock case - adding movz size specifications
* | | Removing OrigAsmgen by moving the necessary functions in Asmgen.v Léo Gourdin2020-11-253-285/+80
| | |
* | | Preservation proof with post pass scheduling in Asmgenproof almost doneLéo Gourdin2020-11-252-14/+14
| | |
* | | Restoring asmgenproof on multiple labels issueLéo Gourdin2020-11-242-176/+29
| | |
* | | Main part of postpasssch proof now completedLéo Gourdin2020-11-247-3884/+108
| | |
* | | Asmblockdeps is now finishedLéo Gourdin2020-11-241-226/+42
| | |
* | | Start of the postpasschedproof, redefining verify schedule lemmasLéo Gourdin2020-11-234-172/+272
| | |
* | | a step forward in bblock_simu_reduceSylvain Boulmé2020-11-231-40/+34
| | |
* | | Trying to finish the bisimu reduce proof for builtin (last case admitted)Léo Gourdin2020-11-202-30/+77
| | |
* | | draft of the exec_bblock Asmblockdeps proofLéo Gourdin2020-11-203-35/+137
| | |
* | | Postpass scheduling OKLéo Gourdin2020-11-183-323/+77
| | | | | | | | | | | | | | | | | | - Modifying Asmblockdeps to adapt to Pfmovimm new specification - Changing the Asmgenproof to adapt PArith in consequence - Modifying the oracle to specify correct wlocs - Cleaning everywhere
* | | fix the semantics ?Sylvain Boulmé2020-11-182-3/+11
| | |
* | | Merge remote-tracking branch 'origin/aarch64-postpass' into aarch64-postpassLéo Gourdin2020-11-171-7/+56
|\ \ \
| * | | extend the aarch64 scheduling verifier to check builtins.Sylvain Boulmé2020-11-171-7/+56
| | | | | | | | | | | | | | | | | | | | | | | | | | | | NB 1: the equality is purely syntactical on builtins. This should not be a limit for our scheduler. NB 2: the correctness proof remains to be done (only a skeleton is given).
* | | | Builtin mem spec in scheduler and some needed proof in Postpasssch.vLéo Gourdin2020-11-173-5/+6
|/ / /
* | | Remaining ctl insts except Pbuiltin (maps to error)Léo Gourdin2020-11-162-400/+538
| | |
* | | Lemma for bisimu with potential builtins, alloc and constantLéo Gourdin2020-11-131-65/+132
| | |
* | | Loads and stores opLéo Gourdin2020-11-132-31/+238
| | |
* | | Arith inst OK for the verifierLéo Gourdin2020-11-122-67/+227
| | |
* | | Verifier is now enabled with debug printsLéo Gourdin2020-11-111-7/+6
| | |
* | | Finishing PArith cases in abb, and linking the pass to compileLéo Gourdin2020-11-111-387/+479
| | |
* | | PArithCmpR0R in checkerLéo Gourdin2020-11-111-36/+130
| | |
* | | PArithComparison special lemmas and adaptationsLéo Gourdin2020-11-101-17/+315
| | |
* | | Simplifications using ltacs and XZR special caseLéo Gourdin2020-11-101-33/+150
| | |
* | | First version of the oracle checker, does not compile yetLéo Gourdin2020-11-093-837/+590
| | |
* | | Preparing the repo for debugging postpass and executing testsLéo Gourdin2020-11-062-31/+32
| | |
* | | set debug to false in oracleLéo Gourdin2020-11-051-1/+1
| | |
* | | A first (not well-tuned) working version of postpass scheduling for A64Léo Gourdin2020-11-052-1004/+1066
| | |
* | | Smart scheduler build problem and flatten solution OKLéo Gourdin2020-11-044-258/+374
| | |
* | | Dumb (identity) scheduling working and integratedLéo Gourdin2020-11-037-869/+2356
| | |
* | | Some adaptations on PostpassScheduling for aarch64, and defs in AsmblockLéo Gourdin2020-11-022-71/+47
| | |
* | | Author and stash single label Asmgenproof after mergeLéo Gourdin2020-11-022-0/+2246
| | |
* | | Merge branch 'aarch64_block_multiple_labels' into aarch64-postpassLéo Gourdin2020-11-022-28/+175
|\ \ \
| * | | Yarpgen C file to test multiple labels and corresponding codeLéo Gourdin2020-11-012-28/+175
| | | | | | | | | | | | In this branch I remove the multiple label limitation to pass some tests but the proof is admitted !
* | | | Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-0213-81/+5515
|/ / /
* | | End of Asmblock translationLéo Gourdin2020-10-291-38/+36
| | |
* | | Bugfix in AsmgenLéo Gourdin2020-10-291-1/+1
| | |
* | | Found a bug in Asmgen about iregsp constructorLéo Gourdin2020-10-291-9/+9
| | |
* | | Some tests and load/store instrLéo Gourdin2020-10-291-26/+145
| | |
* | | If, op, and some tests with a scriptLéo Gourdin2020-10-281-6/+701
| | |
* | | Epilogue OK and loadimmLéo Gourdin2020-10-271-58/+96
| | |
* | | Merge remote-tracking branch 'origin/aarch64_asmblockgen' into aarch64_blockLéo Gourdin2020-10-271-47/+52
|\ \ \
| * | | another start for AsmblockgenSylvain Boulmé2020-10-271-131/+52
| | | |
* | | | A more convenient way to handle basic instLéo Gourdin2020-10-271-99/+18
|/ / /
generated by cgit (git 2.34.1) at 2024-07-11 23:07:58 +0000