<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>