<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>On 09/05/2017 05:57 PM, (IIIT) Siddharth Bhat via llvm-dev wrote:<br>
</p>
<blockquote
cite="mid:CAPipc=1V=x4DCBKSYSWBhA7Cz4dMOLvhteLQLou3-pT+zmYnaQ@mail.gmail.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<div dir="ltr">Hello all,
<div><br>
<div>I've seen some discussion that InstCombine is "too
general" and that llvm should implement a proper graph
rewrite mechanism:</div>
<div><br>
</div>
<div>Link to llvm-dev discussion about this: <a
moz-do-not-send="true"
href="http://lists.llvm.org/pipermail/llvm-dev/2017-May/113219.html">http://lists.llvm.org/pipermail/llvm-dev/2017-May/113219.html</a>,</div>
<div>Link to review where this came up (and I first heard
about it): <a moz-do-not-send="true"
href="https://reviews.llvm.org/D37195">https://reviews.llvm.org/D37195</a>.</div>
<div><br>
</div>
<div>I wanted to understand what the current issues with
InstCombine are, and if a graph rewriter prototype is
something people are interested in. I find the idea
appealing, from what little I know it, so I'd be interested
in hacking something up.</div>
<div><br>
</div>
<div>What would such a framework look like? Is there past
literature on the subject? From what I know, many functional
compilers using combinator based compilation were graph
rewriting. Is there other prior art?</div>
</div>
</div>
</blockquote>
<br>
I'm not sure that I'd describe it as "too general", but I suspect
that it could be made much more efficient. Currently, the patterns
are implemented in C++, which is often fairly verbose, and because
many of the checks are implemented separately, we end up touching
instructions many times as we attempt to match different patterns.
Worse, for many of these instructions we end up checking properties,
such as known bits, that are computed by further backward
instructions visiting. It is also hard to automatically check the
correctness of the transformations, and moreover, it is hard to
prove that we'll eventually reach a fixed point (we've certainly had
problems in the past where some inputs would cause an endless loop
between two different InstCombine patterns).<br>
<br>
I'd love to see a solution where most of the transformations were
specified in TableGen files and:<br>
1. We, as a result, had an easy way to convert these into a form
where some SMT-solver-based checker could certify correctness.<br>
2. We, as a result, has an easy way to somehow check soundness, as
a rewrite system, so we'd know it would reach a fixed point for all
inputs.<br>
3. We, as a result, reduced the number of lines of code we need to
maintain for these peephole optimizations.<br>
4. We, as a result, could generate efficient code for matching the
patterns using some automaton technique for minimizing unnecessary
visiting of instructions.<br>
<br>
I'm not sure how closely it matches what we would need, but
Stratego/XT comes to mind in terms of prior art (now here:
<a class="moz-txt-link-freetext" href="http://www.metaborg.org/en/latest/">http://www.metaborg.org/en/latest/</a>). There's been a lot of work over
the years on terminating graph rewriting systems in compilers.<br>
<br>
-Hal<br>
<br>
<blockquote
cite="mid:CAPipc=1V=x4DCBKSYSWBhA7Cz4dMOLvhteLQLou3-pT+zmYnaQ@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>
<div><br>
</div>
<div>Also, there is the idea of Equality Saturation (<a
moz-do-not-send="true"
href="http://www.cs.cornell.edu/%7Eross/publications/eqsat/">http://www.cs.cornell.edu/~ross/publications/eqsat/</a>)
that I found out about recently. Could this be used to
augment the InstCombine infrastructure?<br>
</div>
<div><br>
</div>
<div>Thanks,</div>
<div>~Siddharth</div>
<div><br>
</div>
</div>
</div>
<div dir="ltr">-- <br>
</div>
<div class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">Sending this from my phone, please excuse any
typos!</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
LLVM Developers mailing list
<a class="moz-txt-link-abbreviated" href="mailto:llvm-dev@lists.llvm.org">llvm-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev</a>
</pre>
</blockquote>
<br>
<pre class="moz-signature" cols="72">--
Hal Finkel
Lead, Compiler Technology and Programming Languages
Leadership Computing Facility
Argonne National Laboratory</pre>
</body>
</html>