<div dir="ltr">Hi,<div>What all methods are possible for program analysis? There are :-</div><div>1) Flow sensitive analysis</div><div>2) Path Sensitive analysis ( Symbolic execution )</div><div>3) Context sensitive analysis</div><div><br></div><div>Any other current research in this field ? Please guide</div><div><br></div><div>Thanks,</div><div>Siddharth</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Aug 25, 2018 at 4:42 AM, Artem Dergachev <span dir="ltr"><<a href="mailto:noqnoqneo@gmail.com" target="_blank">noqnoqneo@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div text="#000000" bgcolor="#FFFFFF"><span class="">
    <br>
    <br>
    <div class="m_-5259996898880083500moz-cite-prefix">On 8/24/18 5:31 AM, Siddharth Shankar
      Swain wrote:<br>
    </div>
    <blockquote type="cite">
      
      <div dir="ltr">Thanks for the detailed explanation. So is changing
        the analysis technique from path sensitive (symbolic execution)
        analysis to some other technique bring in the soundness property
        ? <br>
      </div>
    </blockquote>
    <br></span>
    Yup, depending on the technique.<br>
    <br>
    And that wouldn't be Analyzer-specific anymore.<span class=""><br>
    <br>
    <blockquote type="cite">
      <div dir="ltr">
        <div>Thanks,</div>
        <div>Siddharth</div>
      </div>
      <div class="gmail_extra"><br>
        <div class="gmail_quote">On Sat, Aug 18, 2018 at 1:27 AM, Artem
          Dergachev <span dir="ltr"><<a href="mailto:noqnoqneo@gmail.com" target="_blank">noqnoqneo@gmail.com</a>></span>
          wrote:<br>
          <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
            <div text="#000000" bgcolor="#FFFFFF"> Nope, at least not
              with the "path-sensitive" (symbolic execution) engine.
              Which is the whole point of using the Analyzer, as
              compared to writing an arbitrary tool by exploring the AST
              yourself. Depends on what you want to check, of course,
              something really trivial should be possible.<br>
              <br>
              While we do care about false positives a lot, there are
              some decisions within the Analyzer's core that prevent
              perfect soundness from happening but are still considered
              to be good because they greatly boost our ability to find
              any bugs at all and at the same time simplify development
              dramatically.<br>
              <br>
              One of the most common unsound assumptions that the
              Analyzer makes is that in a program that looks like this:
              "if (x) { ... } if (y) { ... }", where 'x' and 'y' are
              completely unrelated to each other, the Analyzer would
              explore all four paths (i.e., (x is true or false) times
              (y is true or false)) as if it's sure that they are
              feasible. This is not only unsound on its own, but it
              amplifies other inaccuracies in modeling (eg., if function
              body is unavailable for analysis, destroying information
              when such function is called would lead not only to false
              negatives but to false positives as well). But these false
              positives are relatively easy to suppress (eg., by adding
              some sort of assert(x || !y), which is in most cases
              anyway a good thing to document), and the primary benefit
              of this simplification is that checkers no longer need to
              implement a "merge" function for the information that they
              track in the program state: they only need to update their
              state by modeling effect of every non-control-flow event
              in the program. With ~100 checkers already written,
              limiting them to only simple operations on the program
              state helps dramatically.<br>
              <br>
              Additionally, the Analyzer's understanding of the language
              is not perfect. We're constantly working on this, but
              languages like C++ are *huge*. We have a separation of
              responsibilities between core and checkers that allow us
              to write most transfer functions once within the core and
              have checkers simply consume the results of the modeling
              (checkers may still want to model their own metadata), but
              covering all AST nodes and their interactions is still,
              well, harder than writing a CodeGen. Any bugs in core
              transfer functions will prevent you from doing a sound
              analysis, and making sure all such bugs are fixed is
              probably much more work than whatever you plan to
              accomplish here.<br>
              <br>
              On the non-technical side, it is always up to a developer
              of the program to decide what is a genuine bug. For
              example, there are a lot of projects on which a memory
              leak is not considered to be a bug. Or if an application
              is not security-critical, a null pointer dereference we
              find may be on such an unlikely path that the developer
              will only be annoyed to know about it and never really
              appreciate the report. And the Analyzer doesn't even
              guarantee that it'd find anything that's more severe than
              a dead code: after all, the only reason symbolic execution
              works is "state splits are justified because otherwise
              it's dead code".<br>
              <br>
              Last but not least, there's also the "Clang CFG" thing,
              which the Analyzer uses (and some compiler warnings also
              use), but it's not used for compilation (LLVM CFG is used
              instead) and it's not entirely accurate (especially for
              C++, though it's getting better). Clang CFG is usable for
              creating usable data flow analyses which you can make as
              sound as the CFG is accurate. There's a collection of such
              analyses in lib/Analysis. The Analyzer uses some of them
              internally and we're very happy with them most of the
              time. At the same time, there's no fancy framework for
              creating custom data flow analyses, like there is for the
              Analyzer's checkers; you'll have to write all transfer
              functions yourself. So if all you want is a ready-made CFG
              for C, you should have a look at that.
              <div>
                <div class="m_-5259996898880083500h5"><br>
                  <br>
                  <div class="m_-5259996898880083500m_7530136288058460445moz-cite-prefix">On
                    8/17/18 4:35 AM, Siddharth Shankar Swain via cfe-dev
                    wrote:<br>
                  </div>
                </div>
              </div>
              <blockquote type="cite">
                <div>
                  <div class="m_-5259996898880083500h5">
                    <div dir="ltr">Hi all,
                      <div><br>
                      </div>
                      <div>Is it possible to develop a checker  or some
                        feature in clang SA which will only have perfect
                        soundness property ( if we don't care about
                        completness property )  i.e if the analyzer says
                        X is a genuine bug then X is really a genuine
                        bug. Whatever  bug  it reports are all genuine
                        but it doesn't report all genuine bugs. Please
                        guide.</div>
                      <div><br>
                      </div>
                      <div>Thanks,</div>
                      <div>Siddharth</div>
                    </div>
                    <br>
                    <fieldset class="m_-5259996898880083500m_7530136288058460445mimeAttachmentHeader"></fieldset>
                  </div>
                </div>
                <pre class="m_-5259996898880083500m_7530136288058460445moz-quote-pre">______________________________<wbr>_________________
cfe-dev mailing list
<a class="m_-5259996898880083500m_7530136288058460445moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a class="m_-5259996898880083500m_7530136288058460445moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a>
</pre>
              </blockquote>
              <br>
            </div>
          </blockquote>
        </div>
        <br>
      </div>
    </blockquote>
    <br>
  </span></div>

</blockquote></div><br></div>