aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
Commit message (Expand)AuthorAgeFilesLines
* replacing omega with lia in some fileLéo Gourdin2021-03-291-1/+2
* Adding fp stores pairLéo Gourdin2021-01-201-1/+2
* Adding fp loads pairLéo Gourdin2021-01-201-4/+7
* Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into aarch64-p...Léo Gourdin2020-12-201-0/+18
|\
| * Generals lemmas for asmblockgenproofLéo Gourdin2020-12-141-0/+2
| * Removing the PseudoAsm IRLéo Gourdin2020-12-131-0/+16
* | Fix the Asmblock/Asm proofLéo Gourdin2020-12-201-2/+2
* | Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-101-54/+49
|/
* Some cleanup in todosLéo Gourdin2020-12-071-609/+13
* Asmgen proof completely proved with ldp/stpLéo Gourdin2020-12-061-1/+1
* a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-43/+66
* Adding semantics for PldpLéo Gourdin2020-12-021-37/+67
* Proof of Pfmovimm fine tuned OK, moving float checks in AsmLéo Gourdin2020-11-261-33/+0
* Fine tuning for PfmovimmLéo Gourdin2020-11-261-1/+35
* Main part of postpasssch proof now completedLéo Gourdin2020-11-241-1/+2
* Trying to finish the bisimu reduce proof for builtin (last case admitted)Léo Gourdin2020-11-201-1/+1
* draft of the exec_bblock Asmblockdeps proofLéo Gourdin2020-11-201-5/+15
* fix the semantics ?Sylvain Boulmé2020-11-181-1/+9
* First version of the oracle checker, does not compile yetLéo Gourdin2020-11-091-0/+9
* Smart scheduler build problem and flatten solution OKLéo Gourdin2020-11-041-0/+7
* Some adaptations on PostpassScheduling for aarch64, and defs in AsmblockLéo Gourdin2020-11-021-0/+11
* Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-021-0/+1
* aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-528/+5
* Adding buitin_args lemmasLéo Gourdin2020-10-211-4/+7
* Simplifying Ltac and fixing a bug in AsmBlock semanticsLéo Gourdin2020-10-131-1/+1
* Prove exec_body_dont_move_PCJustus Fasse2020-08-181-32/+39
* backward decomposition of the proofSylvain Boulmé2020-07-221-1/+1
* Generate both Pcsel and PfselJustus Fasse2020-07-131-1/+1
* fix size of block in AsmblockSylvain Boulmé2020-07-101-5/+2
* Remove incorrect part of a commentJustus Fasse2020-07-091-2/+1
* Switch back to specific registers for specific (inlined) instructionJustus Fasse2020-07-091-1/+1
* Revert introduction of dregJustus Fasse2020-07-081-158/+120
* Asmblock.dreg: Use option (monad) for dealing with instruction sizesJustus Fasse2020-07-081-39/+62
* Regroup ar_instructions by access to "data" registers (dreg)Justus Fasse2020-07-081-113/+128
* Inline Pfnmul in ar_instructionJustus Fasse2020-07-071-14/+4
* Inline Pcsel in ar_instructionJustus Fasse2020-07-071-28/+5
* Inline Pfmovi in ar_instructionJustus Fasse2020-07-071-24/+5
* Inline Pcset in ar_instructionJustus Fasse2020-07-071-16/+4
* Remove out-of-date commentJustus Fasse2020-07-071-1/+0
* Remove Pfsel which is currently identical to PcselJustus Fasse2020-07-071-3/+1
* Merge PArith(SW|DX)FR0Justus Fasse2020-07-071-17/+13
* Merge PArith(W|X)RR0 and PArith(W|X)ARRRR0Justus Fasse2020-07-071-47/+30
* introduce if_opt_bool_val.Sylvain Boulmé2020-07-061-7/+12
* intermediate comparison function on arit_comparison_*Sylvain Boulmé2020-07-061-11/+17
* merging arith_comparison_w_r0r and arith_comparison_x_r0r into arith_comparis...Sylvain Boulmé2020-07-061-28/+20
* unifying arith_w_rr0r and arith_x_rr0r into arith_rr0rSylvain Boulmé2020-07-061-51/+42
* aarch64/Asmblock: Move Pmovk to arith_ppJustus Fasse2020-07-061-5/+5
* aarch64/Asmblock: Change PArithAFFF to PArithPPP for consistencyJustus Fasse2020-07-061-16/+17
* aarch64/Asmblock: Merge PArithCRRR and PArithCFFFJustus Fasse2020-07-061-23/+12
* aarch64/Asmblock: Merge PArithRRR, PArithRspRspR and PArithFFFJustus Fasse2020-07-061-41/+22
generated by cgit (git 2.34.1) at 2024-05-09 12:30:54 +0000