aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* fix aarch64 merge?Léo Gourdin2021-03-291-0/+2318
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-2318/+0
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-6/+6
| * AArch64: macOS portXavier Leroy2020-12-261-1/+1
* | Adding fp stores pairLéo Gourdin2021-01-201-2/+1
* | Adding fp loads pairLéo Gourdin2021-01-201-4/+6
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-145/+98
* | Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into aarch64-p...Léo Gourdin2020-12-201-21/+11
|\ \
| * | Removing the PseudoAsm IRLéo Gourdin2020-12-131-21/+11
* | | Fix the Asmblock/Asm proofLéo Gourdin2020-12-201-25/+17
* | | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-2/+14
|\ \ \
| * | | fix new register erasing scheme for AArch64David Monniaux2020-12-081-104/+40
| * | | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-081-4/+7
| |\ \ \ | | | |/ | | |/|
| | * | AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-061-4/+7
* | | | Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-101-15/+16
| |_|/ |/| |
* | | Some cleanup in todosLéo Gourdin2020-12-071-2/+0
* | | Asmgen proof completely proved with ldp/stpLéo Gourdin2020-12-061-46/+120
* | | a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-24/+26
* | | Adding semantics for PldpLéo Gourdin2020-12-021-10/+21
* | | Merge branch 'aarch64_Pfmovimm_tuning' into aarch64-postpassLéo Gourdin2020-11-261-1/+3
|\ \ \
| * | | Proof of Pfmovimm fine tuned OK, moving float checks in AsmLéo Gourdin2020-11-261-10/+9
| * | | Fine tuning for PfmovimmLéo Gourdin2020-11-261-6/+9
* | | | finish Asmgenproof.transf_program_correctSylvain Boulmé2020-11-261-5/+15
|/ / /
* | | Preservation proof with post pass scheduling in Asmgenproof almost doneLéo Gourdin2020-11-251-8/+9
* | | Restoring asmgenproof on multiple labels issueLéo Gourdin2020-11-241-172/+25
* | | Postpass scheduling OKLéo Gourdin2020-11-181-13/+35
* | | Dumb (identity) scheduling working and integratedLéo Gourdin2020-11-031-7/+11
* | | Merge branch 'aarch64_block_multiple_labels' into aarch64-postpassLéo Gourdin2020-11-021-24/+171
|\ \ \
| * | | Yarpgen C file to test multiple labels and corresponding codeLéo Gourdin2020-11-011-24/+171
* | | | Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-021-1/+2
|/ / /
* | | Asm gen proof for aarch64 from Asmblock is complete.Léo Gourdin2020-10-231-116/+35
* | | Merge remote-tracking branch 'origin/aarch64_block' into aarch64_blockLéo Gourdin2020-10-231-8/+9
|\ \ \
| * | | aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-8/+9
* | | | [Draft] some lemmas copied for undef_regs.Léo Gourdin2020-10-231-27/+73
|/ / /
* | | [Draft] Improvements on buitin cfi proof and new lemmas for set_res.Léo Gourdin2020-10-221-1/+143
* | | Adding buitin_args lemmasLéo Gourdin2020-10-211-19/+60
* | | update commentsLéo Gourdin2020-10-201-17/+14
* | | cfi_simu finishedLéo Gourdin2020-10-201-15/+36
* | | exec_body_simulation_plus_gen proof OKLéo Gourdin2020-10-201-11/+35
* | | New lemmas and subcases for cfi_simuLéo Gourdin2020-10-191-49/+68
* | | Some subcases for exec cfi simuLéo Gourdin2020-10-191-95/+68
* | | Typo in label_pos_preserved hypLéo Gourdin2020-10-191-2/+1
* | | Improvements in AsmgenproofLéo Gourdin2020-10-191-32/+111
* | | Merge remote-tracking branch 'origin/aarch64_block_bodystar' into aarch64_blo...Léo Gourdin2020-10-161-222/+114
|\ \ \
| * | | replace exec_body_simulation_star' by exec_body_simulation_plus_genSylvain Boulmé2020-10-161-222/+114
* | | | Pb, Pbc, and nextinst incrPC preserved lemmaLéo Gourdin2020-10-161-41/+79
|/ / /
* | | label and goto_label preserved lemmasLéo Gourdin2020-10-161-3/+51
* | | exec_basic_simulation proof OKLéo Gourdin2020-10-161-32/+23
* | | PArithComp subcases OKLéo Gourdin2020-10-161-110/+75
* | | Progress in exec_basic_simuLéo Gourdin2020-10-151-104/+148
generated by cgit (git 2.34.1) at 2024-05-09 08:29:30 +0000