aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/aarch64_Pfmovimm_fix' into aarch64-postpassLéo Gourdin2020-11-181-2/+2
|\
| * fix spec of Pfmovimmd/s on aarch64Sylvain Boulmé2020-11-181-2/+2
* | 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
* | | 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
* | | 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
|/ /
* | [Draft] Flattened levels of binstLéo Gourdin2020-10-271-49/+180
* | [Draft] Problems with coercionsLéo Gourdin2020-10-261-1078/+166
* | Asm gen proof for aarch64 from Asmblock is complete.Léo Gourdin2020-10-231-116/+35
* | Merge remote-tracking branch 'origin/aarch64_block' into aarch64_blockLéo Gourdin2020-10-239-612/+961
|\ \
| * | aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-239-612/+961
* | | [Draft] some lemmas copied for undef_regs.Léo Gourdin2020-10-231-27/+73
|/ /
* | [Draft] Improvements on buitin cfi proof and new lemmas for set_res.Léo Gourdin2020-10-221-1/+143
* | Adding buitin_args lemmasLéo Gourdin2020-10-213-24/+68
* | update commentsLéo Gourdin2020-10-201-17/+14
* | cfi_simu finishedLéo Gourdin2020-10-201-15/+36
* | exec_body_simulation_plus_gen proof OKLéo Gourdin2020-10-201-11/+35
* | New lemmas and subcases for cfi_simuLéo Gourdin2020-10-191-49/+68
* | Some subcases for exec cfi simuLéo Gourdin2020-10-191-95/+68
* | Typo in label_pos_preserved hypLéo Gourdin2020-10-191-2/+1
* | Improvements in AsmgenproofLéo Gourdin2020-10-191-32/+111
* | Merge remote-tracking branch 'origin/aarch64_block_bodystar' into aarch64_blo...Léo Gourdin2020-10-161-222/+114
|\ \
generated by cgit (git 2.34.1) at 2024-06-13 13:10:29 +0000