Access-Based Localization for Octagons

Access-based localization is a two-step process. First, the set of abstract memory locations that are accessed in a procedure are determined. Then, in a subsequent fixed point iteration, the input to the respective procedure is reduced to those variables that are indeed accessed, thereby saving time and memory. The topic of this paper is access-based localization for the octagon abstract domain. For the frequently occurring scenario that only one out of two variables in some octagonal constraint is contained in the access-set of a procedure, there is a variety of opportunities how localization could be implemented. This paper presents three different approaches on how to deal with such constraints. Albeit applied to a subset of the abstract state space, two of these approaches preserve precision, i.e., the abstract state space is as precise as in the case that no localization is performed.