[cfe-dev] Question on inspecting information across program paths

[Venugopal Raghavan via cfe-dev]

Hi,

I am registering my own map in the program state using the the following:

REGISTER_MAP_WITH_PROGRAMSTATE(ConstantMap, SymbolRef, VariableConstVal)

where VariableConstVal is the structure containing the information I want
in this map.

I am populating this map in the callback checkPostStmt() using state =
state->set<ConstantMap>(sym, ...) while the state graph is being
constructed.

At the end of analysis, I want to now read the information stored in this
map in the callback checkEndAnalysis(ExplodedGraph &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.

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:

  SVal val = state->getSVal(S, lctx);
  SymbolRef Sym = val.getAsSymbol();

but in checkEndAnalysis(ExplodedGraph &G, BugReporter &B, ExprEngine &Eng)
I do not seem to have a handle to stmt* to get the SVal.

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.

Thanks.

Regards,
Venugopal Raghavan.

On Wed, Jan 25, 2017 at 3:19 PM, Venugopal Raghavan <venur2005 at gmail.com>
wrote:

> Hi Aleksei,
>
> Thanks. I will check this.
>
> Regards,
> Venu.
>
> On Wed, Jan 25, 2017 at 3:15 PM, Aleksei Sidorin <a.sidorin at samsung.com>
> wrote:
>
>> Hello Venugopal,
>>
>> 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.
>>
>>
>> 25.01.2017 09:25, Venugopal Raghavan via cfe-dev пишет:
>>
>> Hi,
>>
>> Firstly, apologies for the long email below.
>>
>> 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:
>>
>> if (cond) {
>>    x = 4;
>> }
>> else {
>>    x = 5;
>> }
>>
>> L: .... = ...x..; // Use of variable x
>>
>> 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.
>>
>> 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.
>>
>> 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.
>>
>> 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?
>>
>> Thanks.
>>
>> Regards,
>> Venugopal Raghavan.
>>
>>
>> _______________________________________________
>> cfe-dev mailing listcfe-dev at lists.llvm.orghttp://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>
>>
>>
>> --
>> Best regards,
>> Aleksei Sidorin,
>> SRR, Samsung Electronics
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170201/39278f56/attachment.html>