aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof.v
Commit message (Collapse)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
|\ | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-6/+6
| | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
| * AArch64: macOS portXavier Leroy2020-12-261-1/+1
| | | | | | | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
* | 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 ↵Léo Gourdin2020-12-201-21/+11
|\ \ | | | | | | | | | aarch64-peephole
| * | 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
| | | | | | | | | | | | | | | | | | | | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
* | | | 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
| | | | | | | | | This commit prepare the backend for a peephole optimization in Asmblock.
* | | 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
| | | | | | | | | | | | Also some simplifications in Asmblockdeps
| * | | Fine tuning for PfmovimmLéo Gourdin2020-11-261-6/+9
| | | | | | | | | | | | | | | | - Functions to check a float logical immediate were translated from ocaml target printer in coq Asmblock - Some proof are admitted for now (we'll see if it is a good idea after some tests)
* | | | 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
| | | | | | | | | | | | | | | | | | - Modifying Asmblockdeps to adapt to Pfmovimm new specification - Changing the Asmgenproof to adapt PArith in consequence - Modifying the oracle to specify correct wlocs - Cleaning everywhere
* | | 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
| | | | | | | | | | | | In this branch I remove the multiple label limitation to pass some tests but the proof is admitted !
* | | | 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
| | | | | | | | | | | | 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.
* | | 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
| | | | | | | | | | | | | | | | | | | | | | | | * Deleting the (duplicated) length_agree lemma (there was an equivalent lemma named list_length_z_nat for this purpose) * Lemmas about labels : * label_in_header_list * no_label_in_basic_inst * label_pos_body * label_pos_preserved_gen and label_pos_preserved
* | | Merge remote-tracking branch 'origin/aarch64_block_bodystar' into ↵Léo Gourdin2020-10-161-222/+114
|\ \ \ | | | | | | | | | | | | aarch64_block_bodystar
| * | | 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
| | | | | | | | | | | | | | | | | | - New ltacs - simplifications - new subcases - two lemmas for nextinstr agree
generated by cgit (git 2.34.1) at 2024-05-20 07:35:14 +0000