<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Ahaaaaa, ooooookkkkk, iiiiiiii seeeeeeeeee!<br>
    <br>
    Sounds fascinating, must-have and hard.<br>
    <br>
    My primary question is how much do you think this will put stress on
    the checkers. Like, how much more difficult would it be to write
    checkers when we require them to include the slicing criterion with
    their bug reports? How much of it would we (i.e., BugReporter) be
    able to infer ourselves?<br>
    <br>
    ------------------------<br>
    <br>
    Say, let's take Example 1. You describe the slicing criterion as:<br>
    <br>
        (13, <dynamically allocated int object>)<br>
    <br>
    The value of the dynamically allocated into object remains the same
    regardless of whether the object is stored in global_ptr or not, so
    the slice doesn't need to include line 5 or 6. Therefore i think
    that the slicing criterion you proposed is not what we're looking
    for, and the real slicing criterion we're looking for is:<br>
    <br>
        (13, <liveness of <dynamically allocated int
    object>>)<br>
    <br>
    Like, we're mapping every dynamically allocated object to an
    imaginary heap location that represents its current liveness, and
    include that imaginary variable, rather than the object itself, in
    the slicing criterion. Line 6 would affect liveness of the object on
    line 13 (if it's stored into a global, it's alive; otherwise it's
    not), therefore it'll be part of the slice. So, am i understanding
    correctly that you're proposing a checker API that'll look like
    this:<br>
    <br>
      BugReport *R = new BugReport(Node, ...);<br>
      R->addLivenessBasedSlicingCriterion(HeapSym);<br>
    <br>
    ?<br>
    <br>
    I guess we can infer the statement of the slicing criterion from the
    Node, but i'm not entirely sure; see also below.<br>
    <br>
    I'd actually love it if you elaborate this example further because
    it's fairly interesting. Like, we know that the assignment affects
    the liveness information, but how would the slicing algorithm figure
    this out? Do you have a step-by-step description of how the
    algorithm behaves in this case?<br>
    <br>
    ------------------------<br>
    <br>
    Let's take another example i just came up with. Consider
    alpha.unix.PthreadLock - a checker that finds various bugs with
    mutexes, such as double locks or double unlocks. Consider code:<br>
    <br>
    1  pthread_mutex_t mtx1, mtx2;<br>
    2<br>
    3  void foo(bool x1, bool x2) {<br>
    4    if (x1)<br>
    5      pthread_mutex_lock(&mtx1);<br>
    6    if (x2)<br>
    7      pthread_mutex_lock(&mtx1);<br>
    8    // ...<br>
    9  }<br>
    <br>
    In this example we'll report a double lock bug due to a copy-paste
    error: line 7 should probably lock &mtx2 rather than &mtx1.<br>
    <br>
    The whole program is relevant to the report. Without line 5, there
    would only be a single lock. It transitions the mutex object from
    state "unknown" to state "locked".<br>
    <br>
    I don't think the Analyzer would currently do a bad job at
    explaining the bug; it's pretty straightforward.<br>
    <br>
    What would be the slicing criterion in this case? As far as i
    understand, it'll be<br>
    <br>
        (7, <locked-ness of mtx1>)<br>
    <br>
    In this case "lockedness" is, again, an "imaginary heap location"
    that contains metadata for the mutex. More specifically, it is a GDM
    map value. How would a checker API look in this case? How would it
    even describe to the BugReporter what to look at, given that
    currently only the checker understands how to read its GDM values?<br>
    <br>
    My random guess is:<br>
    <br>
      BugReport *R = new BugReport(Node, ...);<br>
      R->addGDMBasedSlicingCriterion<MutexState>(MutexMR);<br>
    <br>
    ------------------------<br>
    <br>
    So it sounds to me that your project is, like many other awesome
    projects, brings in, as a dependency, replacing GDM with a better,
    smarter data map that the analyzer core *can* introspect and
    manipulate without the direct help from the checkers. It might be
    that your project actually requires relatively little amounts of
    such introspection - i.e., you might be able to get away with "it's
    some GDM map and the value for this key has changed, therefore this
    statement is a relevant data dependency" for quite a lot of
    checkers.<br>
    <br>
    That's the subject i was also bringing up as part of
    <a class="moz-txt-link-freetext" href="https://reviews.llvm.org/D59861">https://reviews.llvm.org/D59861</a> - "this was the plan that is part of
    the even-more-long-term plan of completely deprecating the
    void*-based Generic Data Map...". This was also something that
    became a blocker on my old attempt to introduce summary-based
    analysis. It required stuffing fairly large chunks of code into
    every checker that would teach the checker how to collect summary
    information and apply it when the summary is applied, and this new
    boilerplate was fairly brain-damaging to implement and hard to get
    right or even to explain. This problem also blocks other projects,
    such as state merging / loop widening (on one branch the mutex is
    locked, on the other branch it is unlocked, hey checker please teach
    me how to merge this).<br>
    <br>
    The variety of slicing criteria (that is a consequence of the
    variety of checkers that we have) sounds pretty scary to me. Some of
    them are really complicated, eg. the liveness criterion. Making sure
    that the generic algorithm works correctly with at least a
    significant chunk of them is going to be fun. Making sure it can
    actually handle arbitrary criterions required by the checkers
    without having every checker come with its own boilerplate for
    slicing also sounds hard. And it'll be very bad if we have to tell
    our checker developers "hey, by the way, you also need to know what
    backward slicing is and write down part of the algorithm in order to
    ever get your checker enabled by default" - i'm already feeling
    pretty bad explaining dead symbols and pointer escapes (which are
    pretty much must-have in most checkers), these are definitely
    examples of a boilerplate that a smarter version of GDM could handle
    automatically. In order to conquer the world, i think we should
    stick to our "writing a checker in 24 hours" utopia: writing a
    checker should be as easy as writing down the transfer functions for
    relevant statements. In my opinion, we should take it as an
    important constraint.<br>
    <br>
    <br>
    <br>
    <br>
    <div class="moz-cite-prefix">On 4/2/19 12:21 PM, Kristóf Umann
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAGcXOD4nQYpsQ3Rriq9V4fGp=xzRozhr0Mex3_Vyq+FMTihKGw@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div dir="ltr">Somehow the images and the attached files were
          left out, please find them here:</div>
        <br>
        <div class="gmail_quote">
          <div dir="ltr" class="gmail_attr">On Tue, 2 Apr 2019 at 21:16,
            Kristóf Umann <<a href="mailto:dkszelethus@gmail.com"
              target="_blank" moz-do-not-send="true">dkszelethus@gmail.com</a>>
            wrote:<br>
          </div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px
            0.8ex;border-left:1px solid
            rgb(204,204,204);padding-left:1ex">
            <div dir="ltr">
              <div class="gmail_quote">
                <div dir="ltr">
                  <div dir="ltr">
                    <div dir="ltr">
                      <div dir="ltr"><span
                          style="background-color:rgb(255,255,255)"><font
                            color="#000000">Hi!<br>
                            <br>
                          </font></span>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">In this letter, I'd like
                              to describe a particular problem in the
                              Clang StaticAnalyzer's <font
                                face="monospace, monospace">BugReporter
                              </font>class that I'd like to tackle in a
                              Google Summer of Code project this summer.
                              I'll show real-world examples on some of
                              its shortcomings, and propose a potential
                              solution using static backward program
                              slicing. At last, I'll ask some specific
                              questions. I'd love to hear any and all
                              feedback on this!</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">This is a <i>problem
                                statement, </i>not a <i>proposal</i>. I
                              plan to send out a formal proposal by
                              Friday (but not later then Saturday), that
                              will contain more details on both the
                              problem and the solution. I don't
                              introduce myself or my previous works
                              within the project, that will also be
                              detailed in my upcoming letter. I also
                              plan to incorporate the feedback I'll
                              receive to this letter.</font></span></div>
                      </div>
                      <div dir="ltr"><span
                          style="background-color:rgb(255,255,255)"><font
                            color="#000000"><br>
                          </font></span></div>
                      <div><b><font
                            style="background-color:rgb(255,255,255)"
                            size="4" color="#000000">---=== BugReporter
                            constructs bad reports ===---</font></b></div>
                      <div><b><font
                            style="background-color:rgb(255,255,255)"
                            size="4" color="#000000"><br>
                          </font></b></div>
                      <div><span
                          style="background-color:rgb(255,255,255)"><font
                            color="#000000"><b>What does the BugReporter
                              do?</b><br>
                            <br>
                            After the Static Analyzer found an error,
                            the <font face="monospace, monospace">BugReporter
                            </font>receives an <font face="monospace,
                              monospace">ExplodedNode</font>, which,
                            accompanied by its predecessors, contains
                            all the information needed to reproduce that
                            error. This <i>bugpath </i>is then shortened
                            with a variety of heuristics, such as
                            removing unrelated function calls, unrelated
                            branches and so on. <font face="monospace,
                              monospace">BugReporter </font>by the end
                            of this process will construct a <font
                              face="monospace, monospace">PathDiagnostic
                            </font>object for each report, that is,
                            ideally, minimal.</font></span></div>
                      <div><b style="background-color:rgb(255,255,255)"><font
                            color="#000000"><br>
                          </font></b></div>
                      <div><b style="background-color:rgb(255,255,255)"><font
                            color="#000000">Example 1.</font></b></div>
                      <div><span
                          style="background-color:rgb(255,255,255)"><font
                            color="#000000"><br>
                          </font></span></div>
                      <div><span
                          style="background-color:rgb(255,255,255)"><font
                            color="#000000">Consider the following code
                            example:<br>
                            <br>
                          </font></span>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">1 
                            // leak.cpp</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">2 
                            int *global_ptr;</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">3  </font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">4 
                            void save_ext(int storeIt, int *ptr) {</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">5 
                              if (storeIt)</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">6 
                                global_ptr = ptr;</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">7 
                            }</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">8</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">9 
                            void test(int b) {</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">10 
                             int *myptr = new int;</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">11 
                             save_ext(b, myptr);</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">12 
                             delete global_ptr;</font></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="monospace, monospace" color="#000000">13
                            }</font></div>
                      </div>
                      <div><span
                          style="background-color:rgb(255,255,255)"><font
                            color="#000000"><br>
                          </font></span></div>
                      <div dir="ltr">
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">It's clear that if test is
                              invoked with <font face="monospace,
                                monospace">b</font>'s value set to true,
                              there is no error in the program. However,
                              should b be false, we'll leak memory.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <span
style="font-family:monospace,monospace;background-color:rgb(255,255,255)"><font
                            color="#000000">$ clang -cc1 -analyze
                            -analyzer-checker=core,cplusplus leak.cpp</font></span></div>
                      <div dir="ltr">
                        <div><img
                            src="cid:part2.0FD1D4A7.51584B82@gmail.com"
                            alt="image.png" class="" width="472"
                            height="168"><br>
                        </div>
                      </div>
                      <div dir="ltr"><font
                          style="background-color:rgb(255,255,255)"
                          face="monospace, monospace" color="#000000"><br>
                        </font>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">The Static Analyzer is
                              able to catch this error, but fails to
                              mention the call to <font face="monospace,
                                monospace">save_ext</font> entirely,
                              despite the error only occurring because
                              the analyzer assumed that <font
                                face="monospace, monospace">storeIt</font> is
                              false. I've also attached the exploded
                              graph <font face="monospace, monospace">leak.svg </font><font
                                face="arial, helvetica, sans-serif">that
                                demonstrates this.</font></font></span></div>
                        <div><font
                            style="background-color:rgb(255,255,255)"
                            face="arial, helvetica, sans-serif"
                            color="#000000"><br>
                          </font></div>
                        <div>
                          <div><b
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000">Example 2.</font></b></div>
                        </div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Consider the following
                              code example:<br>
                              <br>
                              <font face="monospace, monospace">1  //
                                divbyzero.cpp</font><br>
                            </font></span>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">2  void f() {</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">3    int i = 0;</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">4    (void) (10 / i);</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">5  }</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">6</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">7  void g() { f(); }</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">8  void h() { g(); }</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">9  void j() { h(); }</font></div>
                          <div><font
                              style="background-color:rgb(255,255,255)"
                              face="monospace, monospace"
                              color="#000000">10 void k() { j(); }</font></div>
                          <div><span
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000"><br
class="m_6421736142923902491gmail-m_-3454961580602141710gmail-m_-6979117027997739172gmail-m_4426039388547674777gmail-m_5439174890474816058gmail-m_6038659214782379119gmail-Apple-interchange-newline">
                                Its clear that a call to f will result
                                in a division by zero error.</font></span></div>
                          <div><span
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000"><br>
                              </font></span></div>
                          <span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><span
                                style="font-family:monospace,monospace">$
                                clang -cc1 -analyze
                                -analyzer-checker=core </span><span
                                style="font-family:monospace,monospace">divbyzero.cpp</span></font></span></div>
                        <div><img
                            src="cid:part3.920EB618.C1D65837@gmail.com"
                            alt="image.png" class="" width="334"
                            height="472"><br>
                        </div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Again, the Static Analyzer
                              is plenty smart enough to catch this, but
                              the constructed bug report is littered
                              with a lot of useless information -- it
                              would be enough to only show the body of
                              f, and, optionally where f itself was
                              called. For the sake of completeness, I've
                              attached <font face="monospace, monospace">divbyzero.svg</font> that
                              contains the exploded graph for the above
                              code snippet.<br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">The above examples
                              demonstrate that <font face="monospace,
                                monospace">BugReporter </font>sometimes
                              reduces the bugpath too much or too
                              little.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><b><font
                              style="background-color:rgb(255,255,255)"
                              size="4" color="#000000">---=== Solving
                              the above problem with static backward
                              program slicing ===---</font></b></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><b
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">What is static backward
                              program slicing?</font></b></div>
                        <div>
                          <div><span
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000"><br>
                              </font></span></div>
                          <div><span
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000">A <i>program slice</i> consists
                                of the parts of a program that
                                (potentially) affect the values computed
                                at some point of interest, called the
                                slicing criterion. <i><b>Program slicing</b></i> is
                                a decomposition technique that elides
                                program components not relevant to the
                                slicing criterion (which is a pair of
                                (statement, set of variables)), creating
                                a program slice[1][2]. <b>Static </b>slicing
                                preserves the meaning of the variable(s)
                                in the slicing criterion for all
                                possible inputs[1]. <b>Backward </b>slices
                                answer the question “what program
                                components might affect a selected
                                computation?”[1]</font></span></div>
                        </div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">While statement-minimal
                              slices are not necessarily unique[3],
                              Weisel developed a popular algorithm that
                              constructs one. In essence, his fix-point
                              algorithm constructs sets of <i>relevant
                                variables</i><i> </i>for each edge in
                              between node <i>i</i> and node <i>j</i> in
                              a CFG graph, from which he constructs <i>relevant
                                statements</i>. The fix-point of the
                              relevant statements set is the slice
                              itself.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">One of the characteristic
                              of his algorithm is that the resulting
                              program slice will be executable. However,
                              our problem doesn't require the code to be
                              executable, so we could use a more
                              "aggressive" approach that creates a
                              smaller slice. An improvement to his
                              algorithm is presented in [4].</font></span></div>
                        <div>
                          <div><b
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000"><br>
                              </font></b></div>
                          <div><b
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000">How does this relate to
                                BugReporter?</font></b></div>
                        </div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">We can show that using
                              Weiser's algorithm, issues raised in
                              Example 1. and Example 2. can be improved
                              upon.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">For example 1., the
                              statement-minimal program slice with the
                              criterion (13, <font face="monospace,
                                monospace"><dynamically allocated int
                                object></font>) will contain the
                              statements 5 and 6, and for example 2.,
                              the statement-minimal program slice with
                              the criterion (4,<font face="monospace,
                                monospace"> i</font>) won't contain
                              anything but statements 3 and 4. For the
                              latter, we can even improve the algorithm
                              to also contain statement 7, where a call
                              to f is made.</font></span></div>
                        <span style="background-color:rgb(255,255,255)"><font
                            color="#000000"><br
class="m_6421736142923902491gmail-m_-3454961580602141710gmail-m_-6979117027997739172gmail-m_4426039388547674777gmail-Apple-interchange-newline">
                            The analyzer, as stated earlier, gives <font
                              face="monospace, monospace">BugReporter </font>an
                            <font face="monospace, monospace">ExplodedNode</font>,
                            from which the slicing criterion must be
                            constructed. The statement corresponding to
                            this node, coupled with the interesting
                            regions the checker itself marked could be
                            used to construct this slicing criterion.</font></span>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><b>Challenges</b><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">While the algorithm Weiser
                              developed along with the improvements made
                              by others are interprocedural, I would
                              imagine that in implementation, it would
                              be a challenging step from an
                              intraprocedural prototype.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Several articles also
                              describe pointers, references, and
                              dynamically allocated regions, as well as
                              gotos and other tricky parts of the
                              language, but I still expect to see some
                              skeletons falling out of the closet when
                              implementing this for C++, not only C.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><b
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Drawbacks</font></b></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Static slicing, as an
                              algorithm that doesn't know anything about
                              input values, suffers from the same issues
                              that all static techniques do, meaning
                              that without heuristics, it'll have to do
                              very rough guesses, possibly leaving a far
                              too big program slice. However, with the
                              symbolic values the analyzer holds, this
                              could be improved, turning this into <i>conditioned
                                slicing, </i>as described in [1]. This
                              however is only planned as a followup work
                              after GSoC.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">For this reason, this
                              project would be developed as an
                              alternative approach to some of the
                              techniques used in <font face="monospace,
                                monospace">BugReporter</font>, as an
                              optional off-by-default analyzer feature.</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><font size="4" color="#000000"><b
                              style="background-color:rgb(255,255,255)">---===
                              Questions ===---</b></font></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">What do you think of this
                              approach?</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Do you think that
                              implementing this algorithm is achievable,
                              but tough enough task for GSoC?</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Would you prefer to see a
                              general program slicing library, or an
                              analyzer-specific implementation?
                              Traversing the <font face="monospace,
                                monospace">ExplodedGraph </font>would
                              be far easier in terms of what I want to
                              achieve, but a more general approach that
                              traverses the CFG (like <font
                                face="monospace, monospace">llvm::DominatorTree</font><font
                                face="arial, helvetica, sans-serif">[5])
                                could be beneficial to more developers,
                                but possibly at the cost of not being
                                able to improve the prototype with the
                                symbolic value information the analyzer
                                holds.</font></font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><b><i
                              style="background-color:rgb(255,255,255)"><font
                                color="#000000">References, links</font></i></b></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">[1] <span
                                style="font-size:13px;font-family:Arial,sans-serif">Gallagher,
                                Keith, and David Binkley. "Program
                                slicing." </span><i
                                style="font-size:13px;font-family:Arial,sans-serif">2008
                                Frontiers of Software Maintenance</i><span
style="font-size:13px;font-family:Arial,sans-serif">.</span></font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><span
                                style="font-size:13px;font-family:Arial,sans-serif">[2] </span><span
style="font-size:13px;font-family:Arial,sans-serif">Tip, Frank. </span><i
style="font-size:13px;font-family:Arial,sans-serif">A survey of program
                                slicing techniques</i><span
                                style="font-size:13px;font-family:Arial,sans-serif">.
                                Centrum voor Wiskunde en Informatica,
                                1994.</span></font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><span
                                style="font-size:13px;font-family:Arial,sans-serif">[3] </span><span
style="font-size:13px;font-family:Arial,sans-serif">Weiser, Mark.
                                "Program slicing." </span><i
                                style="font-size:13px;font-family:Arial,sans-serif">Proceedings
                                of the 5th international conference on
                                Software engineering</i><span
                                style="font-size:13px;font-family:Arial,sans-serif">.
                                IEEE Press, 1981.</span></font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><span
                                style="font-size:13px;font-family:Arial,sans-serif">[4] </span><span
style="font-size:13px;font-family:Arial,sans-serif">Binkley, David.
                                "Precise executable interprocedural
                                slices." </span><i
                                style="font-size:13px;font-family:Arial,sans-serif">ACM
                                Letters on Programming Languages and
                                Systems (LOPLAS)</i><span
                                style="font-size:13px;font-family:Arial,sans-serif"> 2.1-4
                                (1993): 31-45.</span></font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><span
                                style="font-size:13px;font-family:Arial,sans-serif">[5] </span><font
                                face="Arial, sans-serif"><a
                                  href="http://llvm.org/doxygen/classllvm_1_1DominatorTree.html"
                                  target="_blank" moz-do-not-send="true">http://llvm.org/doxygen/classllvm_1_1DominatorTree.html</a></font></font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Link to previous GSoC
                              related letter I sent: <a
                                href="http://lists.llvm.org/pipermail/cfe-dev/2019-February/061464.html"
                                target="_blank" moz-do-not-send="true">http://lists.llvm.org/pipermail/cfe-dev/2019-February/061464.html</a></font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000"><br>
                            </font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Cheers,</font></span></div>
                        <div><span
                            style="background-color:rgb(255,255,255)"><font
                              color="#000000">Kristóf Umann</font></span></div>
                      </div>
                    </div>
                  </div>
                </div>
              </div>
            </div>
          </blockquote>
        </div>
      </div>
    </blockquote>
    <br>
  </body>
</html>