Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding fp stores pair | Léo Gourdin | 2021-01-20 | 1 | -6/+12 |
| | |||||
* | Adding fp loads pair | Léo Gourdin | 2021-01-20 | 1 | -13/+30 |
| | |||||
* | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 1 | -6/+6 |
| | |||||
* | Fix the Asmblock/Asm proof | Léo Gourdin | 2020-12-20 | 1 | -7/+7 |
| | |||||
* | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 1 | -1/+3 |
| | |||||
* | Big improvment in peephole, changing LDP/STP semantics | Léo Gourdin | 2020-12-10 | 1 | -92/+110 |
| | |||||
* | Asmgen proof completely proved with ldp/stp | Léo Gourdin | 2020-12-06 | 1 | -2/+3 |
| | |||||
* | a first working draft on ldp/stp peephole | Léo Gourdin | 2020-12-04 | 1 | -52/+227 |
| | |||||
* | Adding semantics for Pldp | Léo Gourdin | 2020-12-02 | 1 | -33/+38 |
| | | | This commit prepare the backend for a peephole optimization in Asmblock. | ||||
* | Some optimizations again | Léo Gourdin | 2020-11-28 | 1 | -27/+30 |
| | |||||
* | Optimizing Asmblockdeps proof | Léo Gourdin | 2020-11-28 | 1 | -58/+92 |
| | | | Proof is now two times faster (from 60 to 30 seconds) | ||||
* | Proof of Pfmovimm fine tuned OK, moving float checks in Asm | Léo Gourdin | 2020-11-26 | 1 | -240/+96 |
| | | | Also some simplifications in Asmblockdeps | ||||
* | Fine tuning for Pfmovimm | Léo Gourdin | 2020-11-26 | 1 | -3/+5 |
| | | | | - 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) | ||||
* | Main part of postpasssch proof now completed | Léo Gourdin | 2020-11-24 | 1 | -1/+1 |
| | |||||
* | Asmblockdeps is now finished | Léo Gourdin | 2020-11-24 | 1 | -226/+42 |
| | |||||
* | Start of the postpasschedproof, redefining verify schedule lemmas | Léo Gourdin | 2020-11-23 | 1 | -36/+42 |
| | |||||
* | a step forward in bblock_simu_reduce | Sylvain Boulmé | 2020-11-23 | 1 | -40/+34 |
| | |||||
* | Trying to finish the bisimu reduce proof for builtin (last case admitted) | Léo Gourdin | 2020-11-20 | 1 | -29/+76 |
| | |||||
* | draft of the exec_bblock Asmblockdeps proof | Léo Gourdin | 2020-11-20 | 1 | -29/+116 |
| | |||||
* | Postpass scheduling OK | Léo Gourdin | 2020-11-18 | 1 | -164/+29 |
| | | | | | | - 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 | ||||
* | Merge remote-tracking branch 'origin/aarch64-postpass' into aarch64-postpass | Léo Gourdin | 2020-11-17 | 1 | -7/+56 |
|\ | |||||
| * | extend the aarch64 scheduling verifier to check builtins. | Sylvain Boulmé | 2020-11-17 | 1 | -7/+56 |
| | | | | | | | | | | | | | | NB 1: the equality is purely syntactical on builtins. This should not be a limit for our scheduler. NB 2: the correctness proof remains to be done (only a skeleton is given). | ||||
* | | Builtin mem spec in scheduler and some needed proof in Postpasssch.v | Léo Gourdin | 2020-11-17 | 1 | -2/+2 |
|/ | |||||
* | Remaining ctl insts except Pbuiltin (maps to error) | Léo Gourdin | 2020-11-16 | 1 | -369/+493 |
| | |||||
* | Lemma for bisimu with potential builtins, alloc and constant | Léo Gourdin | 2020-11-13 | 1 | -65/+132 |
| | |||||
* | Loads and stores op | Léo Gourdin | 2020-11-13 | 1 | -5/+203 |
| | |||||
* | Arith inst OK for the verifier | Léo Gourdin | 2020-11-12 | 1 | -61/+191 |
| | |||||
* | Finishing PArith cases in abb, and linking the pass to compile | Léo Gourdin | 2020-11-11 | 1 | -387/+479 |
| | |||||
* | PArithCmpR0R in checker | Léo Gourdin | 2020-11-11 | 1 | -36/+130 |
| | |||||
* | PArithComparison special lemmas and adaptations | Léo Gourdin | 2020-11-10 | 1 | -17/+315 |
| | |||||
* | Simplifications using ltacs and XZR special case | Léo Gourdin | 2020-11-10 | 1 | -33/+150 |
| | |||||
* | First version of the oracle checker, does not compile yet | Léo Gourdin | 2020-11-09 | 1 | -832/+576 |
| | |||||
* | Preparation for postpass in aarch64 and refactoring | Léo Gourdin | 2020-11-02 | 1 | -0/+1841 |