aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
Commit message (Collapse)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 ↵Léo Gourdin2020-12-201-0/+18
|\ | | | | | | aarch64-peephole
| * 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
| | | This commit prepare the backend for a peephole optimization in Asmblock.
* Proof of Pfmovimm fine tuned OK, moving float checks in AsmLéo Gourdin2020-11-261-33/+0
| | | Also some simplifications in Asmblockdeps
* Fine tuning for PfmovimmLéo Gourdin2020-11-261-1/+35
| | | | - Functions to check a float logical immediate were translated from ocaml target printer in coq Asmblock - Some proof are admitted for now (we'll see if it is a good idea after some tests)
* 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
| | | | 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.
* Simplifying Ltac and fixing a bug in AsmBlock semanticsLéo Gourdin2020-10-131-1/+1
| | | The bug was a typo on the PArithPPP subl inst
* Prove exec_body_dont_move_PCJustus Fasse2020-08-181-32/+39
| | | | | | Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be a misnomer since not all iregs are data regs) TODO: Adjust names of PArithP, PArithPP and the like
* backward decomposition of the proofSylvain Boulmé2020-07-221-1/+1
|
* Generate both Pcsel and PfselJustus Fasse2020-07-131-1/+1
| | | | | | | In Asmblock, Pcsel is used for both integer and floating-point conditional selection. A previous commit (c764ff84) had incorrectly reverted the merging of Pfsel into Pcsel.
* fix size of block in AsmblockSylvain Boulmé2020-07-101-5/+2
| | | | Due to the fact that, at the Asm level, Plabel runs PC++
* 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
| | | | This everts commits 91f991ab and df253300
* Asmblock.dreg: Use option (monad) for dealing with instruction sizesJustus Fasse2020-07-081-39/+62
| | | | | This makes it more clear, and explicit, when we care about the expected register width for an instruction in case an ireg0 will be used.
* Regroup ar_instructions by access to "data" registers (dreg)Justus Fasse2020-07-081-113/+128
| | | | | | | | | | | | | | | A dreg is either a floating poing, integer register, SP, or XZR. This way we can combine a few more varaints in ar_instruction. However, now every dreg case has to deal with the complications of ireg0 by giving, for every instruction, the expected integer register width if it were to use an ireg0. Right now instructions that do not care about this, because the instructions in aarch64/Asm do not use an ireg0, return W and simply should not hit the XZR case. Also causes a warning due to ambiguous coercions: ireg coerces to both ireg0 and iregsp, and both of those coerce to dreg.
* 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
| | | | (since the grouping instructions by pregs)
* 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 ↵Sylvain Boulmé2020-07-061-28/+20
| | | | arith_comparison_r0r
* 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-20 11:35:16 +0000