[cfe-dev] exhaustiveness of CSA checkers

[Fernandez, Matthew via cfe-dev]

The loop unrolling itself is not so much of a problem. However, I think the control flow in the body of the loop causes path explosion. A sample loop looks something like:

    for (size_t i = 0; i < SOME_CONSTANT; i++) {
      if (some condition) {
        call_noreturn_function();
      }
    }

However loop unrolling is a secondary problem to me (I have other work arounds for the target loops). I think the real problem is the branching structure. Much of the function looks like:

    if (some condition)
      call_noreturn_function1();

    if (some other condition)
      call_noreturn_function2();

    ...

Based on a quick eyeballing, there are roughly 20 such branches in the target function. Adding up the '&&' and '||' operators used in the branch conditions, there's about 30 of these, which no doubt compounds the problem. We are certainly talking about a lot of paths here and I anticipated I would need to do some optimization, but I was surprised that (a) I can't seem to tune how early analysis terminates and (b) there is no way for my checker to observe this. Wrt (a), analysis seems to give up after ~19 calculated branches, and given this is 2**19 paths maybe this is reasonable. Wrt (b) I can't find a callback or way to observe this truncation. I guess my checker could define a destructor that validates whether it ever saw the end of the function, but this seems pretty hacky.

Given, as I mentioned, some of the properties I'm trying to check may be provable structurally, I'm going to try an AST visitor approach. Presumably this will scale far better than a path-sensitive analysis, but I was hoping I could leverage the path enumeration logic.

> -----Original Message-----
> From: Artem Dergachev <noqnoqneo at gmail.com>
> Sent: Wednesday, January 15, 2020 16:09
> To: Fernandez, Matthew <matthew.fernandez at intel.com>; Gábor Horváth
> <xazax at google.com>
> Cc: cfe-dev at lists.llvm.org
> Subject: Re: [cfe-dev] exhaustiveness of CSA checkers
> 
> Loop unrolling won't work on most loops if you don't remove the leashes in
> Static Analyzer's LoopUnrolling.cpp that i mentioned before. We don't have
> flags to control this yet (but i don't mind having some).
> 
> Other than that, it works for me most of the time when i debug false
> negatives. So your lack of success makes me curious about specifics. I might
> have forgotten something or it might be that something really curious is going
> on in your case.
> 
> 
> On 1/16/20 2:17 AM, Fernandez, Matthew wrote:
> > Thanks, Artem. Lots of useful flags. Unfortunately I have already
> experimented with all of them though.
> >
> >> -----Original Message-----
> >> From: Artem Dergachev <noqnoqneo at gmail.com>
> >> Sent: Wednesday, January 15, 2020 14:36
> >> To: Fernandez, Matthew <matthew.fernandez at intel.com>; Gábor Horváth
> >> <xazax at google.com>
> >> Cc: cfe-dev at lists.llvm.org
> >> Subject: Re: [cfe-dev] exhaustiveness of CSA checkers
> >>
> >> ...
> >> and also removing the artificial heuristics for loop unrolling (that
> >> attempt to discover whether the loop is statically bounded in
> >> LoopUnrolling.cpp) ...