Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | refining CSE3 nodes | David Monniaux | 2020-10-31 | 3 | -14/+84 | |
| | | ||||||
| * | seems to work better | David Monniaux | 2020-10-31 | 2 | -3/+37 | |
| | | ||||||
| * | also match Istore | David Monniaux | 2020-10-30 | 1 | -1/+2 | |
| | | ||||||
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-30 | 4 | -168/+78 | |
|\| | ||||||
| * | reinstated old version | David Monniaux | 2020-10-30 | 4 | -216/+39 | |
| | | ||||||
| * | reinstated previous forward_move function | David Monniaux | 2020-10-29 | 2 | -11/+98 | |
| | | ||||||
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-29 | 5 | -48/+109 | |
|\| | ||||||
| * | CSE3 trivial_ops flag | David Monniaux | 2020-10-29 | 2 | -3/+3 | |
| | | ||||||
| * | in CSE3 choose lowest variable as representative for moves | David Monniaux | 2020-10-29 | 4 | -45/+106 | |
| | | ||||||
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-28 | 4 | -42/+27 | |
|\| | ||||||
| * | deactivate LICM | David Monniaux | 2020-10-28 | 1 | -1/+1 | |
| | | ||||||
| * | DuplicateParam -> DuplicateOracle + simpler Duplicatepasses | Sylvain Boulmé | 2020-10-28 | 3 | -40/+24 | |
| | | ||||||
| * | restore URL on the coqdoc | Sylvain Boulmé | 2020-10-28 | 1 | -2/+3 | |
| | | ||||||
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 7 | -63/+166 | |
|\| | ||||||
| * | Correcting typo | Cyril SIX | 2020-10-27 | 1 | -3/+3 | |
| | | ||||||
| * | Merge branch 'kvx-work' into duplicate-param | Cyril SIX | 2020-10-27 | 8 | -41/+370 | |
| |\ | ||||||
| * | | Oops forgot Duplicatepasses.v | Cyril SIX | 2020-10-27 | 1 | -0/+64 | |
| | | | ||||||
| * | | Splitting Duplicate in several passes | Cyril SIX | 2020-10-27 | 2 | -54/+71 | |
| | | | ||||||
| * | | Adding Duplicatepasses.v to Makefile | Cyril SIX | 2020-10-27 | 1 | -1/+1 | |
| | | | ||||||
| * | | Reworked Duplicate to be parametrized | Cyril SIX | 2020-10-27 | 3 | -5/+27 | |
| | | | ||||||
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 7 | -10/+277 | |
|\ \ \ | | |/ | |/| | ||||||
| * | | new option for CSE3 (trivial ops) | David Monniaux | 2020-10-27 | 3 | -0/+7 | |
| | | | ||||||
| * | | new CSE3 | David Monniaux | 2020-10-27 | 3 | -41/+107 | |
| | | | ||||||
| * | | Merge branch 'kvx-work' of ↵ | David Monniaux | 2020-10-20 | 2 | -10/+14 | |
| |\| | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work | |||||
| | * | link on Cyril's short video | Sylvain Boulmé | 2020-10-19 | 2 | -10/+14 | |
| | | | ||||||
| * | | Merge branch 'kvx-work' of ↵ | David Monniaux | 2020-10-18 | 3 | -2/+52 | |
| |\| | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work | |||||
| * | | Merge remote-tracking branch 'origin/kvx-work-unroll-fixcse3' into kvx-work | David Monniaux | 2020-10-16 | 2 | -0/+256 | |
| |\ \ | ||||||
| | * | | forgot these | David Monniaux | 2020-10-16 | 2 | -0/+256 | |
| | | | | ||||||
* | | | | improved CSE3 | David Monniaux | 2020-10-27 | 1 | -12/+12 | |
| | | | | ||||||
* | | | | progress in proofs on new CSE3 | David Monniaux | 2020-10-27 | 1 | -3/+34 | |
| | | | | ||||||
* | | | | deactivate LICM by default | David Monniaux | 2020-10-27 | 2 | -21/+12 | |
| | | | | ||||||
* | | | | begin fixing CSE3 to keep more inductive stuff | David Monniaux | 2020-10-27 | 2 | -10/+19 | |
| | | | | ||||||
* | | | | invariant printing more aligned with RTL dumps | David Monniaux | 2020-10-27 | 1 | -2/+2 | |
| | | | | ||||||
* | | | | print invariants | David Monniaux | 2020-10-27 | 1 | -11/+46 | |
| | | | | ||||||
* | | | | attempt at store -> load.s | David Monniaux | 2020-10-26 | 1 | -2/+3 | |
| | | | | ||||||
* | | | | new OpWeights | David Monniaux | 2020-10-22 | 2 | -0/+25 | |
| | | | | ||||||
* | | | | new OpWeights for aarch64 | David Monniaux | 2020-10-22 | 1 | -318/+342 | |
| | | | | ||||||
* | | | | -mtune= | David Monniaux | 2020-10-22 | 2 | -1/+5 | |
| | | | | ||||||
* | | | | allow changing target cpu | David Monniaux | 2020-10-22 | 2 | -21/+40 | |
| | | | | ||||||
* | | | | allow changing the target core | David Monniaux | 2020-10-22 | 2 | -120/+160 | |
| | | | | ||||||
* | | | | prefix all calls to OpWeights as preparation to using a structure | David Monniaux | 2020-10-22 | 1 | -14/+14 | |
| | | | | ||||||
* | | | | attempt at modeling Rocket | David Monniaux | 2020-10-22 | 1 | -0/+83 | |
| | | | | ||||||
* | | | | turn on cache emulation | David Monniaux | 2020-10-19 | 1 | -9/+9 | |
| | | | | ||||||
* | | | | op_valid_pointer_eq x86 | David Monniaux | 2020-10-19 | 1 | -0/+14 | |
| | | | | ||||||
* | | | | op_valid_pointer_eq ppc | David Monniaux | 2020-10-19 | 1 | -0/+14 | |
| | | | | ||||||
* | | | | op_valid_pointer_eq arm | David Monniaux | 2020-10-19 | 1 | -0/+15 | |
| | | | | ||||||
* | | | | op_valid_pointer_eq for aarch64 | David Monniaux | 2020-10-19 | 1 | -0/+14 | |
| | | | | ||||||
* | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 22 | -176/+939 | |
|\ \ \ \ | | |_|/ | |/| | | ||||||
| * | | | Loop body unrolling with -funrollbody n | Cyril SIX | 2020-10-16 | 3 | -3/+9 | |
| | | | | ||||||
| * | | | Loop body unrolling | Cyril SIX | 2020-10-16 | 1 | -1/+39 | |
| | | | |