aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0279-731/+10580
|\
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-016-11/+161
| |\
| * | Ignore loopback edges on tail-duplicateCyril SIX2020-12-011-0/+2
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-2413-31/+343
| |\ \
| * | | prepass scheduling proof finished !Sylvain Boulmé2020-11-201-24/+56
| * | | merge nouveau tunnelingDavid Monniaux2020-11-191-1/+1
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-198-270/+728
| |\ \ \
| * | | | seval_builtin_sval_preservedDavid Monniaux2020-11-171-1/+4
| * | | | a little lemma on list of builtinsDavid Monniaux2020-11-171-2/+15
| * | | | there remains two tricky casesDavid Monniaux2020-11-161-3/+14
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-062-27/+32
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-055-31/+114
| |\ \ \ \ \
| * | | | | | disable debug printing in schedulerDavid Monniaux2020-11-042-7/+9
| * | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-041-1/+2
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-037-36/+121
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-315-17/+121
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-304-168/+78
| |\ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-295-48/+109
| |\ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-284-42/+27
| |\ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-63/+166
| |\ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-10/+277
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | improved CSE3David Monniaux2020-10-271-12/+12
| * | | | | | | | | | | | | | progress in proofs on new CSE3David Monniaux2020-10-271-3/+34
| * | | | | | | | | | | | | | deactivate LICM by defaultDavid Monniaux2020-10-272-21/+12
| * | | | | | | | | | | | | | begin fixing CSE3 to keep more inductive stuffDavid Monniaux2020-10-272-10/+19
| * | | | | | | | | | | | | | invariant printing more aligned with RTL dumpsDavid Monniaux2020-10-271-2/+2
| * | | | | | | | | | | | | | print invariantsDavid Monniaux2020-10-271-11/+46
| * | | | | | | | | | | | | | attempt at store -> load.sDavid Monniaux2020-10-261-2/+3
| * | | | | | | | | | | | | | new OpWeightsDavid Monniaux2020-10-222-0/+25
| * | | | | | | | | | | | | | new OpWeights for aarch64David Monniaux2020-10-221-318/+342
| * | | | | | | | | | | | | | -mtune=David Monniaux2020-10-222-1/+5
| * | | | | | | | | | | | | | allow changing target cpuDavid Monniaux2020-10-222-21/+40
| * | | | | | | | | | | | | | allow changing the target coreDavid Monniaux2020-10-222-120/+160
| * | | | | | | | | | | | | | prefix all calls to OpWeights as preparation to using a structureDavid Monniaux2020-10-221-14/+14
| * | | | | | | | | | | | | | attempt at modeling RocketDavid Monniaux2020-10-221-0/+83
| * | | | | | | | | | | | | | turn on cache emulationDavid Monniaux2020-10-191-9/+9
| * | | | | | | | | | | | | | op_valid_pointer_eq x86David Monniaux2020-10-191-0/+14
| * | | | | | | | | | | | | | op_valid_pointer_eq ppcDavid Monniaux2020-10-191-0/+14
| * | | | | | | | | | | | | | op_valid_pointer_eq armDavid Monniaux2020-10-191-0/+15
| * | | | | | | | | | | | | | op_valid_pointer_eq for aarch64David Monniaux2020-10-191-0/+14
| * | | | | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-1822-176/+939
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | simplify HSop (and merge hSop and hSop_Sinit)Sylvain Boulmé2020-10-172-42/+23
| * | | | | | | | | | | | | | | update op_valid_pointer_eq proof on the KVXSylvain Boulmé2020-10-171-22/+4
| * | | | | | | | | | | | | | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass sched...Sylvain Boulmé2020-10-172-0/+32
| * | | | | | | | | | | | | | | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-174-762/+2
| * | | | | | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-1692-11356/+3357
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | | | pour ARMDavid Monniaux2020-10-021-4/+4
| | * | | | | | | | | | | | | | | fix need for kvx-elfDavid Monniaux2020-10-021-5/+1
| | * | | | | | | | | | | | | | | so that all architectures compileDavid Monniaux2020-10-027-8/+24
| | * | | | | | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-027-19/+38
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit (git 2.34.1) at 2024-07-11 19:12:39 +0000