aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* aarch64/Asmblock: Merge PArithComparisonRR and PArithComparisonFFJustus Fasse2020-07-061-21/+11
|
* aarch64/Asmblock: Merge RR, RF, FR, FF, RspRspJustus Fasse2020-07-061-85/+41
|
* aarch64/Asmblock: Merge arith_comparison_(r|f)Justus Fasse2020-07-061-26/+12
|
* aarch64/Asmblock: Switch arith_c_r to arith_c_p for consistencyJustus Fasse2020-07-061-4/+4
|
* aarch64/Asmblock: Merge arith_r and arith_f into arith_pJustus Fasse2020-07-061-19/+10
|
* aarch64/Asmblock: Change preg to simplify preg-ificationJustus Fasse2020-07-061-10/+12
| | | | | | | | | | | | | Since ireg and iregsp coerces to preg, and iregsp subsumes ireg define preg's IR constructor with iregsp and remove SP. This is the first step in the "preg-ification" of aarch64/Asmblock. The goal is to unify instructions that only differ in the types of registers they use. That is, we want to group together instructions e.g. `rd <- op r1 ...` even if r1 is ireg for one op and freg for another operation. (NB: This currently excludes operations that use ireg0 which will are and will be grouped separately for now.)
* Asmblock: Rename arith_name_<...> -> arith_name_<...>Justus Fasse2020-07-051-62/+62
| | | | | Following the example of 6fd50b46 where arith_name_r was renamed to arith_r
* Asmblock: Use i as variable name for instructionsJustus Fasse2020-07-051-73/+73
|
* Asmblock: Add instructions with conditional executionJustus Fasse2020-07-051-6/+41
|
* Asmblock: PArithWRR0I -> PArithWRR0, PArithXRR0I -> PArithXRR0Justus Fasse2020-07-041-22/+22
|
* Asmblock: Merge PArithFF32 and PArithFF64 into PArithFJustus Fasse2020-07-041-19/+9
|
* Asmblock: Add TODO for instructions I had previously forgottenJustus Fasse2020-07-041-0/+3
|
* Asmblock: PArithRspRspI -> PArithRspRspJustus Fasse2020-07-041-11/+11
|
* Asmblock: PArithComparisonRI -> PArithComparisonRJustus Fasse2020-07-041-17/+17
| | | | | Reflects the fact that immediates are not really relevant as scheduling dependencies.
* fixing type of PLoad and PStoreSylvain Boulmé2020-07-031-3/+3
|
* Merging arith_name_r and arith_name_ri into arith_rSylvain Boulmé2020-07-031-24/+18
|
* Asmblock: Add floating-point load and storesJustus Fasse2020-07-021-4/+24
| | | | | | Since exec_load and exec_store are defined with preg (not ireg or freg) I simply appended the floating point instructions to the already defined types and functions.
* Asmblock: First attempt at completing PArith/ar_instruction/...Justus Fasse2020-07-021-38/+626
| | | | | Pmovk is currently missing. (Pmovk aloways uses a register as both source and desintation)
* aarch64/Asmblock: Add PStore, based on PLoadJustus Fasse2020-06-281-1/+28
|
* fix linker model in AsmblockSylvain Boulmé2020-06-221-30/+10
|
* [WIP: Coq compilation broken] Stub for AsmgenSylvain Boulmé2020-06-211-5/+9
|
* Skeleton of AsmblockSylvain Boulmé2020-06-201-82/+136
|
generated by cgit (git 2.34.1) at 2024-07-14 09:41:21 +0000