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

[Venugopal Raghavan via cfe-dev]

Hi,

Please read CSA wherever I have used CLA or CFA. Sorry about that.

Regards,
Venugopal Raghavan.

On Wed, Jan 25, 2017 at 11:55 AM, Venugopal Raghavan <venur2005 at gmail.com>
wrote:

> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170125/8088132a/attachment.html>