Context Gas and friends: taming context-sensitivity on the fly

Abstract Context-sensitive analysis of programs containing recursive procedures may be expensive. This may particularly be the case when expressive domains are used, rendering the set of possible contexts large or even infinite. Here we present a framework for context-sensitivity and, as a base step, show how to formalize full contexts, partial contexts, and call strings in it. In this framework, we propose three generic lifters that allow bounding the number of encountered contexts for existing analyses on the fly, i.e., without requiring a preanalysis: Context Widening , Loopfree Callsting , and Context Gas . The proposed analysis lifters maintain the soundness of the underlying base analyses. For these approaches, we prove that only finitely many function contexts are encountered during fixpoint iteration—a key requirement for termination—when the fixpoint iteration is known to update the value of each unknown only a finite number of times. Context Gas and friends are implemented within the abstract interpreter Goblint and compared to existing approaches to context-sensitivity on the SV-COMP benchmark suite. On a subset of recursive benchmarks, all proposed lifters manage to reduce the number of stack overflows and timeouts compared to a full context approach, with one configuration of the Context Gas approach improving the number of correct verdicts by $31\%$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mn>31</mml:mn> <mml:mi>%</mml:mi> </mml:math> and showing promising results on the considered SV-COMP categories.