On the Properties of Partial Completeness in Abstract Interpretation (Short Paper)⋆ Marco Campion 0 Mila Dalla Preda 0 Roberto Giacobazzi 0 University of Verona , Italy eol>Abstract Interpretation Program Analysis Computability Partial Completeness 1. Introduction

represents the ideal situation where no false alarms are produced. Completeness, however, is a very rare condition to be satisfied in practice, therefore, static program analysis needs to, in some way, deal with incompleteness. Moreover, the experience tells us that there are results that are “more incomplete”, i.e., less precise, than others, and this depends upon the way the program is written and the way the abstract interpreter is implemented [ 7 ]. As an example, consider the following program ::= while > 1 do := − 2 if = 1 then := 10 if = 2 then := 100 and the set of values {2, 4}. Clearly J K{2, 4} = {0}. However, when is analyzed by an abstract interpreter J KInt (e.g., see [6, Chapter 4.5]) which considers abstract arithmetical operators as the best correct approximation (bca for short), defined on the abstract domain of intervals Int ≜ {[, ] | , ∈ Z ∪ {−∞ , +∞}, ≤ } ∪ {⊥Int} [ 2 ] or defined as the bca for Int, namely, J KIbncat ≜ Int ∘ J K ∘ Int ∘ Int, then it may exhibit diferent levels of imprecision . Recall that Int abstracts sets of integer values and it contains all intervals [, ] such that , ∈ Z±∞ where Z±∞ ≜ Z ∪ {−∞ , +∞} , and ≤ . So, for the input of we get Int({2, 4}) = [ 2, 4 ], while for the output we obtain the single point Int(J K{2, 4}) = [0, 0]. Then, for the two mentioned analysis of we get J KIbncat{2, 4} = [ 0, 10 ] and J KInt Int({2, 4}) = [0, 100]. Note the three diferent interval properties obtained by the concrete, bca and abstract evaluations of over Int with input {2, 4}: [0, 0] ≤ Int [ 0, 10 ] ≤ Int [0, 100]. These discrepancies are what we want to measure.

To this end, we consider a weaker form of metric function that is made specific for the elements of an abstract domain, namely, it is compatible with the underlying ordering relation ≤ , hence taking into account the presence of incomparable elements. This distance function incorporates both the qualitative comparison given by the partial order and a quantitative comparison (Section 2). By exploiting this idea, we can introduce the notion of -partial completeness of an abstract domain with respect to a given program and a given (set of) input values (Section 3). A partially complete abstract interpretation allows some false-alarms to be reported, but their number is bounded. In this case, the imprecision of the abstract interpreter is bounded by , namely, the distance between the property represented by the abstraction of the concrete semantics and the result of the abstract interpretation on the given input, is at most . Given a tolerance of imprecision and a set of inputs , we want to answer the following questions (Section 4): Can we implement a program analyzer such that all programs having as input are -partial complete? Can we prove if our program analysis has or not a bounded level of imprecision?

 2. Quasi-metrics on Abstract Domains

Our goal is to derive the bound of imprecision of an abstract interpreter with respect to a given measure over the abstract domain. For this reason, we need a metric to compare the elements of the abstract domain according to their relative degree of precision. We refer to the weaker notion of quasi-metric introduced in [ 8 ] on a non-empty set . This is a metric function : × → Q≥ 0 whose symmetry property may not hold. A set endowed with a quasi-metric is called quasi-metric space. Let () be the set of all abstract domains abstracting some set of concrete properties and having ordering relation ≤ 2.

Definition 2.1 (Quasi-metrics -compatible). We say that the distance function : × → N≥∞0 ∪ {⊥} is a quasi-metric -compatible for ∈ () if for all 1, 2, 3 ∈ , it satisfies the following axioms: (i) 1 = 2 ⇔ (1, 2) = 0 (ii) 1 ≤ 2 ⇔ (1, 2) ̸= ⊥ (iii) 1 ≤ 2 ≤ 3 ⇒ (1, 3) ≤ (1, 2) + (2, 3) (iv) ∀1, 2 ∈ , ∈ N≥ 0 the predicate (1, 2) ≤ is decidable.

We allow the quasi-metric between two uncomparable elements to be ⊥, which represents an undefined distance. An abstract domain ∈ () endowed with a quasi-metric -compatible , forms an abstract quasi-metric space, denoted by ≜ (, ). We use A() to refer to the set of all abstract quasi-metric spaces, and write ∈ A().

As an example of quasi-metric -compatible, we define the weighted path-length w as the minimum weighted path, w.r.t. a weight function w, of intermediate elements between two comparable elements of an abstract domain . Here w considers the lattice of as a weighted directed graph where each edge corresponds to two adjacent abstract elements , , that is, ≤ and there are no elements ∈ such that ≤ ≤ . So for example, Iwnt over the intervals abstraction having w(· , · ) = 1, i.e., setting to 1 the weight of each edge of Int, returns 9 between [0, 0] and [ 0, 10 ] meaning that there are exactly 9 more elements in [ 0, 10 ] respect to [0, 0], while Iwnt([0, 0], [0, +∞]) = ∞ and Iwnt([0, 0], [ 1, 10 ]) = ⊥ because [0, 0] ̸≤ Int [ 1, 10 ].

3. Partial Completeness

Standard completeness in program analysis3, e.g., see [ 2, 3, 13 ], means that no false alarms are returned by analyzing the program with an abstract interpreter on any possible input state. Local completeness, instead, is a recently introduced property [ 14 ] that requires completeness only with respect to specific inputs. An -partially complete program analyzer allows some false alarms to be reported over a considered (set of) input, but their amount is bounded by a constant which is determined according to a quasi-metric which is compatible with the abstract domain used by the analysis. Formally, given a program ∈ Programs, a constant bound ∈ N≥ 0, a non-empty set of stores ∈ ℘(S) and ∈ A(℘(S)), we say that is -partially complete for in if (J K) ≤ J K (), where ≤ if (, ) ≤ . We now have all the ingredients to introduce the notion of -partial completeness class of programs. 2We consider abstract domains in () that are either recursive or trivial [ 9, 1 ]. 3In some topics concerning abstract interpretation, completeness is typically recurrent, e.g., in comparative semantics [ 10, 11 ] or formal languages [ 12 ]. Here we are considering only the field of program analysis. Definition 3.1 (-Partial completeness class). The partial completeness class of an abstract quasi-metric space ∈ A(℘(S)), a constant ∈ N≥ 0 and a non-empty set of inputs ∈ ℘(S), denoted C(, , ) ⊆ Programs, is defined as:

C(, , ) ≜ { ∈ Programs | (J K) ≤ J K ()}.

Similarly to the completeness case [ 15 ], for every , the -partial completeness class is infinite and non-extensional. It is infinite because for all ∈ N≥ 0 and ∈ ℘(S), C() ⊆ C(, , ) and C() is infinite, where C() denotes the (global) completeness class of programs. It is also non-extensional because there always exist programs and such that: is partially complete for , J K = JK, and is not partially complete for .

4. Recursive Properties of Partial Complete Programs

It is well known that for trivial abstractions (i.e., either the identity or an abstraction having one element only) the corresponding completeness class turns out to be the whole set of programs [ 13 ]. Moreover, for all non-trivial abstractions in (℘(S)), its completeness class is strictly contained in Programs [ 15 ]. In this section, we study the counterpart of these results for the case of partial completeness. It turns out that the quasi-metric -compatible chosen for measuring the imprecision of the analysis, plays an important rule here in order to determine the recursive properties of C(, , ) and, therefore, of the considered program analysis. We first consider the simplest case of abstract quasi-metric spaces of stores ∈ A(℘(S)) satisfying the property of having a limited imprecision by ∈ N≥ 0, i.e., abstractions such that ∀ ∈ : (⊥, ) ≤ . These include, for instance, the case of finite height lattices with the weighted path-length quasi-metric—complete lattices which are both ACC and DCC. Theorem 4.1. If ∈ A(℘(S)) has limited imprecision, then we have for all ∈ ℘(S): ∃ ∈ N≥ 0. C(, , ) = Programs .

For example, the Sign ≜ {Z, − , 0, +, ∅} abstraction [ 16 ] measured with Swign having w(· , · ) = 1, has limited imprecision because by for any ≥ 3, the partial completeness class turns out C((Sign, Swign), , ) = Programs. The diference with respect to the case of standard completeness class C() is that, thanks to the possibility of admitting an upper margin to imprecision (i.e., possible false alarms), there always exists a class of partial completeness with respect to a given bound which includes all programs.

Conversely, an abstract quasi-metric space of stores ∈ A(℘(S)) has unlimited imprecision when: ∀ ∈ N≥ 0, ∃ ∈ . (⊥, ) > . The abstract quasi-metric space (Int, Iwnt) is such an example.

Theorem 4.2. Let ∈ A(℘(S)) be any abstract quasi-metric space of stores with unlimited imprecision and ∈ ℘(S). Then, the following equivalence holds: ∃ ∈ N≥ 0. C(, , ) = Programs ⇔ = ℘(S).

Informally, if we consider a non-trivial abstract quasi-metric space that has unlimited imprecision and an input , then independently of how we set a threshold of false alarms acceptance, there always exists a program for which the abstract analysis over with input , is not -partially complete, namely ̸∈ C(, , ). By a straightforward padding argument, any of these programs can be extended to an infinite set of programs for which the abstraction is -partially incomplete. The class of -partial incomplete programs for ∈ A(℘(S)) with input , is the complement set of C(, , ), formally: C(, , ) = { ∈ Programs | (J K) ̸≤ J K ()}. Theorem 4.2 implies that any non-trivial abstract domain of stores endowed with an unlimited imprecision , has an infinite set of programs for which the abstract interpreter is -partially incomplete. Conversely, if has limited imprecision, then, trivially, we can always ifnd a certain level of tolerance that makes the analysis -partially complete for all programs.

We now study the computational limits of the class of partially complete and incomplete programs. In this case, the topological structure of in terms of ascending chains, is fundamental. We say that an abstract quasi-metric space of stores ∈ A(℘(S)) is -trivial for some ∈ N≥ 0 if C(, , ) = Programs. The following theorem shows that the class of programs C(, , ) turns out to be recursively enumerable (r.e.) whenever the abstract domain of stores satisfies the Ascending Chain Condition (ACC).

Theorem 4.3. If ∈ A(℘(S)) is ACC, then for every ∈ ℘(S) and ∈ N≥ 0, C(, , ) is r.e.. Sketch. Run a dovetail algorithm constructing the set ≜ ⨆︀∈N{ (J K)} starting from = ⊥, where ∈ is an enumeration of . If, at some point of the iterates, there exists ∈ such that J K ̸= ∅, = ⊔ (J K) and (, J K ()) ≤ , then the algorithm terminates. If ∈ C(, , ) then the convergence of the above algorithms is guaranteed by the ACC of .

The following theorem states that both C(, , ) and C(, , ) are non-r.e. sets when is not -trivial and not ACC.

Theorem 4.4. If ∈ A(℘(S)) is not -trivial, then C(, , ) is non-r.e.. Moreover, if is also not ACC, then C(, , ) is non-r.e..

As a straightforward corollary, the local completeness class C(, ) for satisfying the ACC property is r.e., while non-r.e. for non-ACC abstractions. Furthermore, if is not trivial, then C(, ) is non-r.e. even if is ACC. Let us notice that Theorems 4.3 and 4.4 provide a further insight into the structure of C(, , ) and its complement class C(, , ). These theorems prove that, given any non-ACC abstract quasi-metric space of stores , whenever we limit the expected imprecision of our analysis to a bound of possible false alarms w.r.t. an input , we cannot build a procedure that enumerates all programs satisfying that bound or that do not respect that bound, unless the abstract domain is -trivial. Therefore, deciding whether a static program analysis can produce or cannot produce some bounded set of false alarms is in general impossible, unless satisfies the ACC. In this last case, we can at least answer “yes” if the static analysis has a bounded imprecision over a program with a specific input. The -partial completeness and incompleteness class of an abstraction are therefore a non-trivial property of programs for which no recursively enumerable procedure may exist which is able to enumerate all of their elements.

 [1] M. Campion , M. Dalla Preda , R. Giacobazzi , Partial (in)completeness in abstract interpretation: Limiting the imprecision in program analysis , Proc. ACM Program. Lang . 6 ( 2022 ). doi: 10 .1145/3498721. [2] P. Cousot , R. Cousot , Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , ACM Press, 1977 , pp. 238 - 252 . doi: 10 .1145/512950.512973. [3] P. Cousot , R. Cousot , Systematic design of program analysis frameworks, in: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , ACM Press, 1979 , pp. 269 - 282 . doi: 10 .1145/567752.567778. [4] P. Cousot , Principles of Abstract Interpretation, The MIT Press, Cambridge, Mass., 2021 . [5] G. Winskel, The formal semantics of programming languages: an introduction , MIT press, 1993 . [6] A. Miné , Tutorial on static inference of numeric invariants by abstract interpretation, Foundations and Trends in Programming Languages 4 ( 2017 ) 120 - 372 . URL: https://doi. org/10.1561/2500000034. doi: 10 .1561/2500000034. [7] R. Bruni , R. Giacobazzi , R. Gori , I. Garcia-Contreras , D. Pavlovic , Abstract extensionality: on the properties of incomplete abstract interpretations , PACMPL 4 ( 2020 ) 28 : 1 - 28 : 28 . doi: 10 .1145/3371096. [8] W. A. Wilson , On quasi-metric spaces , American Journal of Mathematics 53 ( 1931 ) 675 - 684 . doi: 10 .2307/2371174. [9] P. Cousot , R. Giacobazzi , F. Ranzato , Program analysis is harder than verification: A computability perspective , in: International Conference on Computer Aided Verification, Springer, 2018 , pp. 75 - 95 . doi: 10 .1007/978-3- 319 -96142- 2 _ 8 . [10] P. Cousot , R. Cousot , Inductive definitions, semantics and abstract interpretation , in: Conference Record of the 19th ACM Symp. on Principles of Programming Languages (POPL '92) , ACM Press, 1992 , pp. 83 - 94 . [11] P. Cousot , R. Cousot , Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form (Invited Paper) , in: P. Wolper (Ed.), Proc. of the 7th Internat. Conf. on Computer Aided Verification (CAV '95) , volume 939 of Lecture Notes in Computer Science, Springer-Verlag, 1995 , pp. 293 - 308 . [12] M. Campion , M. Dalla Preda , R. Giacobazzi , Abstract interpretation of indexed grammars , in: International Static Analysis Symposium , Springer, 2019 , pp. 121 - 139 . doi: 10 .1007/ 978-3- 030 -32304- 2 _ 7 . [13] R. Giacobazzi , F. Ranzato , F. Scozzari. , Making abstract interpretation complete , Journal of the ACM 47 ( 2000 ) 361 - 416 . doi: 10 .1145/333979.333989. [14] R. Bruni , R. Giacobazzi , R. Gori , F. Ranzato , A logic for locally complete abstract interpretations , in: Proc. 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021 ), IEEE Computer Society, 2021 , pp. 1 - 13 . doi: 10 .1109/LICS52264. 2021 . 9470608 , distinguished paper. [15] R. Giacobazzi , F. Logozzo , F. Ranzato , Analyzing program analyses , in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 , Mumbai, India, January 15 - 17 , 2015 , 2015 , pp. 261 - 273 . doi: 10 . 1145/2676726.2676987. [16] P. Cousot , R. Cousot , Static determination of dynamic properties of programs , in: Proceedings of the 2nd International Symposium on Programming , Dunod, Paris, 1976 , pp. 106 - 130 . doi: 10 .1145/390019.808314.