Linear relation analysis (polyhedral analysis), devoted to discovering
linear invariant relations among variables of a program, remains one of
the most powerful abstract interpretations but is subject to convexity
limitations. Absolute value enjoys piecewise linear expressiveness
and thus natively fits to encode certain non-convex properties.
Based on this insight, we propose to use linear absolute value relation
analysis to discover linear relations among values and absolute values of
program variables.
A first result states the
equivalence between these “linear absolute value inequalities” (AVI)
with “interval linear inequalities” (ILI), and “extended linear
complementary inequalities” (XLCP, pairs of positive solutions whose
pairwise components are not both not zero).
Under the framework of abstract interpretation, the
analysis yields a new numerical abstract domain, namely the abstract domain of
linear absolute value inequalities
(Σk ak xk +
Σk bk |xk| ≤ c),
which can be used to analyze programs involving piecewise linear behaviors (e.g., due to conditional branches or absolute value function calls). The key contribution is the
extension of the double-description of polyhedra to XLCP solutions,
which is then used to define the standard operations on AVI.
Experimental results of our prototype are encouraging; The new abstract domain can find non-convex invariants of interest in practice.
\bibitem{ChenMineWangCousot-ESOP-11}
Liqian Chen, Antoine Min{\'e}, Ji Wang, and Patrick Cousot.
\newblock Linear Absolute Value Relation Analysis.
\newblock In 20th European Symposium on Programming (ESOP 2011),
G.~Barthe (Ed.), March 26 -- April 3, 2011, Saarbr{\"u}cken, Germany.
\newblock Lecture Notes in Computer Science, Vol. 6602, pages 156--175,
Springer-Verlag, Heidelberg, 2011.
@incollection{ChenMineWangCousot-ESOP-11,
author = "Liqian Chen and Antoine Min{\'e} and Ji Wang and Patrick Cousot",
title = "Linear Absolute Value Relation Analysis",
booktitle = "20th European Symposium on Programming (ESOP 2011), Saarbr{\"u}cken, Germany",
editor = "G.~Barthe",
series = "Lecture Notes in Computer Science",
volume = {6602},
publisher = "Springer-Verlag",
address = "Heidelberg",
pages = "156--175",
month = { March 26 -- April 3, },
year = 2011,
}