<div dir="ltr">Hi Aleksei,<div><br></div><div>Thanks, I have re-written the checker based on your suggestion. </div><div><br></div><div>The custom program state that a checker adds to a program state gets propagated to succeeding states also unless they are explicitly removed. Is there a way to write some data into the custom state which is valid only for that state and does not get propagated to succeeding states? I did something like this:</div><div><br></div><div><div>ProgramStateRef state = C.getState(); // C is CheckerContext</div><div>const LocationContext *lctx = C.getLocationContext();</div><div>SVal val = state->getSVal(S, lctx);</div><div>SymbolRef Sym = val.getAsSymbol(); // Symbol I want to be added to this state and to this state alone</div></div><div><br></div><div>// Remove existing custom state data</div><div><div>const CustomStateTy &Syms = state->get<CustomState>();<br></div><div> for (auto I = Syms.begin(), E = Syms.end(); I != E; ++I) {</div><div> SymbolRef Sym1 = *I;</div><div> state = state->remove<CustomState>(Sym1);</div><div> }</div><div>state = state->add<CustomState>(Sym); // Add the symbol that is needed for the current state</div></div><div><br></div><div>The idea was to remove custom state information from a state and then write the information (symbol) corresponding to that state. Thus I write the symbol to a state S and that creates a new state S1 with that symbol. S itself is not modified since states are immutable. Now, the state which succeeds S1 (which I call S2) also gets the same symbol through state propagation which should however not be associated with that state. Hence I try remove the symbol from S2 but it does not actually remove it from that S2 but creates a new state S3 with the symbol removed (due to the immutable nature of states).</div><div><br></div><div>Finally, I would still be left with states such as S2 which has information which do not belong to them. Can I fix this in some way?</div><div><br></div><div>Not sure if this is a requirement outside the support provided by the analyzer or I have created a requirement which is unnatural.</div><div><br></div><div>Thanks.</div><div><br></div><div>Regards,</div><div>Venu.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 9, 2017 at 8:54 PM, Aleksei Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<div class="m_-3091663750839211701moz-cite-prefix">Hello Venugopal,<br>
<br>
Unfortunately, there is no a simple way to get "symbol diff". Your
approach with sequential iteration seems right to me in general.<br>
About comparison of symbols. If you want just ensure that some
symbols are same or different (like reg_$0<x> and
reg_$1<y> which are different), you can just compare their
pointers (SymbolRefs). Symbols are not modifiable, every symbol is
allocated in the pool and lives here, SymbolRefs just point on it.
If these pointers are different, symbols are different too, and
equal otherwise.<br>
<br>
<br>
09.02.2017 18:20, Aleksei Sidorin пишет:<br>
</div>
<blockquote type="cite">
<div class="m_-3091663750839211701moz-cite-prefix">Hello Venugopal,<br>
<br>
If you want just ensure that some symbols are same (like
reg_$0<x> and reg_$1<y>), you can just compare their
pointers (SymbolRefs). Symbols are not modifiable, every symbol
is allocated in the pool and lives here, SymbolRefs just point
on it. If these pointers are different, symbols are different
too, and equal otherwise.<br>
<br>
<br>
09.02.2017 13:03, Venugopal Raghavan пишет:<br>
</div><div><div class="h5">
<blockquote type="cite">
<div dir="ltr">Hi,
<div><br>
</div>
<div>Apologies, but, I am back again. </div>
<div><br>
</div>
<div>I have two SymbolRef pointers (SymExpr *). One SymbolRef
is (reg_$0<x>) + 3$117. The other SymbolRef
is (reg_$0<x>) + 2$130. x is a variable in my program
and these SymbolRefs respresent an assignment of x + y to a
variable "a". y has the value 3 along one path to the
program point where "a" is assigned and it has the value 2
along a second path to the same point, hence the two
SymbolRefs differ in the constants.</div>
<div><br>
</div>
<div>I want to compare these two SymbolRefs and find out where
they differ. In this case, I want to be able to say that
they differ in the constant value. I thought of using
symbol_iterator to iterate over each SymbolRef or SymExpr *
in lock-step fashion and find the first point where it
differs. But these is no operator== defined in the SymExpr
class and hence I am unable to check the equality or
otherwise of two symbols in the SymbolRefs.</div>
<div><br>
</div>
<div>Is there a way to compare two SymbolRefs and check for
the differences? Otherwise, is there a better way to check
whether the symbolic value at the same program point but in
two different program states are the same or not, and if
they are different, is there a way to identify the
difference? Maybe, my approach of comparing two symbolic
expressions at a program point is not the right approach in
the first place.</div>
<div><br>
</div>
<div>Thanks.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Venu.</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Mon, Feb 6, 2017 at 2:42 PM,
Venugopal Raghavan <span dir="ltr"><<a href="mailto:venur2005@gmail.com" target="_blank">venur2005@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 dir="ltr">Hi Aleksei,
<div><br>
</div>
<div>Thanks. That seems to work.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Venu.</div>
</div>
<div class="m_-3091663750839211701HOEnZb">
<div class="m_-3091663750839211701h5">
<div class="gmail_extra"><br>
<div class="gmail_quote">On Mon, Feb 6, 2017 at 2:05
PM, Aleksei Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<div class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645moz-cite-prefix">Hello,<br>
<br>
On the point where PreStmt callbacks are
called, the expression value is still not
computed so the result of getSVal() is
always UnknownVal and not a symbol. You
should probably use PostStmt callback
instead.<br>
<br>
<br>
06.02.2017 08:21, Venugopal Raghavan пишет:<br>
</div>
<div>
<div class="m_-3091663750839211701m_-1035519723042365625h5">
<blockquote type="cite">
<div dir="ltr">Hi Aleksei,
<div><br>
</div>
<div>Thanks for the reply.
Unfortunately, I am having further
trouble with my checker
implementation. I have the following
code in my checker (called
ConstantChecker):</div>
<div><br>
</div>
<div>
<div> void
ConstantChecker::checkPreStmt(<wbr>const
Stmt *S, CheckerContext &C)
const {</div>
<div> ProgramStateRef state =
C.getState();</div>
<div> const LocationContext
*lctx = C.getLocationContext();</div>
<div> SVal val =
state->getSVal(S, lctx);</div>
<div> SymbolRef Sym =
val.getAsSymbol(); </div>
</div>
<div> // Stmt 1</div>
<div> .</div>
<div> .</div>
<div> .</div>
<div>}</div>
<div> </div>
<div>My input test case for the
checker is test1.c and I run the
command clang -cc1 -analyze
-analyzer-checker=optin.perfor<wbr>mance.PathSpecificConstants
test1.c where PathSpecificConstants
is the name of my checker:</div>
<div><br>
</div>
<div>
<div>test(int x) {</div>
<div> int y;</div>
<div> int a;</div>
<div> if (x > 0) {</div>
<div> y = 2;</div>
<div> }</div>
<div> else {</div>
<div> y = 3;</div>
<div> }</div>
<div> a = x + y;</div>
<div> printf("a = %d\n", a);</div>
<div>}</div>
</div>
<div><br>
</div>
<div>When I print "Sym" in gdb at the
break point Stmt 1, I always get Sym
as 0x0. This probably means that val
is never a symbol for my test case
and hence val.getAsSymbol() fails. I
do not understand this. I would have
thought that at least the expression
x + y would be represented by a
symbolic value such as $0. I tried
doing const MemRegion *mem =
val.getAsRegion() also at that
point and tried to print out mem in
gdb. That also has a value 0x0
except for the printf statement. I
cannot understand this too. I would
have expected variables such as "x",
"y" and "a" to be associated with a
memory region and hence mem to have
a non-null value at least at the
points where y and a are being
assigned to.</div>
<div><br>
</div>
<div>My plan was to use Sym as the
index into a custom map that I have
created where I am storing the
values of constants seen in the test
case. I am unable to get this plan
working since Sym is always 0x0.</div>
<div><br>
</div>
<div>I have gone through the Checker
Developer Manual. I am sorry to be
asking specific questions about my
code in this fashion, but,
unfortunately, I am stuck at this
point.</div>
<div><br>
</div>
<div>Thanks.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Venugopal Raghavan.</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Wed, Feb
1, 2017 at 11:13 PM, Aleksei Sidorin
<span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<div class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662moz-cite-prefix">Hello
Venugopal,<br>
<br>
You will need to extract all
the information from
ExplodedNodes.<br>
For example, state is a part
of ExplodedNode. So, you can
iterate over ExplodedNodes of
graph using smth like:<br>
for (auto Iter =
G.nodes_begin(), E =
G.nodes_end(); I != E; ++I) {<br>
ProgramStateRef State =
I->getState();<br>
// Do the stuff with State<br>
}<br>
<br>
<br>
<br>
<br>
01.02.2017 12:19, Venugopal
Raghavan пишет:<br>
</div>
<div>
<div class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645h5">
<blockquote type="cite">
<div dir="ltr">Hi,
<div><br>
</div>
<div>I am registering my
own map in the program
state using the the
following:</div>
<div><br>
</div>
<div>REGISTER_MAP_WITH_PROGRAMSTATE<wbr>(ConstantMap,
SymbolRef,
VariableConstVal)<br>
</div>
<div><br>
</div>
<div>where
VariableConstVal is
the structure
containing the
information I want in
this map. </div>
<div><br>
</div>
<div>I am populating
this map in the
callback checkPostStmt()
using state =
state->set<ConstantMap>(sym,
...) while the state
graph is being
constructed.</div>
<div><br>
</div>
<div>At the end of
analysis, I want to
now read the
information stored in
this map in the
callback checkEndAnalysis(Expl<wbr>odedGraph
&G, BugReporter
&B, ExprEngine
&Eng). However, I
am not sure how to get
the SymbolRef
associated with an
ExplodedNode which is
what I get when I
iterate over the
ExplodedGraph at the
end of the analysis.</div>
<div><br>
</div>
<div>How can I get the
SymbolRef that I can
use to index into my
map? In
checkPostStmt(stmt* S,
CheckerContext
&C), I used the
following code to get
the SymbolRef that I
can use to store the
information in the
map:</div>
<div><br>
</div>
<div>
<div> SVal val =
state->getSVal(S,
lctx);</div>
<div> SymbolRef Sym =
val.getAsSymbol();</div>
</div>
<div><br>
</div>
<div>but in
checkEndAnalysis(ExplodedGraph
&G, BugReporter
&B, ExprEngine
&Eng) I do not
seem to have a handle
to stmt* to get the
SVal.</div>
<div><br>
</div>
<div>I guess my question
is probably not
phrased very well, but
I hope some one can
make some sense out of
it. Also, I guess I
have a long way to go
before I understand
the data structures in
the analyzer well. I
checked the other
checkers, but none of
them seem to exhibit
exactly my
requirement.</div>
<div><br>
</div>
<div>Thanks.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Venugopal Raghavan.</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On
Wed, Jan 25, 2017 at
3:19 PM, Venugopal
Raghavan <span dir="ltr"><<a href="mailto:venur2005@gmail.com" target="_blank">venur2005@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 dir="ltr">Hi
Aleksei,
<div><br>
</div>
<div>Thanks. I
will check this.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Venu.</div>
</div>
<div class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662HOEnZb">
<div class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662h5">
<div class="gmail_extra"><br>
<div class="gmail_quote">On
Wed, Jan 25,
2017 at 3:15
PM, Aleksei
Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<div class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-cite-prefix">Hello
Venugopal,<br>
<br>
During
analysis, you
have access to
a single path
only. But
after the
analysis is
done, you can
summarize
information
across
different
paths using
checkEndAnalysis()
callback. You
will get full
ExplodedGraph
built for the
function so
you will be
able to look
into its every
node.<br>
<br>
<br>
25.01.2017
09:25,
Venugopal
Raghavan via
cfe-dev пишет:<br>
</div>
<blockquote type="cite">
<div>
<div class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944h5">
<div dir="ltr">Hi,
<div><br>
</div>
<div>Firstly,
apologies for
the long email
below.</div>
<div><br>
</div>
<div>I am new
to the Clang
Static
Analyzer
(CLA). My
interest in
CLA was more
to see if I
can solve
quickly
path-sensitive
data-flow
analysis
problems than
as a vehicle
to build
bug-finding
checkers. I
needed the
solutions to
such data flow
problems to
extract some
behavioral
properties
from some test
cases I have.
For example,
consider the
following
piece of code:</div>
<div><br>
</div>
<div>if (cond)
{</div>
<div> x = 4;</div>
<div>}</div>
<div>else {</div>
<div> x = 5;</div>
<div>}</div>
<div><br>
</div>
<div>L: .... =
...x..; // Use
of variable x</div>
<div><br>
</div>
<div>I want to
identify
program
locations such
as "L" in the
code above
where x is not
a constant if
you aggregate
data-flow
information
across paths,
but, on the
other hand, is
actually a
constant if
you have
path-specific
data flow
information.
Since CFA does
path-specific
analysis, I
was curious to
know if it
would help me
with such
tasks. The
"bug-report" I
want at
location L is
that x has a
value 4, given
the path
constraint for
the path
including the
"then-path" of
the if
statement and
that x has a
value 5 along
the else-path.</div>
<div><br>
</div>
<div>I started
writing a
checker to
accomplish the
above task,
but was
quickly
blocked by
some basic
doubts. My
rough plan for
the checker
was to
maintain a map
in
ProgramState
which maps
ProgramPoints
(or, maybe
program
symbols) to
constants when
those
variables
indeed have
constant
values at the
ProgramPoint.
For example,
when CFA
expands states
along the
then-path and
reaches "L",
my map would
say that at
ProgramPoint
"L", variable
x has a
constant value
4. Then, when
CFA expands
nodes along
the else-path,
I guess it
would again
create a state
corresponding
to L which now
says that x
has the
constant value
5. I want to
be able to
catch this
scenario where
the same
variable at
the same
ProgramPoint
has two
different
constant
values
depending on
the path
taken.</div>
<div><br>
</div>
<div>However,
the issue is
that, when the
state graph
along the
else-path is
expanded, it
would no
longer have
any of the map
contents that
was built
along the
disjoint
then-path. How
then can I get
access to the
then-path
information
when I am
expanding the
path along the
else-path?
Since the
checker is
also required
to be
stateless, I
cannot
maintain
auxiliary
information in
the checker
that is
persistent
across
multiple calls
to the
call-back
function. </div>
<div><br>
</div>
<div>Can you
help me with
this question?
Maybe, I am
trying to use
CFA in ways it
was not meant
to be used
viz. as a
vehicle to
solve data
flow problems
which consults
information
cutting across
paths. Maybe,
the CFA is
meant to
handle
problems which
require the
examination of
information
restricted to
single paths.
Is that the
case? Or, am I
missing
something?</div>
<div><br>
</div>
<div>Thanks.</div>
<div><br>
</div>
<div>Regards,</div>
<div>Venugopal
Raghavan.</div>
</div>
<br>
<fieldset class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759mimeAttachmentHeader"></fieldset>
<br>
</div>
</div>
<pre>______________________________<wbr>_________________
cfe-dev mailing list
<a class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-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><span class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></pre><span class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></blockquote><span class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
<p>
</p>
<pre class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>
</font></span></div>
</blockquote></div>
</div>
</div></div></blockquote></div>
</div>
</blockquote>
<p>
</p><pre class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div>
</div>
</blockquote>
<p>
</p><pre class="m_-3091663750839211701m_-1035519723042365625m_4390566528069532645moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div>
</div>
</div></div></blockquote></div>
</div>
</blockquote>
<p>
</p><pre class="m_-3091663750839211701moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>
</div></div></blockquote><div><div class="h5">
<p>
</p><pre class="m_-3091663750839211701moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div><br></div>