aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-313-17/+118
| |\ \ \ \ \ \
| * \ \ \ \ \ \ 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-294-48/+107
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-283-40/+24
| |\ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-274-19/+110
| |\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | improved CSE3David Monniaux2020-10-271-12/+12
| | | | | | | | | | | |
| * | | | | | | | | | | progress in proofs on new CSE3David Monniaux2020-10-271-3/+34
| | | | | | | | | | | |
| * | | | | | | | | | | deactivate LICM by defaultDavid Monniaux2020-10-271-20/+11
| | | | | | | | | | | |
| * | | | | | | | | | | 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
| | | | | | | | | | | |
| * | | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-188-143/+845
| |\ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-021-2/+9
| |\ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-211-1/+482
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | risc-V now without trapping instructionsDavid Monniaux2020-09-211-0/+24
| | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | moved Risc-V div ValueAOp to central locationDavid Monniaux2020-09-211-0/+215
| | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | moved some "total" value domain functions to a central locationDavid Monniaux2020-09-211-1/+243
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-2852-391/+6967
| |\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework
| * | | | | | | | | | | | | | [BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSECyril SIX2020-04-1067-473/+5837
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | Compatibility Coq 8.11.0Cyril SIX2020-04-103-10/+10
| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-1812-63/+109
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | / | | |_|_|_|_|_|_|_|_|_|_|_|_|/ | |/| | | | | | | | | | | | |
| * | | | | | | | | | | | | | Add support for __builtin_fabsfXavier Leroy2020-07-272-0/+6
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Introduce additional "branch" build information.Bernhard Schommer2020-07-081-2/+2
| | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | Move shared code in new file.Bernhard Schommer2020-06-286-5/+44
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
| * | | | | | | | | | | | | | Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A typical example is `(void) __builtin_sel(a, b, c)`. It is safe to generate zero code for these uses of builtins because builtins whose semantics are known to the compiler are pure. Other builtins with side effects (e.g. `__builtin_trap`) are not known and will remain in the compiled code. It is useful to generate zero code for these uses of builtins because some of them (e.g. `__builtin_sel`) must be transformed into proper CminorSel expressions during instruction selection. Otherwise, they propagate all the way to ExpandAsm, causing a "not implemented" error there.
| * | | | | | | | | | | | | | Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-212-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
| * | | | | | | | | | | | | | Move reserved_registers to CPragmas.Bernhard Schommer2020-04-202-7/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
* | | | | | | | | | | | | | | Fixing issue with loops having branches leading to goto backedgeCyril SIX2020-11-052-27/+32
| |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Fixing get_loop_headers + alternative get_inner_loops (commented, not active)Cyril SIX2020-11-042-27/+107
| | | | | | | | | | | | | |
* | | | | | | | | | | | | | do not print "refining" unless askedDavid Monniaux2020-11-041-1/+2
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | |
* | | | | | | | | | | | | do not print "updates" to nodesDavid Monniaux2020-11-041-1/+2
| |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |
* | | | | | | | | | | | refixcse3David Monniaux2020-11-032-34/+53
| | | | | | | | | | | |
* | | | | | | | | | | | Loop Rotate with -flooprotateCyril SIX2020-11-032-1/+61
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | |
* | | | | | | | | | | refining CSE3 nodesDavid Monniaux2020-10-311-14/+81
| | | | | | | | | | |
* | | | | | | | | | | seems to work betterDavid Monniaux2020-10-312-3/+37
| | | | | | | | | | |
* | | | | | | | | | | also match IstoreDavid Monniaux2020-10-301-1/+2
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
* | | | | | | | | | reinstated old versionDavid Monniaux2020-10-304-216/+39
| | | | | | | | | |
* | | | | | | | | | reinstated previous forward_move functionDavid Monniaux2020-10-292-11/+98
| |_|_|_|_|_|_|_|/ |/| | | | | | | |
* | | | | | | | | CSE3 trivial_ops flagDavid Monniaux2020-10-292-3/+3
| | | | | | | | |
* | | | | | | | | in CSE3 choose lowest variable as representative for movesDavid Monniaux2020-10-293-45/+104
| |_|_|_|_|_|_|/ |/| | | | | | |
* | | | | | | | DuplicateParam -> DuplicateOracle + simpler DuplicatepassesSylvain Boulmé2020-10-283-40/+24
| |_|_|_|_|_|/ |/| | | | | |
* | | | | | | Correcting typoCyril SIX2020-10-271-3/+3
| | | | | | |
* | | | | | | Merge branch 'kvx-work' into duplicate-paramCyril SIX2020-10-273-41/+107
|\ \ \ \ \ \ \
| * | | | | | | new CSE3David Monniaux2020-10-273-41/+107
| | |_|_|_|_|/ | |/| | | | |
* | | | | | | Oops forgot Duplicatepasses.vCyril SIX2020-10-271-0/+64
| | | | | | |
* | | | | | | Splitting Duplicate in several passesCyril SIX2020-10-271-14/+20
| | | | | | |
* | | | | | | Reworked Duplicate to be parametrizedCyril SIX2020-10-272-5/+26
|/ / / / / /
* | | | | | Loop body unrolling with -funrollbody nCyril SIX2020-10-161-3/+6
| | | | | |
* | | | | | Loop body unrollingCyril SIX2020-10-161-1/+39
| | | | | |
generated by cgit (git 2.34.1) at 2024-07-04 11:40:04 +0000