[cfe-dev] exhaustiveness of CSA checkers

[Gábor Horváth via cfe-dev]

Hi!

I am not sure what are you planning to do based on the AST, but you might
want to look into the clang CFG and the ExprSequence class in clang-tidy
[1]. They might prove useful for you.

Cheers,
Gabor

[1]:
https://github.com/llvm/llvm-project/blob/master/clang-tools-extra/clang-tidy/utils/ExprSequence.h#L68

On Thu, Jan 16, 2020 at 11:21 AM Fernandez, Matthew <
matthew.fernandez at intel.com> wrote:

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