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

[Aleksei Sidorin via cfe-dev]

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 list
> cfe-dev at lists.llvm.org
> http://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/20170125/a6542900/attachment.html>