aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | Implement unfold function from Asmblock to AsmJustus Fasse2020-07-091-2/+299
* | 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
* | Merge branch 'aarch64-asmblock-pregification' into aarch64_blockJustus Fasse2020-07-062-246/+142
|\ \
| * | aarch64/Asm: Fix `Error: Pattern "PC" is redundant in this clause.`Justus Fasse2020-07-061-1/+1
| * | 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
|/ /
* | Asmblock: Rename arith_name_<...> -> arith_name_<...>Justus Fasse2020-07-051-62/+62
* | 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
* | 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
* | Asmblock: First attempt at completing PArith/ar_instruction/...Justus Fasse2020-07-021-38/+626
* | aarch64/Asmblock: Add PStore, based on PLoadJustus Fasse2020-06-281-1/+28
* | fix linker model in AsmblockSylvain Boulmé2020-06-223-33/+31
* | restauring Coq compilation with STUBSSylvain Boulmé2020-06-226-7/+198
* | Compiler.v in .gitignoreSylvain Boulmé2020-06-211-0/+1
* | [WIP: Coq compilation broken] Stub for AsmgenSylvain Boulmé2020-06-218-2768/+2370
* | Skeleton of AsmblockSylvain Boulmé2020-06-201-82/+136
* | start aarch64/Asmblock (work-in-progress)Sylvain Boulmé2020-06-192-2/+1549
* | fix configure for aarch64_blockSylvain Boulmé2020-06-191-2/+6