aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
* Complete bblock_size_auxJustus Fasse2020-07-241-1/+24
* Complete bblock_size_aux_posJustus Fasse2020-07-241-1/+6
* proof of exec_header_simulationSylvain Boulmé2020-07-231-10/+91
* Complete bblock_non_emptyJustus Fasse2020-07-231-1/+10
* Remove trailing whitespaceJustus Fasse2020-07-221-6/+6
* Complete proof of exec_exit_simulation_starJustus Fasse2020-07-221-2/+10
* backward decomposition of the proofSylvain Boulmé2020-07-223-22/+167
* Add dynamically checked assumption to simplify AsmgenproofJustus Fasse2020-07-212-10/+24
* suggestion of simpler nameSylvain Boulmé2020-07-171-1/+1
* suggestion of translation from find_bblock to find_instrSylvain Boulmé2020-07-171-0/+22
* Less auto-generated namesJustus Fasse2020-07-151-36/+36
* First go at showing that translated cfi behave the sameJustus Fasse2020-07-151-0/+191
* Add lemma showing 1 <= Ptrofs.max_unsignedJustus Fasse2020-07-151-2/+8
* Miscellaneous lemmas that I used at some point while experimentingJustus Fasse2020-07-151-0/+84
* Add definition of match_internalJustus Fasse2020-07-151-0/+18
* "we must check that the generated code contains less than [2^32] instructions...Justus Fasse2020-07-151-2/+3
* Generate both Pcsel and PfselJustus Fasse2020-07-132-2/+13
* Revert back to original definition of match_statesJustus Fasse2020-07-121-172/+8
* fix size of block in AsmblockSylvain Boulmé2020-07-101-5/+2
* Change definition of match_statesJustus Fasse2020-07-101-8/+172
* Start AsmgenproofJustus Fasse2020-07-091-3/+69
* Finish proof of Lemma symbol_high_lowJustus Fasse2020-07-092-6/+11
* 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
* 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
generated by cgit (git 2.34.1) at 2024-07-14 13:21:24 +0000