Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Add option to set thresold and support for riscv | nicolas.nardino | 2021-06-17 | 1 | -2/+7 |
| | |||||
* | Now working, tests show a decrease in spillage | nicolas.nardino | 2021-06-16 | 2 | -59/+61 |
| | | | | | Should still find a proper way to treat the case mentioned in earlier commits | ||||
* | kinda fixed | nicolas.nardino | 2021-06-15 | 2 | -25/+57 |
| | | | | | | | | Spills are definitely reduced, but lots of arbitrary in there: See previous commit: need to determine what to do if pressure is too high but no schedulable instruction can reduce it. For now, advance time for at most 5 cycles, if still no suitable instruction, go back to CSP | ||||
* | fixing | nicolas.nardino | 2021-06-15 | 3 | -23/+109 |
| | | | | | Still need to find what to do when pressure is high but there are no instructions available that decrease it | ||||
* | was very wrong, fixing | nicolas.nardino | 2021-06-14 | 3 | -15/+72 |
| | |||||
* | scheduler written, need to test now | nicolas.nardino | 2021-06-14 | 1 | -17/+67 |
| | |||||
* | work on the scheduler | nicolas.nardino | 2021-06-12 | 2 | -40/+110 |
| | |||||
* | Work on new schedluer | nicolas.nardino | 2021-06-10 | 3 | -11/+101 |
| | | | | | | Renamed a test file, wrote function to compute pressure deltas, Still need to pass the info in some way; beginning of the actual scheduler function | ||||
* | Fix RTLpathScheduleraux.get_live_regs_entry | nicolas.nardino | 2021-06-08 | 1 | -2/+3 |
| | |||||
* | Add some tests | nicolas.nardino | 2021-06-08 | 1 | -1/+1 |
| | |||||
* | Adding debug info | nicolas.nardino | 2021-06-06 | 1 | -42/+53 |
| | |||||
* | Fixing scope error, and non-exhaustive pattern matching | nicolas.nardino | 2021-06-06 | 1 | -5/+6 |
| | |||||
* | function written, now needs testing | nicolas.nardino | 2021-06-05 | 1 | -10/+40 |
| | |||||
* | computing live regs at sb entry from its live output regs | nicolas.nardino | 2021-06-04 | 1 | -3/+21 |
| | |||||
* | Passing info of live regs to scheduler: beginning | nicolas.nardino | 2021-06-04 | 3 | -1/+13 |
| | |||||
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1 | Cyril SIX | 2021-06-01 | 7 | -31/+24 |
|\ | |||||
| * | Compatibilité Coq 8.13 | David Monniaux | 2021-04-28 | 3 | -8/+3 |
| | | |||||
| * | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVX | Cyril SIX | 2021-04-13 | 1 | -14/+16 |
| |\ | |||||
| | * | Code simplification of get_path_map (no functionality change) | Cyril SIX | 2021-01-26 | 1 | -14/+16 |
| | | | |||||
| * | | Remove flags | Léo Gourdin | 2021-04-09 | 1 | -3/+1 |
| | | | |||||
| * | | Important commit on expansions' mini CSE, and a draft for addptrofs | Léo Gourdin | 2021-04-06 | 2 | -5/+2 |
| | | | |||||
| * | | Remove first nop when doing expansion | Léo Gourdin | 2021-03-21 | 1 | -0/+1 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp | Léo Gourdin | 2021-03-06 | 2 | -5/+5 |
| |\ \ | |||||
| | * | | Adding a mini CSE pass in the expansion oracle | Léo Gourdin | 2021-03-06 | 2 | -4/+5 |
| | | | | |||||
| * | | | Adding fp init expansions | Léo Gourdin | 2021-03-02 | 1 | -3/+3 |
| | | | | |||||
| * | | | [Admitted checker] Oracle expansion for float/float32 constant init | Léo Gourdin | 2021-03-02 | 2 | -4/+4 |
| |/ / | |||||
* / / | replacing omega with lia in some file | Léo Gourdin | 2021-03-29 | 4 | -39/+43 |
|/ / | |||||
* | | fix ci ? | Léo Gourdin | 2021-03-02 | 1 | -1/+1 |
| | | |||||
* | | Try to save values in virtual registers during expansion | Léo Gourdin | 2021-03-01 | 1 | -1/+1 |
| | | |||||
* | | Proofs finished for expansion | Léo Gourdin | 2021-03-01 | 1 | -22/+6 |
| | | |||||
* | | Debugging fake values finished | Léo Gourdin | 2021-03-01 | 1 | -10/+19 |
| | | |||||
* | | proof of fsval_proj_correct | Sylvain Boulmé | 2021-03-01 | 1 | -7/+27 |
| | | |||||
* | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work | Léo Gourdin | 2021-03-01 | 1 | -4/+4 |
|\ \ | |||||
| * | | bug fix ? | Sylvain Boulmé | 2021-03-01 | 1 | -4/+4 |
| | | | |||||
* | | | Proof of fsval condition cmp ok | Léo Gourdin | 2021-03-01 | 1 | -968/+18 |
| | | | |||||
* | | | [Admitted checker] Some more proof, version with buggy addirw0 | Léo Gourdin | 2021-02-25 | 1 | -18/+2 |
| | | | |||||
* | | | some more proof for fake hsval checker expansions | Léo Gourdin | 2021-02-25 | 1 | -324/+1 |
| | | | |||||
* | | | [Intermediate] Adding fake hsval for Ccomp expansion | Léo Gourdin | 2021-02-23 | 2 | -164/+68 |
| | | | |||||
* | | | Fix imports | Léo Gourdin | 2021-02-23 | 1 | -1/+1 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work | Léo Gourdin | 2021-02-23 | 6 | -79/+202 |
|\| | | |||||
| * | | Merge branch 'riscv-work-rules' of ↵ | Léo Gourdin | 2021-02-23 | 1 | -2/+52 |
| |\ \ | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules | ||||
| | * | | add target_cbranch_expanse | Sylvain Boulmé | 2021-02-23 | 1 | -2/+52 |
| | | | | |||||
| * | | | Separate target_op_simplify for riscV | Léo Gourdin | 2021-02-23 | 1 | -19/+2 |
| |/ / | |||||
| * | | fix comments | Sylvain Boulmé | 2021-02-23 | 1 | -2/+5 |
| | | | |||||
| * | | starting an interface for target rewriting rules. | Sylvain Boulmé | 2021-02-23 | 1 | -9/+130 |
| | | | |||||
| * | | improved pre_output_regs | Sylvain Boulmé | 2021-02-22 | 1 | -5/+8 |
| | | | |||||
| * | | a bit more cleaning | Sylvain Boulmé | 2021-02-22 | 5 | -44/+21 |
| | | | |||||
| * | | quick fixcomments | Léo Gourdin | 2021-02-16 | 1 | -4/+1 |
| | | | |||||
* | | | others case for ccompimm | Léo Gourdin | 2021-02-23 | 1 | -53/+51 |
| | | | |||||
* | | | Some more proofs on branch expansion, using make_immed32_sound | Léo Gourdin | 2021-02-23 | 1 | -59/+221 |
| | | |