<div dir="ltr"><div><div>Hi Ted,<br><br>> <i>I think the problem should be looked at in a different fashion. You
should not need to reason about aliases at all. The analyzer engine
handles this for you. It’s all symbolic execution.<br><br></i></div>Yes, I realize the Static Analyzer will recognize that the line p = q means that 'p' and 'q' now has the same value, but it does not copy the user state (REGISTER_*_WITH_PROGRAMSTATE data) - which makes total sense, since it does not know how that data is structured. Therefore, I need to record the fact the aliasing has happened using checkBind. This is where I encountered the problem described in my original e-mail.<br>
<br></div><div>Reading through the <a href="http://clang-analyzer.llvm.org/checker_dev_manual.html">checker dev manual</a>, I found the relevant section:<br><i>"When <tt>x</tt> is evaluated,
we first construct an <tt>SVal</tt> that represents the lvalue of <tt>x</tt>, in
this case it is an <tt>SVal</tt> that references the <tt>MemRegion</tt> for <tt>x</tt>.
Afterwards, when we do the lvalue-to-rvalue conversion, we get a new <tt>SVal</tt>,
which references the value <b>currently bound</b> to <tt>x</tt>. That value is
symbolic; it's whatever <tt>x</tt> was bound to at the start of the function."<br><br></i></div><div>I need the reverse: not the value currently bound to x, but the SVal that references the MemRegion for x itself. I searched the documentation, but all I could find was ProgramState::getLValue, none of whose overloads give me what I need. So how could I achieve this?<br>
<br></div><div>Back to the aliasing problem: I think it would be very useful if the Static Analyzer exposes functions to retrieve aliasing information. For example, I would like to ask whether a given SVal is an alias of another. My original thought was that this alias-analysis could be implemented as a checker itself, which would dispatch an event when it detects an aliasing, but I do not see how it could expose methods to the other checkers (e.g. for them to be able to ask "is x an alias of y in this ProgramState?"). Does this make sense?<br>
<br>> <i>A null check might not always be redundant. On some paths the null
check may be redundant and others it won’t be. Thus there is a
dominance relationship here that needs to be checked. Essentially, all
paths need to show that the pointer is always non-null before the
pointer is checked. Otherwise you’ll get false positives. Doing this
correctly is hard, because not all paths are guaranteed to be traced.
You’ll need to handle that too.<br><br></i></div><div>Yes, this is a problem, but I have absolutely no clue as to how it could be solved. I would naturally want to keep the number of false-positive at minimum, even at the cost of some bugs going undetected.<br>
<br>> <i>In this scheme, the pointer value is the symbolic region. You’ll
essentially want to monitor the actual null checks of a symbolic region,
and see if that region is constrained to always be non-null.<br><br></i></div><div>My only vague idea is to use the checkEndAnalysis callback to explore
the ExplodedGraph, but I don't even know how to get started on it, i.e.
what I should look for. Any pointers (haha) you could give me would be extremely useful.<br><br></div><div>Thanks for your answer!<br><br>Gabor<br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">2013/7/23 Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div class="im">On Jul 23, 2013, at 10:33 AM, Gábor Kozár <<a href="mailto:kozargabor@gmail.com" target="_blank">kozargabor@gmail.com</a>> wrote:<br>
<div><br><blockquote type="cite"><span style="font-family:Helvetica;font-size:14px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">I'm building a checker that detects inconsistent pointer usages, for example when a pointer is dereferenced, then along the same path is null-checked (without its value changing in between, obviously).</span></blockquote>
</div><br></div><div>Hi Gabor,</div><div><br></div><div>I think the problem should be looked at in a different fashion. You should not need to reason about aliases at all. The analyzer engine handles this for you. It’s all symbolic execution.</div>
<div><br></div><div>One way to reason about this problem is that a pointer *value* has a notion of trust.</div><div><br></div><div>If it is trusted, it is safe to dereference. If it isn’t trusted, it isn’t safe to dereference. The trust level is a tri-state: { Trusted, NotTrusted, Unknown }. A pointer value needs to start in one of those states. It goes from { NotTrusted | Unknown } to { Trusted } by a null pointer check. The checker then fires if a { Trusted } pointer is checked for null.</div>
<div><br></div><div>There are details of course. First, this formalism isn’t necessary to model explicitly because the analyzer essentially already does this. “Trust” essentially means “constrained to be not-null”, “not trusted” means “known to be null” and “unknown” means unconstrained. Second, when does the check fire? A null check might not always be redundant. On some paths the null check may be redundant and others it won’t be. Thus there is a dominance relationship here that needs to be checked. Essentially, all paths need to show that the pointer is always non-null before the pointer is checked. Otherwise you’ll get false positives. Doing this correctly is hard, because not all paths are guaranteed to be traced. You’ll need to handle that too.</div>
<div><br></div><div>In this scheme, the pointer value is the symbolic region. You’ll essentially want to monitor the actual null checks of a symbolic region, and see if that region is constrained to always be non-null.</div>
<span class="HOEnZb"><font color="#888888"><div><br></div><div>Ted</div></font></span></div></blockquote></div><br></div>