[cfe-dev] [StaticAnalyzer] I think ExplodedGraph is wrong

[Anna Zaks via cfe-dev]

Thanks for digging into this! Looks like we are "caching out" when we should not. When analyzer sees the same exact node twice, it should cache out. One use case of that is ensuring we do not infinitely go around a loop.

The node consists of a ProgramPoint (like 'pc' or a location) and ProgramState. From what I can tell, here the root problem is that the program location changed, but it is not represented in the node. (However, in the patch you are trying to fix it by modifying the ProgramState.) As for the next steps, could you double check that the CFG for this looks correct? What do the ProgramPoints for this code look like? 

Thanks!
Anna.

> On Sep 9, 2016, at 4:25 AM, Aleksei Sidorin <a.sidorin at samsung.com> wrote:
> 
> Hm, seems like there is no difference between versions.
> 
> There is my understanding of the problem.
> We don't handle sym-sym comparisons well. The result of comparison between two symbols is an UnknownVal.
> First, analyzer renders "b >= Min" branch and assumes it false. Then, it renders operator '&&', then makes a cleanup which results in a new node with an empty state (1). It proceeds with false branch to operator! and then - to ReturnStmt.
> 
> Then, it renders branch where (b >= Min) is true. It assigns another UnknownVal to b < Max, cleanups ... and tries to create another empty-stated node before entering operator!. But there is already a node with an empty state and in the ProgramPoint. So, two execution paths are merged unexpectedly. And the analysis finishes since 'operator!' was rendered already for this merged branch.
> 
> I tried a quick solution which is the conjuring a symbolic value for comparisons instead of leaving it Unknown. It seems to work but I'm not sure if it is exactly what we need here. Anna, Artem, what is your opinion? Should we proceed with review or it is a bad idea in general?
> 
> 
> 
> 09.09.2016 12:05, Aleksei Sidorin via cfe-dev пишет:
>> Hello Daniel,
>> 
>> Thank you for report! Yes, I can confirm this bug. However, I cannot see this behaviour with an old version of clang: with clang-3.4.1 'b++' is still reachable. Will investigate.
>> 
>> 
>> 
>> 08.09.2016 18:06, Daniel Marjamäki via cfe-dev пишет:
>>> Hello!
>>> 
>>> When I analyze this code:
>>> 
>>>     extern int Min,Max;
>>>          void dfsd(int b) {
>>>         if (!(b >= Min && b < Max))
>>>           return;
>>>         b++;
>>>     }
>>> 
>>> It says that "b++;" is unreachable. When I look at the ExplodedGraph it seems to me that there is no node below the return. I would like to debug this. But I don't know where I should look. Do you have some idea?
>>> 
>>> Best regards,
>>> Daniel Marjamäki
>>> 
>>> .................................................................................................................. 
>>> Daniel Marjamäki Senior Engineer
>>> Evidente ES East AB  Warfvinges väg 34  SE-112 51 Stockholm Sweden
>>> 
>>> Mobile:                 +46 (0)709 12 42 62
>>> E-mail:                 Daniel.Marjamaki at evidente.se
>>> 
>>> www.evidente.se
>>> _______________________________________________
>>> cfe-dev mailing list
>>> cfe-dev at lists.llvm.org
>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>> 
>> 
> 
> 
> -- 
> Best regards,
> Aleksei Sidorin
> Software Engineer,
> IMSWL-IMCG, SRR, Samsung Electronics
>