[PATCH] Division by zero

[Ted Kremenek]

The dead stores checker is an example of a CFG-based check.  That checker rides on top of the live variables analysis (which is CFG-based), so really the guts of the analysis of the checker are there.  The analysis for -Wuninitialized is also dataflow-based, although that is a compiler warning instead of a checker, but it works exactly the same way.

Essentially you do a dataflow analysis to collect possible facts at each basic block, propagating facts forward as you analyze the statements of a basic block.  You then "merge" values at confluence points, which are the basic blocks with multiple predecessors.  That merging is what makes the analysis path-insensitive, but flow-sensitive.  Path-insensitive analyses are dramatically faster, but for many of the properties the static analyzer looks for they are too imprecise.  For this checker it may be the case you don't need path-sensitivity, which is why Jordan suggested it.  If it can be implemented as path-insensitive, it then has the possible chance of becoming a compiler warning one day.

> On Aug 11, 2014, at 11:58 PM, Anders Rönnholm <Anders.Ronnholm at evidente.se> wrote:
> 
> Hi Jordan,
>  
> I don’t know if I have the time to change division by zero right away but I can make the dereference check CFG-based. Do you have an example of a CFG-based checker? I don’t know how to make those.
>  
> //Anders
>  
> From: Jordan Rose [mailto:jordan_rose at apple.com] 
> Sent: den 21 juli 2014 19:40
> To: Anders Rönnholm
> Cc: cfe-commits at cs.uiuc.edu; Daniel Marjamäki; Anna Zaks
> Subject: Re: [PATCH] Division by zero
>  
> So, Anna brought up that the check as implemented is very nearly path-independent, i.e. it only depends on flow-sensitive properties of the CFG. The path-sensitivity is buying us very little; it catches this case:
>  
> int y = x;
> int div = z / y;
> if (x) { ...}
>  
> But also warns here, which doesn't necessarily make sense:
>  
> int foo(int x, int y, int z) {
>         int div = z / y;
>         if (x) return div;
>         return 0;
> }
>  
> foo(a, a, b); // only coincidentally the same symbol
>  
> What would you think about turning this (and/or the null dereference check) into a CFG-based check instead? We lose the first example (and cases where inlining would help), but fix the second, and very possibly speed up analysis. CFG analysis is also more capable of proving that something happens on all paths rather than just some, since that's just propagating information along the graph.
>  
> Jordan
>  
>  
> On Jul 10, 2014, at 9:55 , Anders Rönnholm <Anders.Ronnholm at evidente.se <mailto:Anders.Ronnholm at evidente.se>> wrote:
> 
> 
> Great, no problem. I'll move forward with my dereference then check patch now that this one is commited, which will be pretty similar.
> 
> //Anders
> 
> .......................................................................................................................
> Anders Rönnholm Senior Engineer
> Evidente ES East AB  Warfvinges väg 34  SE-112 51 Stockholm  Sweden
> 
> Mobile:                    +46 (0)70 912 42 54
> E-mail:                    Anders.Ronnholm at evidente.se <mailto:Anders.Ronnholm at evidente.se>
> 
> www.evidente.se <http://www.evidente.se/>
> 
> ________________________________________
> Från: Jordan Rose [jordan_rose at apple.com]
> Skickat: den 10 juli 2014 18:20
> Till: Anders Rönnholm
> Cc: cfe-commits at cs.uiuc.edu <mailto:cfe-commits at cs.uiuc.edu>; Daniel Marjamäki
> Ämne: Re: [PATCH] Division by zero
> 
> Thank you for going through so many rounds of review on this. Committed in r212731! (The one change I made was to reset the test in isZero to use assume instead of assumeDual, now that my confusion has been fixed.)
> 
> Jordan
>  
> _______________________________________________
> cfe-commits mailing list
> cfe-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20140812/0bfa2f8d/attachment.html>