Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 1 | -1/+1 |
| | |||||
* | Cleanup | Léo Gourdin | 2020-12-19 | 1 | -46/+0 |
| | |||||
* | Some progress in Asmblockgenproof | Léo Gourdin | 2020-12-17 | 1 | -14/+15 |
| | |||||
* | intermediatet commit before builtins | Léo Gourdin | 2020-12-16 | 1 | -6/+9 |
| | |||||
* | Generals lemmas for asmblockgenproof | Léo Gourdin | 2020-12-14 | 1 | -12/+28 |
| | |||||
* | Removing the PseudoAsm IR | Léo Gourdin | 2020-12-13 | 1 | -10/+29 |
| | |||||
* | Some cleanup in todos | Léo Gourdin | 2020-12-07 | 1 | -12/+0 |
| | |||||
* | a first working draft on ldp/stp peephole | Léo Gourdin | 2020-12-04 | 1 | -16/+16 |
| | |||||
* | Adding semantics for Pldp | Léo Gourdin | 2020-12-02 | 1 | -18/+18 |
| | | | This commit prepare the backend for a peephole optimization in Asmblock. | ||||
* | Fixing a generation bug on shrx in Asmblockgen | Léo Gourdin | 2020-11-26 | 1 | -0/+6 |
| | | | I forgot this one and the gen test script reminds me | ||||
* | This commit fix the issue #226 | Léo Gourdin | 2020-11-26 | 1 | -50/+57 |
| | | | | - adding two functions to manage special bblock case - adding movz size specifications | ||||
* | Preparation for postpass in aarch64 and refactoring | Léo Gourdin | 2020-11-02 | 1 | -20/+20 |
| | |||||
* | End of Asmblock translation | Léo Gourdin | 2020-10-29 | 1 | -38/+36 |
| | |||||
* | Some tests and load/store instr | Léo Gourdin | 2020-10-29 | 1 | -26/+145 |
| | |||||
* | If, op, and some tests with a script | Léo Gourdin | 2020-10-28 | 1 | -6/+701 |
| | |||||
* | Epilogue OK and loadimm | Léo Gourdin | 2020-10-27 | 1 | -58/+96 |
| | |||||
* | Merge remote-tracking branch 'origin/aarch64_asmblockgen' into aarch64_block | Léo Gourdin | 2020-10-27 | 1 | -47/+52 |
|\ | |||||
| * | another start for Asmblockgen | Sylvain Boulmé | 2020-10-27 | 1 | -131/+52 |
| | | |||||
* | | A more convenient way to handle basic inst | Léo Gourdin | 2020-10-27 | 1 | -99/+18 |
|/ | |||||
* | [Draft] Flattened levels of binst | Léo Gourdin | 2020-10-27 | 1 | -49/+180 |
| | |||||
* | [Draft] Problems with coercions | Léo Gourdin | 2020-10-26 | 1 | -1078/+166 |
| | |||||
* | aarch64 compiles again (but ccomp generates incorrect assembly) | Sylvain Boulmé | 2020-10-23 | 1 | -6/+74 |
| | |||||
* | [WIP: Coq compilation broken] Stub for Asmgen | Sylvain Boulmé | 2020-06-21 | 1 | -0/+1197 |