<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="HOEnZb"><div class="h5"><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_-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_-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_-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_-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_-1035519723042365625m_4390566528069532645m_4335525358519862662HOEnZb">
<div class="m_-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_-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_-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_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759mimeAttachmentHeader"></fieldset>
<br>
</div>
</div>
<pre>______________________________<wbr>_________________
cfe-dev mailing list
<a class="m_-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_-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_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></pre><span class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></blockquote><span class="m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
<p>
</p>
<pre class="m_-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_-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_-1035519723042365625m_4390566528069532645moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>