aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblockdeps.v
Commit message (Expand)AuthorAgeFilesLines
* Adding fp stores pairLéo Gourdin2021-01-201-6/+12
* Adding fp loads pairLéo Gourdin2021-01-201-13/+30
* Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-6/+6
* Fix the Asmblock/Asm proofLéo Gourdin2020-12-201-7/+7
* Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-1/+3
* Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-101-92/+110
* Asmgen proof completely proved with ldp/stpLéo Gourdin2020-12-061-2/+3
* a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-52/+227
* Adding semantics for PldpLéo Gourdin2020-12-021-33/+38
* Some optimizations againLéo Gourdin2020-11-281-27/+30
* Optimizing Asmblockdeps proofLéo Gourdin2020-11-281-58/+92
* Proof of Pfmovimm fine tuned OK, moving float checks in AsmLéo Gourdin2020-11-261-240/+96
* Fine tuning for PfmovimmLéo Gourdin2020-11-261-3/+5
* Main part of postpasssch proof now completedLéo Gourdin2020-11-241-1/+1
* Asmblockdeps is now finishedLéo Gourdin2020-11-241-226/+42
* Start of the postpasschedproof, redefining verify schedule lemmasLéo Gourdin2020-11-231-36/+42
* 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-201-29/+76
* draft of the exec_bblock Asmblockdeps proofLéo Gourdin2020-11-201-29/+116
* Postpass scheduling OKLéo Gourdin2020-11-181-164/+29
* 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-171-2/+2
|/
* Remaining ctl insts except Pbuiltin (maps to error)Léo Gourdin2020-11-161-369/+493
* Lemma for bisimu with potential builtins, alloc and constantLéo Gourdin2020-11-131-65/+132
* Loads and stores opLéo Gourdin2020-11-131-5/+203
* Arith inst OK for the verifierLéo Gourdin2020-11-121-61/+191
* 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-091-832/+576
* Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-021-0/+1841
generated by cgit (git 2.34.1) at 2024-05-09 10:54:01 +0000