[StaticAnalyzer] I think ExplodedGraph is wrong


When I analyze this code:

    extern int Min,Max;
    void dfsd(int b) {
        if (!(b >= Min && b < Max))

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@evidente.se


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 пишет:

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 пишет:

A very initial version of patch for this issue is here: https://reviews.llvm.org/D24384

09.09.2016 14:25, Aleksei Sidorin 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?


Hello Anna,

Broken CFG was the first idea I had. However, it was correct and had all the branches we need (nothing unexpected). But I cannot remember what happened with ProgramPoints (I cannot check it now, sorry). Will re-check on Monday.

09.09.2016 23:51, Anna Zaks via cfe-dev пишет: