Unbounded Procedure Summaries from Bounded Environments

Modular approaches to verifying interprocedural programs involve learning summaries for individual procedures rather than verifying a monolithic program. Modern approaches based on use of Satisfiability Modulo Theory (SMT) solvers have made much progress in this direction. However, it is still challenging to handle mutual recursion and to derive adequate procedure summaries using scalable methods. We propose a novel modular verification algorithm that addresses these challenges by learning lemmas about the relationships among procedure summaries and by using bounded environments in SMT queries. We have implemented our algorithm in a tool called Clover and report on a detailed evaluation that shows that it outperforms existing automated tools on benchmark programs with mutual recursion while being competitive on standard benchmarks.

1. 1.

   Expressions such as \( x~\mathrm {mod}~2 = 0\) can be generated by existentially quantifying local variables and then performing quantifier elimination.

2. 2.

   We lift the ancestor relationship from nodes to their procedures.

3. 3.

   In the implementation, multiple checks can be done together.

4. 4.

   We expect that our platform is less performant than the StarExec platform.

5. 5.

   We did not compare against FreqHorn since it cannot handle nonlinear CHCs.

6. 6.

   Unlike Spacer it does not use PDR to derive invariants, and unlike Smash it is not limited to predicate abstractions.

This material is based upon work supported by the National Science Foundation Graduate Research Fellowship Program under Grant No. DGE-1656466. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. This work was supported in part by the National Science Foundation award FMitF 1837030.

Authors and Affiliations

1. Princeton University, Princeton, NJ, USA

   Lauren Pick & Aarti Gupta

2. Florida State University, Tallahassee, FL, USA

   Grigory Fedyukovich

Corresponding author

Correspondence to Lauren Pick .

Editors and Affiliations

1. University of Copenhagen, Copenhagen, Denmark

   Fritz Henglein

2. Tel Aviv University, Tel Aviv, Israel

   Sharon Shoham

3. Technion, Haifa, Israel

   Yakir Vizel

A Renaming and Unfolding

Here, a formula f ranging over variables v is denoted f(v). For example, a procedure body is encoded by some formula \( body_p(in_p, out_p, local_p) \) and a path within it is encoded by some formula \( \pi _p(in_p, out_p, local_p) \).

Definition 14 (Renaming)

Given a set of program paths \(\varPi ({v}, {y}, {x})\) that contain the statement \(\ell :{y} := p({x})\), the renaming of a formula \(\varPi _p({ in }, { out }, { locs })\) that represents a subset of all paths in procedure p is defined as follows:

where \( fresh ({v}, {x}, {y})\) is a vector of fresh variables not present already in v, x, or y.

Definition 15 (Unfolding)

Let \(\ell \) be a location at which procedure p is called. Given set of program paths \(\varPi \) that all go through location \(\ell \), an unfolding of p is a one-level inlining at location \(\ell \) of one of the control-flow paths \(\pi _p\) in the body of p:

B Full Set of Derivation Rules

C Heuristics

1.1 C.1 Prioritizing Choice of Node

The Verify procedure from Fig. 1 employs a heuristic to choose which node in the set A to call ProcessNode on next. The factors that contribute toward an node’s priority are as follows, with ties in one factor being broken by the next factor, where \( depth (n)\) denotes the depth of node n in D and \( previous (n)\) denotes the number of times that the node n has been chosen previously:

• A lower \(\alpha * depth (n) + \beta * previous (n)\) score gives higher priority, where \(\alpha \) and \(\beta \) are weights

• A lower call graph depth of \( proc (n)\) gives higher priority

• A later call location \( ctx (n). loc \) gives higher priority

We prioritize nodes n with lower \( depth (n)\) values because they are more likely to help propagate learned summaries up to the \( main \) procedure’s callees. This priority is moderated by the \( previous (n)\) score which should prevent the starvation of nodes with larger \( depth (n)\) values. Our current heuristic search is more BFS-like, but for some examples, a DFS-like search is better. We plan to improve our heuristics in future work.

1.2 C.2 Avoiding Redundant Queries

If we have previously considered a node n that we are now processing, we can avoid making the same queries that we have previously made. E.g., if none of the over-approximate summaries for any of the procedures in \( bctx (n). env \) nor any of over-approximate summaries for any of the procedures called by \( proc (n)\) have been updated since the last time n was processed, we do not need to redo the over-over check.

1.3 C.3 Learning Over-approximate Bodies

Although there are many existing methods to interpolate, in many cases they are useless (recall our motivating example where an interpolant is just \(\top \)). To improve our chances of learning a refinement for an over-approximate summary, whenever we apply one of the proof rules that involves over-approximating the procedure body (e.g., OO, UO, OOIL, UOIL), we ensure that we at least learn the result of over-approximating the procedure body as an over-approximate fact about that procedure. For example, if we consider doing this for OO, we would simply replace premise \(O' = O[p \mapsto O[p] \wedge \mathbb {I}]\) with \(O' = O[p \mapsto O[p] \wedge \mathbb {I} \wedge \exists locals _p . \widehat{ body }_O]\). Note that the result of applying quantifier elimination to \(\mathbb {I} \wedge \exists locals _p . \widehat{ body }_O\) is also an interpolant. Similarly, if we consider doing this for OOIL, we replace the goal \(D, O, U, L', P \vdash Res \) with \(D, O[p \mapsto \exists locals _p . \widehat{ body }_O], U, L', P \vdash Res \).

1.4 C.4 Preventing Summaries from Growing too Large

Although we want to increase our chances of learning useful refinements of over-approximations as we have just discussed, we still wish to prevent summaries from becoming too complicated. We can achieve this in a few ways.

Quantifier Elimination. One way that we can achieve this is to use quantifier elimination or an approximation thereof on each conjunct (resp. disjunct) that we add to an over- (resp. under-) approximate summary. For example, we can replace \(U' = U[p \mapsto U[p] \vee \exists locals _p. \pi ]\) with \(U' = U[p \mapsto U[p] \vee \mathrm {QE}(\exists locals _p. \pi )]\) in the UU rule. We illustrate how to do this using two examples:

• Instead of using premise \(O' = O[p \mapsto O[p] \wedge \mathbb {I} \wedge \exists locals _p . \widehat{ body }_O]\) for the OO rule as just discussed, we use the following premise: \(O' = O[p \mapsto O[p] \wedge \mathbb {I} \wedge \mathrm {QE}(\exists locals _p . \widehat{ body }_O)]\)

• We can also apply this to properties we learn by induction. Instead of using the premise \(L' = L \cup \{ \forall vars (A) . \bigwedge A \Rightarrow (p( in , out ) \Rightarrow indProp )\) for rule OOIL, use the following premise: \(L' = L \cup \{ \forall vars (A) . \bigwedge A \Rightarrow (p( in , out ) \Rightarrow QE(indProp) )\)

• Replace premise \(U' = U[p \mapsto U[p] \vee \exists locals _p. \pi ]\) with \(U' = U[p \mapsto U[p] \vee \mathrm {QE}(\exists locals _p. \pi )]\) in the UU rule.

This use of \(\mathrm {QE}\) leads to quantifier-free summaries.

When we update over- (resp. under-) approximate summaries, we can use over- (resp. under-) approximate \(\mathrm {QE}\). By comparison, under- (resp. over-) approximate \(\mathrm {QE}\) would lead to unsoundness. Approximating \(\mathrm {QE}\) is not only cheaper but can also further simplify the resulting summary.

Selective Updates. We can also prevent summaries from growing too quickly syntactically by only performing semantic updates. For example, consider O from the goal of the OO rule and \(O'\) from its subgoal. If \(O[p] \Rightarrow O'[p]\), then although \(O'[p]\) contains more conjuncts than O[p], it does not provide any new information. In this case, we avoid the update and simply use O in the subgoal instead of \(O'\). Similarly, if we consider U from the goal of UU and \(U'\) from its subgoal, then we only want to update the under-approximation if we have that \(U'[p] \not \Rightarrow U[p]\). Over-approximate summaries become monotonically more constrained, so if \(O[p] \Rightarrow O'[p]\), then \(O[p] \Leftrightarrow O'[p]\) must hold. Under-approximations become monotonically less constrained.

D Addition of Nodes in Derivation Tree

The AddNodes procedure is shown in Algorithm 3. For every path \(\pi \) through \( body_{proc(n)} \), it calls procedure

\(\textsc {TryAddNode}(n, \pi , p, \ell , Goal )\), which tries to apply AN to \( Goal \) with premises \(n \in A\) (AVAIL), path \(\pi \) in \( body \) (PATH), and procedure call to \(p = proc (n') \in P\) at location \(\ell \) in \(\pi \) (CALL). If TryAddNode succeeds in applying AN, then it updates \( Goal \) to be the subgoal of the application and returns \( true \). If it fails, then it performs no updates and returns \( false \). If TryAddNode fails, then there is already a node \(n''\) in D with the same bounded environment that the new node \(n'\) would have. In this case, AddNodes calls MakeAvailableIfNew, which applies MA if either of the following hold:

• \(n''\) has never been processed before

• \(n''\) has previously been processed with summaries \(O_ prev \) and \(U_ prev \) and the body \( body \) of \( proc(n) \) or the bounded environment \( benv \) for \(n''\) has a different over- or under-approximation than before, i.e., \(\widehat{ body }_{M_ prev } \ne \widehat{ body }_M\) or else \(\widehat{ benv }_{M_ prev } \ne \widehat{ benv }_M\) for \(M \in \{O, U\}\)

Similarly to TryAddNode, the procedure

\(\textsc {MakeAvailableIfNew}(n, \pi , p, \ell , Goal )\) applies MA with premises \(n \in D.N\) (NODE), path \(\pi \) in \( body \) (PATH), and procedure call to \( proc (n') \in P\) at location \(\ell \) in \(\pi \) (CALL). Both TryAddNode and MakeAvailableIfNew have the side-effect of updating \( Goal \) to be the subgoal of the applied rule (if any).

E Correctness and Progress Proof Sketches

Theorem 3 (Correctness)

Algorithm 1 returns \( safe \) (resp. \( unsafe \)) only if main’s semantics are such that it never violates the assertion (resp. a path in main violates the assertion).

Proof

The over-approximate summaries O in every proof subgoal are guaranteed to be such that for any procedure \(p \in P\), the semantics of p, given by interpreted predicate \(R_p( in , out )\), imply O[p] (see Definition 3), so approximation \(\widehat{m}_O\) contains at least all of the behaviors of the main procedure. The proof rule SAFE can only be applied when \(\widehat{m}_O \Rightarrow \bot \), i.e., when the over-approximate summary of main’s body does not violate the assertion along any path, indicating that the actual semantics of main also cannot violate the assertion. Similarly, the under-approximate summaries U in every proof subgoal are guaranteed to be such that for any \(p \in P\), U[p] imply \(R_p( in , out )\), so the approximation \(\widehat{m}_U\) only contains behaviors that are behaviors of the main procedure. The proof rule UNSAFE can only be applied when \(\widehat{m}_U \Rightarrow \top \), i.e., when the under-approximation of main violates the assertion along some path, which thus indicates that the actual semantics of main also includes assertion-violating behaviors.

Theorem 4 (Progress)

Processing a node in the derivation tree leads to at least one new (non-redundant) query.

Proof

Initially, no nodes in A have been processed, and after a node is processed, it is removed from the derivation tree. The only way that a node can be processed and not have a new query made about it is if an already-processed node is re-added A and this node does not have a new query that can be made about it. The AddNodes and MakeUnavailable procedures are the only ones that add nodes to A. The AddNodes procedure, by definition, will only add a node to A if there is a new query that can be made about it. MakeUnavailable only adds bounded parents of nodes whose summaries were updated. For any such bounded parent, at least one approximation of its procedure’s body must be different than it was the last time the bounded parent was processed, since one of its callee’s summaries was updated.

F Additional Experimental Results

Timing results for the Real-World benchmarks. Points below the diagonal line are those for which Clover outperforms the corresponding tool. Points on the right edge indicate timeouts of the corresponding tool.

Full size image

Timing results for the Mutual Recursion benchmarks. Points below the diagonal line are those for which Clover outperforms the corresponding tool. Points on the right edge indicate timeouts of the corresponding tool. Points on the top edge indicate a timeout for Clover.

Full size image

Figures 9 and  10 compare timing results for other tools against Clover for Real-World and Mutual Recursion benchmarks.

Reprints and permissions

© 2021 Springer Nature Switzerland AG

Policies and ethics