Hey,
I have an in-development multi-target superoptimization project(z3-based). For an experiment, I added a Go SSA converter to the project and discovered several missing optimizations through brute-force search. In my humble opinion, the most important one was the subtraction cancellation rule.
I’ve also implemented automatic harvesting and rule discovery but failed to find anything on standard library itself. However, my main limitation right now is a lack of sufficient knowledge of high-quality samples to analyze. If you could guide me on selecting good samples (e.g, popular packages and programs or tools, or specific workloads), I believe I could uncover more optimizations.
Here’s the full list of discovered rules. Some of them are patterns commonly used in cryptography, although I couldn’t find them triggering anywhere in the standard library. If you’re interested in any of them, I’d be happy to send another PR to include them.
| # |
rule |
| 1 |
x-(x-y)==y |
| 2 |
x|(~x&y)==x|y |
| 3 |
x&(~x|y)==x&y |
| 4 |
(x&y)|(x&~y)==x |
| 5 |
(x|y)&(x|~y)==x |
| 6 |
(x|y)-(x&y)==x^y |
| 7 |
(x^y)^(x|y)==x&y |
| 8 |
(x^y)^(x&y)==x|y |
| 9 |
(x&y)+(x|y)==x+y |
Hey,
I have an in-development multi-target superoptimization project(z3-based). For an experiment, I added a Go SSA converter to the project and discovered several missing optimizations through brute-force search. In my humble opinion, the most important one was the subtraction cancellation rule.
I’ve also implemented automatic harvesting and rule discovery but failed to find anything on standard library itself. However, my main limitation right now is a lack of sufficient knowledge of high-quality samples to analyze. If you could guide me on selecting good samples (e.g, popular packages and programs or tools, or specific workloads), I believe I could uncover more optimizations.
Here’s the full list of discovered rules. Some of them are patterns commonly used in cryptography, although I couldn’t find them triggering anywhere in the standard library. If you’re interested in any of them, I’d be happy to send another PR to include them.
x-(x-y)==yx|(~x&y)==x|yx&(~x|y)==x&y(x&y)|(x&~y)==x(x|y)&(x|~y)==x(x|y)-(x&y)==x^y(x^y)^(x|y)==x&y(x^y)^(x&y)==x|y(x&y)+(x|y)==x+y