aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof.v
Commit message (Collapse)AuthorAgeFilesLines
* aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-8/+9
|
* [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
* Some subcases for exec_basic_simuLéo Gourdin2020-10-141-86/+49
| | | | | | | - Ploadsymbol - Pcvtsw2x - Pcvtuw2x - Pcvtx2w - First subcase for PArithCompPP
* an idea to tackle PArithComparisonPPSylvain Boulmé2020-10-141-2/+43
|
* draft commit for the Pallocframe proof subcaseLéo Gourdin2020-10-141-2/+15
|
* Pstore preserved lemmaLéo Gourdin2020-10-141-3/+64
|
* Other subcases for PArith are done.Léo Gourdin2020-10-141-8/+29
|
* Draft commit on the PArithComparisonPP ProofLéo Gourdin2020-10-141-14/+72
| | | in exec_basic_simulation
* Simplifying Ltac and fixing a bug in AsmBlock semanticsLéo Gourdin2020-10-131-10/+30
| | | The bug was a typo on the PArithPPP subl inst
* Fixing the propagation of the new BOUNDED hypLéo Gourdin2020-10-131-8/+20
|
* Proof for PmovzLéo Gourdin2020-10-131-7/+29
| | | Adding Ltac to simplify code and improve readability
* Adding a lemma next_instr_preservedLéo Gourdin2020-10-121-7/+56
| | | this is useful in the exec_basic_simu proof
* Continue the proof of exec_basic_simulationLéo Gourdin2020-10-111-18/+12
|
* Adding a lemma for exec load propagation.Léo Gourdin2020-10-111-25/+27
| | | | The commit also contains an incomplete proof for assert (BDYLENPOS: ((length li) < length (body bb))%nat).
* Merge branch 'aarch64_block_bodystar' of ↵Léo Gourdin2020-10-101-10/+14
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64_block_bodystar
| * Merge branch 'aarch64_block_bodystar' of ↵Sylvain Boulmé2020-10-101-0/+14
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64_block_bodystar
| * | Still generalizing exec_body_simulation_plus for an inductive proofSylvain Boulmé2020-10-091-10/+14
| | | | | | | | | | | | This will require some lemma about is_tail...
* | | More general version of load preservation lemma.Léo Gourdin2020-10-101-7/+25
| |/ |/| | | | | Problem with the ptr bounds.
* | Adding a lemma for load preservationLéo Gourdin2020-10-101-0/+14
|/ | | | This is a test lemma, I may remove the exists predicate later.
* slight refactoring, in order to avoid a duplication of the proof.Sylvain Boulmé2020-10-091-40/+36
|
* exec_body_simulation without star'Léo Gourdin2020-10-091-0/+101
|
* Replace common pattern with simpler lemma.Justus Fasse2020-09-211-29/+16
| | | | | Turns two rewrites and a simplification into a single rewrite via list_length_z_cons.
* Proof of exec_body_simulation_plusJustus Fasse2020-09-211-1/+238
| | | | | | | | | | | Added exec_body_simulation_star' in order to prove it. exec_body_simulation_star' could also be used to prove exec_body_simulation_star directly (without using exec_body_simulation_plus). However, at least the way I did it the proof turns out to be longer. eexec_body_simulation_plus is still required/useful for exec_bblock_simulation.
* Move a couple of lemmas up in the fileJustus Fasse2020-09-211-68/+68
|
* Admitted lemma for exec_basic_simulation.Justus Fasse2020-09-211-0/+9
| | | | Probably still missing a couple of assumptions.
* Prove exec_body_dont_move_PCJustus Fasse2020-08-181-1/+64
| | | | | | 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
* Proof for size_of_blocks_max_posJustus Fasse2020-08-051-18/+50
|
* Minor cleanup of find_instr_bblockJustus Fasse2020-07-301-11/+10
| | | | | | | | - Remove one auto-generated name - Move assertion on n's size up - Clear unnecessary hypothesis (iirc generalize worked better than exploit here) - Rewrite progress of Asm.find_instr only in the case that needs it
* Complete proof of find_instr_bblockJustus Fasse2020-07-301-3/+30
| | | | Cleanup is still TODO
* Absurd case in find_instr_bblockJustus Fasse2020-07-301-1/+107
| | | | | n points to neither label nor basic instruction but there is also no final exit instruction
* Prove find_instr_bblock_tailJustus Fasse2020-07-301-2/+89
|
* Simplify unfold_bblock and complete unfold_body's case in find_instr_bblockJustus Fasse2020-07-291-3/+74
| | | | | | | The previous version of unfold_bblock was copied from kvx/Asm.v. kvx's version is slightly different in that for the (here removed) special case it does not put a semicolon to separate bundles. Since aarch64 does not have kvx's bundles the two versions should be equivalent.
* Find label in base case of find_instr_bblockJustus Fasse2020-07-281-2/+18
|
* Messy progress on builtin-case of exec_exit_simulation_plusJustus Fasse2020-07-281-10/+25
|
* Messy progress on exec_exit_simulation_plusJustus Fasse2020-07-281-3/+27
| | | | | Proves exec_exit_simulation_plus for cf_instruction (as opposed to builtins)
generated by cgit (git 2.34.1) at 2024-07-14 09:26:05 +0000