An Abstract Domain of Linear Templates with Disjunctive Right-Hand-Side Intervals

Abstract interpretation provides a general framework for analyzing the value ranges of program variables while ensuring soundness. Abstract domains are at the core of the abstract interpretation framework, and the numerical abstract domains aiming at analyzing numerical properties have received extensive attention. The template constraint matrix domain (also called the template polyhedra domain) is widely used due to its configurable constraint matrix (describing limited but user-concerned linear relationships among variables) and its high efficiency. However, it cannot express non-convex properties that appear naturally due to the inherent disjunctive behaviors in a program. In this paper, we introduce a new abstract domain, namely the abstract domain of linear templates with disjunctive right-hand-side intervals, in the form of \(\sum _{i} a_ix_i \in \bigvee _{j=0}^p [c_j,d_j]\) (where \(a_i\) ’s and p are configurable and fixed before conducting analysis). Experimental results of our prototype are encouraging: In practice, the new abstract domain can find interesting non-convex invariants that are out of the expressiveness of the classic template constraint matrix abstract domain.