aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
...
* | | 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
|/ / /
* | | [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
| | | | | | | | | | | | There was an issue with the register PC in the eval_BA constructor for builtin : we were not able to prove that the concerned reg was different from PC. This commit modify the definitions in Asmgen and Asmblock to support this, by replacing the parameter with a dreg instead of a preg.
* | | 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
| | | | | | | | | | | | | | | | | | | | | | | | * Deleting the (duplicated) length_agree lemma (there was an equivalent lemma named list_length_z_nat for this purpose) * Lemmas about labels : * label_in_header_list * no_label_in_basic_inst * label_pos_body * label_pos_preserved_gen and label_pos_preserved
* | | Merge remote-tracking branch 'origin/aarch64_block_bodystar' into ↵Léo Gourdin2020-10-161-222/+114
|\ \ \ | | | | | | | | | | | | aarch64_block_bodystar
| * | | 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
|/ / /
generated by cgit (git 2.34.1) at 2024-07-12 05:50:41 +0000