aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
...
* | | 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
|\ \ \
| * | | replace exec_body_simulation_star' by exec_body_simulation_plus_genSylvain Boulmé2020-10-161-222/+114
* | | | Pb, Pbc, and nextinst incrPC preserved lemmaLéo Gourdin2020-10-161-41/+79
|/ / /
* | | label and goto_label preserved lemmasLéo Gourdin2020-10-161-3/+51
* | | exec_basic_simulation proof OKLéo Gourdin2020-10-161-32/+23
* | | PArithComp subcases OKLéo Gourdin2020-10-161-110/+75
* | | Progress in exec_basic_simuLéo Gourdin2020-10-151-104/+148
* | | Some subcases for exec_basic_simuLéo Gourdin2020-10-141-86/+49
generated by cgit (git 2.34.1) at 2024-06-03 00:25:51 +0000