<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">Hi Venugopal,<br>
<br>
There is a way to do it. The simplest way, as I guess, is to
create a chain of ExplodedNodes with your states. The code will
look similar to this:<br>
<br>
ProgramStateRef InitialState = C.getState();<br>
ProgramStateRef MarkedState =
InitialState->set<...>(...);<br>
if (ExplodedNode *MarkedNode =
C.generate[NonFatalError?]Node(MarkedState)) {<br>
ExplodedNode *NonMarkedNode =
C.generate[NonFatalError?]Node(InitialState, MarkedNode))<br>
}<br>
<br>
So, the chain will look like this:<br>
<InitialState, InitialNode> => <MarkedState,
MarkedNode> => <InitialState, NonMarkedNode><br>
<br>
But if you want to just add some mark to a newly-created node, you
can not use state at all. Instead, you can just create a node with
a specified tag.<br>
<br>
static SimpleProgramPointTag CustomTag("My marked node!");<br>
ExplodedNode *NodeWithSpecialTag =
C.generate[NonFatalError?]Node(NewState, C.getPredecessor(),
&CustomTag);<br>
<br>
<br>
<br>
13.02.2017 15:57, Venugopal Raghavan пишет:<br>
</div>
<blockquote
cite="mid:CANHhPPVnuFM7=knOc_nJCukqO8P3RGxjM+eqx+zaZyYNGMVcHA@mail.gmail.com"
type="cite">
<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 moz-do-not-send="true"
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
moz-do-not-send="true"
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
moz-do-not-send="true"
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
moz-do-not-send="true"
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
moz-do-not-send="true" 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
moz-do-not-send="true" 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 moz-do-not-send="true" 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 moz-do-not-send="true" 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>
</div>
</blockquote>
<p>
</p><pre class="moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></body></html>