Norn: An SMT Solver for String Constraints

Abstract

We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.

This work was supported by the Czech Science Foundation project 202/13/37876P, the Ministry of Science and Technology of Taiwan (103- 2221-E-001 -019 -MY3 and 103-2221-E-001 -020 -MY3), Uppsala Programming for Multicore Architectures Research Center (UPMARC), and the Linkö** CENIIT Center (12.04).

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

We introduce version 1.0 of the Norn SMT solver. Norn targets an expressive constraint language that includes word equations, length constraints, and regular membership queries. Norn is based on the calculus introduced in [1]. This version adopts several improvements on the original version, which allow it to efficiently establish or refute the satisfiability of benchmarks that are out of the reach of existing state of the art solvers.

Norn aims to establish satisfiability of constraints written as Boolean combinations of: (i) word equations such as equalities $(a\cdot u = v\cdot b)$ or disequalities $(a\cdot u\ne v\cdot b)$, where a, b are letters and u, v are string variables denoting words of arbitrary lengths, (ii) length constraints such as $(|u|=|v|+1)$, where |u| refers to the length of the word denoted by string variable u, and (iii) predicates representing membership in regular expressions, e.g., $u\in c\cdot (a+b)^*$. The analysis is not trivial as it needs to capture subtle interactions between different types of predicates. The general decidability problem is still open. We guarantee termination of our procedure in case the considered initial constraints are acyclic. Acyclicity is a syntactic condition and it ensures that no variable appears more than once in word (dis)equalities during the analysis. This defines a fragment that is rich enough to capture all the practical examples we have encountered.

This version of the Norn solver follows a DPLL(T) architecture in order to turn the calculus introduced in [1] into an effective proof procedure, and introduces optimizations that are key to its current efficiency: an improved approach to handling disequalities, and a better strategy for splitting equalities compared to [1]. Norn accepts SMT-LIB scripts as input, both in the format proposed in [2] and in the CVC4 dialect [6], and can handle the combination of string constraints and linear integer arithmetic. In addition, Norn contains a fixed-point engine for processing recursive programs in the form of Horn constraints, which are expressed as SMT-LIB scripts with uninterpreted predicates; the algorithm for solving such Horn constraints was introduced in [1, 9].

Related work. Over the last years, several SMT solvers for strings and related logics have been introduced. A number of tools handled strings by means of a translation to bit-vectors [5, 10, 11], thus assuming a fixed upper bound on the length of the possible words. More recently, DPLL(T)-based string solvers lift the restriction to strings of bounded length; this generation of solvers includes Z3-str [14], CVC4 [6], and S3 [12], which are all compared to Norn in Sect. 4. Most of those solvers are more restrictive than Norn in their support for language constraints. In our experience, such restrictions are particularly problematic for software model checking, where regular membership constraints offer an elegant and powerful way of expressing and synthesising program invariants. Another related technique are automata-based solvers for analyzing string-manipulated programs [13]. According to  [4], automata-based solvers are faster than the SMT-based ones on checking single execution trace. On the other hand, Norns ability to derive loop invariants and to verify entire programs can allow it to conclude even in the presence of an infinite number of possible single executions. Automata-based solvers would need to provide widening operators to handle such cases.

2 Logic and Calculus

Our constraint language includes word equations, membership queries in regular languages and length and arithmetic inequalities. We assume a finite alphabet $\Sigma$ and write $\Sigma ^*$ to mean the set of finite words over $\Sigma$. We assume w.l.o.g. that each letter in our alphabet is represented by its unique Unicode character. We work with a set $U$ of string variables denoting words in $\Sigma ^*$ and write $\mathbb {Z}$ for the set of integer numbers.

Assume variables $u, v \in U$, integers $k \in \mathbb {Z}$, letters $c \in \Sigma$, and words $w \in \Sigma ^*$. We further write $|t|$ for length of word $t$. The syntax of the constraints is then given by:

A constraint is linear if no variable appears more than once in any of its (dis)equalities. We write $w_t$ to mean a word denoted by a term $t$. Semantics of the constraints are in [1].

Given a constraint $\upphi$ in our logic, we build a proof tree rooted at $\upphi$ by repeatedly applying inference rules. We assume here, without loss of generality, that $\upphi$ is given in Disjunctive Normal Form. An inference rule is of the form:

$\textsc {Name}$ is the name of the rule,  cond is a side condition on A for the application of the rule, $B_1~B_2~...~B_n$ are the premises, and A is the conclusion. Premises and conclusions are constraints. Each application consumes a conclusion and produces premises. In our calculus, if one of the produced premises turns out to be satisfiable, then $\upphi$ is also satisfiable. If none of the produced premises is satisfiable, then $\upphi$ is unsatisfiable. The inference rules are introduced in [1]. The repeated application of the rules starting from a constraint $\upphi$ is guaranteed to terminate (i.e., giving a decision procedure) in case $\upphi$ is acyclic. Intuitively, acyclicity is a syntactic condition on the occurences of variables. This condition ensures all (dis)equalities are linear, whether in $\upphi$ or after the application of some inference rule. We describe one rule. Other rules are introduced in [1].

Rule $\textsc {Eq-Var}$ eliminates variable u from the equality $u\cdot t_1=t_2\wedge \upphi$. The equality is satisfied if a word $w_u$ coincides with the prefix of a word $w_{t_2}$. We assume $u\cdot t_1=t_2\wedge \upphi$ is linear (see [1] for the general case). There are two sets of premises. The first set corresponds to all the cases where $w_u$ coincides with a word $w_{t_3}$ where $t_2$ is the concatenation $t_3\cdot t_4$. The second set represents all situations where $w_{t_3}$ is a prefix of $w_u$ which is a prefix of $w_{t_3\cdot v}$ with $t_2$ being written as the concatenation $t_3\cdot v\cdot t_4$.

3 A DPLL(T)-Style Proof Procedure for Strings

We follow the classical DPLL(T)-architecture [8] to turn the calculus from Sect. 2 into an effective proof procedure. For a given (quantifier-free) formula in our logic, first a Boolean skeleton is computed, abstracting every atom to a Boolean variable. A SAT-solver is then used to check satisfiability of the Boolean skeleton, producing (in the positive case) an implicant of the skeleton; the implicant is subsequently translated back to a conjunction of string literals, and checked for satisfiability in the string logic.

Our theory solver for checking conjunctions of string literals implements the rules of Sect. 2 and Sect. 3.1, and handles all necessary splitting internally, i.e., without involving the SAT-solver. In our experience (which is consistent with observations in other domains, e.g., [3]), this approach makes it easier to integrate splitting heuristics, and often shows better performance in practice. In particular, our approach to split equalities is model-based and exploits information extracted from arithmetic constraints in order to prune the search space; the method is explained in Sect. 3.2.

Starting from a conjunction $\upphi = (\upphi _= \wedge \upphi _{\not =} \wedge \upphi _\in \wedge \upphi _a)$ of literals (which is here split into equalities $\upphi _=$, disequalities $\upphi _{\not =}$, membership constraints $\upphi _\in$, and arithmetic constraints $\upphi _a$) the theory solver performs depth-first exploration until either a proof branch is found that cannot be closed (and constitutes a model), or all branches have been closed and discharged. In the latter case, information about the string literals involved in showing unsatisfiability is propagated back to the SAT-solver as a blocking clause.

Rules are applied to $\upphi = (\upphi _= \wedge \upphi _{\not =} \wedge \upphi _\in \wedge \upphi _a)$ in the following order: (i) Satisfiability of $\upphi _a$ (in Presburger arithmetic) is checked, (ii) Compound disequalities in $\upphi _{\not =}$ are eliminated (Sect. 3.1), (iii) Equalities in $\upphi _=$ with complex left-hand side are split (Sect. 3.2), (iv) Membership constraints in $\upphi _\in$ with complex term are split, and (v) Satisfiability of all remaining membership literals and arithmetic constraints is checked.

3.1 Efficient Handling of Disequalities

To handle disequalities, we proceed differently than the method presented in [1]. For each disequality of the form $t\ne t'$, the rule Diseq-Split produces only two premises. The first premise corresponds to the case where the words $w_{t}$ and $w_{t'}$ have different length. The second case is when $w_{t}$ and $w_{t'}$ have the same length but contain different letters $c \ne c'$ after a common prefix. Rather than constructing a premise for each pair of different letters (as it is done in [1]), we introduce two special variables $\mu$ and $\mu '$ (called witness variables) such that the letters c and $c'$ correspond to the words denoted by $\mu$ and $\mu '$. Therefore, the length of these witness variables is one and this fact is added to the arithmetic constraints. Furthermore, we add a disequality $\mu \ne \mu '$ in order to denote that c is different from $c'$. Assuming fresh variables u, v and $v'$, we rewrite $t\ne t'$ as two equalities $t=u\cdot \mu \cdot v$ and $t'=u \cdot \mu '\cdot v'$. Finally, w.l.o.g. we restrict the inference rules such that witness variables can only be substituted by other witness variables.

The new Rule Reg-Witness can only be applied to a witness variable $\mu$ in a certain case. For a formula $\upphi$, we define the condition $\Theta (\upphi ,\mu )$ to denote that $\mu$ appears in $\upphi$ only in disequalities. The Rule Reg-Witness replaces all membership predicates $\{\mu \in R_i\}_{i=1}^n$ with an arithmetic constraint $\mathsf{Unicode}(R_1,R_2,\ldots ,R_n,\mu )$. This constraint uses a fresh variable $\mu _{uni}$ s.t. the set of possible lengths of the word denoted by $\mu _{uni}$ represents the set of Unicode characters belonging to the intersection of all regular expressions $\{R_i\}_{i=1}^n$. In order to do so, we construct a finite state automaton A accepting the intersection of $\{R_i\}_{i=1}^n$. Furthermore, we restrict A to accept only words of size exactly one (since $\mu$ is a witness variable). The obtained automaton is then determined. Notice that the determined automaton B has only transitions from the initial state to the final one. Each transition of B is labelled by a Unicode character interval as specified by the automata library [7] we are using. Then, for each transition labeled by an interval of the form {min, ...,max}, we associate the arithmetic constraint $min\le |\mu _{uni}|\le max$. Finally, our arithmetic constraint $\mathsf{Unicode}(R_1,R_2,\ldots ,R_n,\mu )$ will be the disjunction of all associated arithmetic constraints to all the transitions of B. In the case that the intersection is empty, we set $\mathsf{Unicode}(R_1,R_2,\ldots ,R_n,\mu )$ to $\mathtt false$.

Finally, the Rule Diseq-Witness replaces a disequality of the form $\mu \ne \mu '$ by the arithmetic constraint $|\mu _{uni}| \ne |\mu '_{uni}|$.

3.2 Length-Guided Splitting of Equalities

The original calculus rule for handling complex equalities is Eq-Var, which systematically enumerates the different ways of matching up left-hand and right-hand side terms. For a practical proof procedure, naive use of this rule is sub-optimal in two respects: the number of cases to be considered grows quickly (in the worst case, exponentially in the number of equalities); and the rule does not provide any guidance on the order in which the cases should be considered, which can have dramatic impact on the performance for satisfiable problems. We found that both aspects can be improved by eagerly taking arithmetic constraints on the length of strings into account.

To present the approach, we assume that conjunctions $\upphi = (\upphi _= \wedge \upphi _{\not =} \wedge \upphi _\in \wedge \upphi _a)$ are continuously saturated by propagating length information from $\upphi _=$ to $\upphi _a$: for every equality $s = t$, a corresponding length equality $|s| = |t|$ is added, compound expressions $|s \cdot t|$ are rewritten to $|s| + |t|$, and the length |w| of concrete words $w \in \Sigma ^*$ is evaluated. In addition, for every variable v an inequality $|v| \ge 0$ is generated. Similar propagation is possible for membership constraints in $\upphi _\in$.

Prior to splitting equalities from $\upphi _=$, it is then possible to check the satisfiability of arithmetic constraints $\upphi _a$ (using any solver for Presburger arithmetic), and compute a satisfying assignment $\upbeta$. This assignment defines the length $val_{\upbeta }(|v|)$ of all string variables v, and thus uniquely determines how the right-hand side of an equality $u \cdot t_1 = t_2$ should be split into a prefix corresponding to u, and a suffix corresponding to $t_1$. We obtain the following modified splitting rule, which has the side condition that $u \cdot t_1 = t_2 \cdot v \cdot t_3$ is linear, and that a satisfying assignment $\upbeta$ of $\upphi _a$ exists such that $val_{\upbeta }(|t_2|) \le val_{\upbeta }(|u|) \le val_{\upbeta }(|t_2\cdot v|)$:

A similar rule is introduced to cover the situation that the right-hand side has to be split between two concrete letters, i.e., in case we have $val_{\upbeta }(|u|) = val_{\upbeta }(|t_2|)$ and $val_{\upbeta }(|t_1|) = val_{\upbeta }(|t_3|)$ for an equation $u \cdot t_1 = t_2 \cdot t_3$.

4 Implementation and Experiments

We compare the new version of Norn¹ to other solvers on two sets of benchmarks. First, we use the well-known set of Kaluza benchmarks, which were translated to SMT-LIB by the authors of CVC4 [6]. These benchmarks contain constraints generated by a Javascript analysis tool, and are mainly equational, with relatively little use of regular expressions. Results are given in Table 1, and show that currently Z3-str [14] performs best for this kind of benchmarks; however, Norn can solve 27 benchmarks that no other tool can handle (Table 2). S3 [12] produced internal errors on a larger number of the Kaluza benchmarks, and sometimes results that were contradictory with the other solvers: for 95 problems, S3 claimed unsat, whereas Z3-str and CVC4 reported sat. For 27 of those, also Norn gave the answer sat. No contradictions were observed between CVC4, Z3-str, and Norn. A direct comparison with Norn 0.3 [1] was not possible due to lacking support for SMT-LIB input. Instead, we internally modified Norn and reverted back to the old version of the calculus. The results indicate that our new rules significantly improve the performance specially on large benchmarks.

As a second set of benchmarks, we considered queries generated during CEGAR-based verification of string-processing programs [1]; those queries are quite small, but make heavy use of regular expressions and operators like the Kleene star. Norn could solve all of the benchmarks. We did not observe any major difference between the two versions of the calculus (runtimes are typically very small). Comparison with Z3-str was not possible, since the solver does not support regular expressions.² CVC4 and S3 showed timeouts, ran out of memory, or crashed on a large number of the benchmarks. S3 and Norn gave contradicting answers in altogether 413 cases, with manual inspection indicating that the answers by Norn were correct. This was confirmed by the S3 authors, and will be fixed in the near future; a corrected version was not available by the deadline.

Table 1. Experimental results. All experiments were done on an AMD Opteron 2220 SE machine, running 64-bit Linux and Java 1.8. Runtime was limited to 240 s (wall clock time), and heap space to 1.5 GB. CEGAR were benchmarks downsized from UTF16 when necessary.

Table 2. Complementarity of the results: number of problems for which one tool can show sat/unsat, whereas another tool times out or crashes. For instance, Norn can prove satisfiability of 435 Kaluza benchmarks on which CVC4 times out.