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