Non-Numerical Weakly Relational Domains

TL;DR

The paper tackles scalable static analysis of relational properties beyond numeric domains by introducing a general framework to convert any relational domain into a weakly relational one, enabling efficient analysis while controlling precision. It presents two main pathways: (i) a $2$-decomposable construction (with $2$-clusters) and a constraint-based method to create polynomial-time abstract operators, including a $2$-decomposable domain for disjunctive constants; (ii) directed domains formed by conjunctions of inequalities over arbitrary partial orders, with lattice cases admitting $1$-normal forms for tractable satisfiability and implication, plus $0$-normal forms and approximate normalizations for general orders. The work also extends these domains with disjunctions, provides abstract transformers for assignments and guards, and outlines the applicability to string- and order-based analyses, offering a flexible toolkit for building weakly relational domains that balance precision and efficiency. The results yield practical, scalable abstractions for programs manipulating complex data relations such as strings and pointer-like structures, while delineating NP-completeness boundaries in certain disjunctive settings. Overall, it establishes a unifying, extensible approach to crafting tractable weakly relational abstractions from richer relational domains.

Abstract

The weakly relational domain of Octagons offers a decent compromise between precision and efficiency for numerical properties. Here, we are concerned with the construction of non-numerical relational domains. We provide a general construction of weakly relational domains, which we exemplify with an extension of constant propagation by disjunctions. Since for the resulting domain of 2-disjunctive formulas, satisfiability is NP-complete, we provide a general construction for a further, more abstract weakly relational domain where the abstract operations of restriction and least upper bound can be efficiently implemented. In the second step, we consider a relational domain that tracks conjunctions of inequalities between variables, and between variables and constants for arbitrary partial orders of values. Examples are sub(multi)sets, as well as prefix, substring or scattered substring orderings on strings. When the partial order is a lattice, we provide precise polynomial algorithms for satisfiability, restriction, and the best abstraction of disjunction. Complementary to the constructions for lattices, we find that, in general, satisfiability of conjunctions is NP-complete. We therefore again provide polynomial abstract versions of restriction, conjunction, and join. By using our generic constructions, these domains are extended to weakly relational domains that additionally track disjunctions. For all our domains, we indicate how abstract transformers for assignments and guards can be constructed.