Non-Numerical Weakly Relational Domains

TL;DR

This paper develops a general framework for constructing non-numerical weakly relational domains, extending constant propagation with disjunctions and analyzing their computational complexity, including efficient algorithms for certain cases.

Contribution

It introduces a generic construction method for non-numerical weakly relational domains and provides algorithms for satisfiability and operations within these domains.

Findings

Extended constant propagation with disjunctions.

Polynomial algorithms for satisfiability in lattice-based domains.

NP-completeness results for general conjunction satisfiability.

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.