Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Passing info of live regs to scheduler: beginning | nicolas.nardino | 2021-06-04 | 1 | -0/+1 |
| | |||||
* | Adding fp loads pair | Léo Gourdin | 2021-01-20 | 1 | -4/+4 |
| | |||||
* | Big improvment in peephole, changing LDP/STP semantics | Léo Gourdin | 2020-12-10 | 1 | -124/+69 |
| | |||||
* | a first working draft on ldp/stp peephole | Léo Gourdin | 2020-12-04 | 1 | -3/+25 |
| | |||||
* | Adding semantics for Pldp | Léo Gourdin | 2020-12-02 | 1 | -3/+16 |
| | | | This commit prepare the backend for a peephole optimization in Asmblock. | ||||
* | add option in scheduler to record bb size | Léo Gourdin | 2020-11-30 | 1 | -0/+5 |
| | |||||
* | Changing weights system at asmblock level instead of asm | Léo Gourdin | 2020-11-30 | 1 | -240/+71 |
| | |||||
* | Main part of postpasssch proof now completed | Léo Gourdin | 2020-11-24 | 1 | -1/+5 |
| | |||||
* | Postpass scheduling OK | Léo Gourdin | 2020-11-18 | 1 | -146/+13 |
| | | | | | | - 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 | ||||
* | Builtin mem spec in scheduler and some needed proof in Postpasssch.v | Léo Gourdin | 2020-11-17 | 1 | -1/+1 |
| | |||||
* | Remaining ctl insts except Pbuiltin (maps to error) | Léo Gourdin | 2020-11-16 | 1 | -31/+45 |
| | |||||
* | Loads and stores op | Léo Gourdin | 2020-11-13 | 1 | -26/+35 |
| | |||||
* | Arith inst OK for the verifier | Léo Gourdin | 2020-11-12 | 1 | -6/+36 |
| | |||||
* | Preparing the repo for debugging postpass and executing tests | Léo Gourdin | 2020-11-06 | 1 | -4/+4 |
| | |||||
* | set debug to false in oracle | Léo Gourdin | 2020-11-05 | 1 | -1/+1 |
| | |||||
* | A first (not well-tuned) working version of postpass scheduling for A64 | Léo Gourdin | 2020-11-05 | 1 | -714/+713 |
| | |||||
* | Smart scheduler build problem and flatten solution OK | Léo Gourdin | 2020-11-04 | 1 | -237/+245 |
| | |||||
* | Dumb (identity) scheduling working and integrated | Léo Gourdin | 2020-11-03 | 1 | -858/+753 |
| | |||||
* | Preparation for postpass in aarch64 and refactoring | Léo Gourdin | 2020-11-02 | 1 | -0/+1029 |