Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Prove exec_body_dont_move_PC | Justus Fasse | 2020-08-18 | 1 | -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 proof | Sylvain Boulmé | 2020-07-22 | 1 | -1/+1 |
| | |||||
* | Generate both Pcsel and Pfsel | Justus Fasse | 2020-07-13 | 1 | -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 Asmblock | Sylvain Boulmé | 2020-07-10 | 1 | -5/+2 |
| | | | | Due to the fact that, at the Asm level, Plabel runs PC++ | ||||
* | Remove incorrect part of a comment | Justus Fasse | 2020-07-09 | 1 | -2/+1 |
| | |||||
* | Switch back to specific registers for specific (inlined) instruction | Justus Fasse | 2020-07-09 | 1 | -1/+1 |
| | |||||
* | Revert introduction of dreg | Justus Fasse | 2020-07-08 | 1 | -158/+120 |
| | | | | This everts commits 91f991ab and df253300 | ||||
* | Asmblock.dreg: Use option (monad) for dealing with instruction sizes | Justus Fasse | 2020-07-08 | 1 | -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 Fasse | 2020-07-08 | 1 | -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_instruction | Justus Fasse | 2020-07-07 | 1 | -14/+4 |
| | |||||
* | Inline Pcsel in ar_instruction | Justus Fasse | 2020-07-07 | 1 | -28/+5 |
| | |||||
* | Inline Pfmovi in ar_instruction | Justus Fasse | 2020-07-07 | 1 | -24/+5 |
| | |||||
* | Inline Pcset in ar_instruction | Justus Fasse | 2020-07-07 | 1 | -16/+4 |
| | |||||
* | Remove out-of-date comment | Justus Fasse | 2020-07-07 | 1 | -1/+0 |
| | |||||
* | Remove Pfsel which is currently identical to Pcsel | Justus Fasse | 2020-07-07 | 1 | -3/+1 |
| | | | | (since the grouping instructions by pregs) | ||||
* | Merge PArith(SW|DX)FR0 | Justus Fasse | 2020-07-07 | 1 | -17/+13 |
| | |||||
* | Merge PArith(W|X)RR0 and PArith(W|X)ARRRR0 | Justus Fasse | 2020-07-07 | 1 | -47/+30 |
| | |||||
* | introduce if_opt_bool_val. | Sylvain Boulmé | 2020-07-06 | 1 | -7/+12 |
| | |||||
* | intermediate comparison function on arit_comparison_* | Sylvain Boulmé | 2020-07-06 | 1 | -11/+17 |
| | |||||
* | merging arith_comparison_w_r0r and arith_comparison_x_r0r into ↵ | Sylvain Boulmé | 2020-07-06 | 1 | -28/+20 |
| | | | | arith_comparison_r0r | ||||
* | unifying arith_w_rr0r and arith_x_rr0r into arith_rr0r | Sylvain Boulmé | 2020-07-06 | 1 | -51/+42 |
| | |||||
* | aarch64/Asmblock: Move Pmovk to arith_pp | Justus Fasse | 2020-07-06 | 1 | -5/+5 |
| | |||||
* | aarch64/Asmblock: Change PArithAFFF to PArithPPP for consistency | Justus Fasse | 2020-07-06 | 1 | -16/+17 |
| | |||||
* | aarch64/Asmblock: Merge PArithCRRR and PArithCFFF | Justus Fasse | 2020-07-06 | 1 | -23/+12 |
| | |||||
* | aarch64/Asmblock: Merge PArithRRR, PArithRspRspR and PArithFFF | Justus Fasse | 2020-07-06 | 1 | -41/+22 |
| | |||||
* | aarch64/Asmblock: Merge PArithComparisonRR and PArithComparisonFF | Justus Fasse | 2020-07-06 | 1 | -21/+11 |
| | |||||
* | aarch64/Asmblock: Merge RR, RF, FR, FF, RspRsp | Justus Fasse | 2020-07-06 | 1 | -85/+41 |
| | |||||
* | aarch64/Asmblock: Merge arith_comparison_(r|f) | Justus Fasse | 2020-07-06 | 1 | -26/+12 |
| | |||||
* | aarch64/Asmblock: Switch arith_c_r to arith_c_p for consistency | Justus Fasse | 2020-07-06 | 1 | -4/+4 |
| | |||||
* | aarch64/Asmblock: Merge arith_r and arith_f into arith_p | Justus Fasse | 2020-07-06 | 1 | -19/+10 |
| | |||||
* | aarch64/Asmblock: Change preg to simplify preg-ification | Justus Fasse | 2020-07-06 | 1 | -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 Fasse | 2020-07-05 | 1 | -62/+62 |
| | | | | | Following the example of 6fd50b46 where arith_name_r was renamed to arith_r | ||||
* | Asmblock: Use i as variable name for instructions | Justus Fasse | 2020-07-05 | 1 | -73/+73 |
| | |||||
* | Asmblock: Add instructions with conditional execution | Justus Fasse | 2020-07-05 | 1 | -6/+41 |
| | |||||
* | Asmblock: PArithWRR0I -> PArithWRR0, PArithXRR0I -> PArithXRR0 | Justus Fasse | 2020-07-04 | 1 | -22/+22 |
| | |||||
* | Asmblock: Merge PArithFF32 and PArithFF64 into PArithF | Justus Fasse | 2020-07-04 | 1 | -19/+9 |
| | |||||
* | Asmblock: Add TODO for instructions I had previously forgotten | Justus Fasse | 2020-07-04 | 1 | -0/+3 |
| | |||||
* | Asmblock: PArithRspRspI -> PArithRspRsp | Justus Fasse | 2020-07-04 | 1 | -11/+11 |
| | |||||
* | Asmblock: PArithComparisonRI -> PArithComparisonR | Justus Fasse | 2020-07-04 | 1 | -17/+17 |
| | | | | | Reflects the fact that immediates are not really relevant as scheduling dependencies. | ||||
* | fixing type of PLoad and PStore | Sylvain Boulmé | 2020-07-03 | 1 | -3/+3 |
| | |||||
* | Merging arith_name_r and arith_name_ri into arith_r | Sylvain Boulmé | 2020-07-03 | 1 | -24/+18 |
| | |||||
* | Asmblock: Add floating-point load and stores | Justus Fasse | 2020-07-02 | 1 | -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 Fasse | 2020-07-02 | 1 | -38/+626 |
| | | | | | Pmovk is currently missing. (Pmovk aloways uses a register as both source and desintation) | ||||
* | aarch64/Asmblock: Add PStore, based on PLoad | Justus Fasse | 2020-06-28 | 1 | -1/+28 |
| | |||||
* | fix linker model in Asmblock | Sylvain Boulmé | 2020-06-22 | 1 | -30/+10 |
| | |||||
* | [WIP: Coq compilation broken] Stub for Asmgen | Sylvain Boulmé | 2020-06-21 | 1 | -5/+9 |
| | |||||
* | Skeleton of Asmblock | Sylvain Boulmé | 2020-06-20 | 1 | -82/+136 |
| | |||||
* | start aarch64/Asmblock (work-in-progress) | Sylvain Boulmé | 2020-06-19 | 1 | -0/+1546 |