Fast and Precise Interval Analysis on Industry code

This paper introduces an algorithm for data-flow analysis using functional approach to solve infinite-height analyses, such as interval analysis. The algorithm utilizes function summaries and employs a combination of one bottom-up and multiple top-down traversals over the call graph, referred to as OneBMultiT. The OneBMultiT approach is further extended to enable incremental analysis for code changes by selectively analysing only affected functions, referred to as ONEBMULTIT<inf xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">incr</inf>. We have implemented the interval analysis and incrementalized it using the proposed algorithms in our proprietary static analysis tool. The analysis results of interval analysis are used to validate properties such as array index within bounds, non-zero division, and the prevention of arithmetic overflow/underflow on real-life applications. Our evaluation shows that 93% properties on four automotive applications are successfully validated. Additionally, ONEBMULTIT<inf xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">incr</inf> approach yields up to 83% reduction in analysis time and a significant reduction in reported alarms in comparison to whole program analysis, demonstrating its practical benefit on real-world evolving applications.