Recursive Games for Compositional Program Synthesis

Abstract

Compositionality, i.e., the use of procedure summarization instead of code inlining, is key to scaling automated verification to large code bases. In this paper, we present a way to exploit compositionality in the context of program synthesis.

The goal in our synthesis problem is to instantiate missing expressions in a procedural program so that the resulting program satisfies a safety or termination requirement in spite of an adversarial environment. The problem is modeled as a game between two players — the program and the environment — that take turns changing the program’s state and stack. The objective of the program is to ensure that all executions of this recursive game satisfy the requirement. Synthesis involves the modular computation of a strategy under which the program meets this objective. Our solution is based on the notion of game summaries, which generalize traditional procedure summaries, and relate program states in a procedural context with sets of states at which the game can return from that context. Our method for compositional reasoning about game summaries is embodied in a set of deductive proof rules. We prove these rules sound and relatively complete. We also show that a sound approximation of these rules can be automated using a Horn constraint solver that utilizes SMT-solving, counterexample-guided abstraction refinement, and interpolation. An experimental evaluation over a set of systems code benchmarks demonstrates the practical promise of the approach.

A Correctness Proofs for RuleTerm

Proof

We split the proof into two parts: soundness and relative completeness.

Soundness. We prove the soundness by contradiction.

Assume that there exist an assertions ${sum}(v_1,v_2, R)$, $round (v_1,v_2)$ and $descent (v_1,v_2)$ that satisfy the premises of the rule, yet the conclusion of the rule does not hold. That is, there is no winning strategy for Prog.

Hence, there exists a strategy $\sigma$ for Env in which each play does not terminates. This strategy $\sigma$ alternates between existential choices of Env and universal choices of Prog. Let $aux (v)$ be a set of states for which $\sigma$ provides existentially chosen successors wrt. Prog. Note that no play terminates from any $s\in aux (v)$ since no play determined by $\sigma$ terminates.

We derive a contradiction by relying on a certain play $\pi$ that is determined by $\sigma$. The play $\pi$ is constructed iteratively. We start from some root state $s_0$ of $\sigma$, which satisfies the initial condition $init (v)$. Note that ${sum}(s_0,s_0,R_0)$, due to T1, and $aux (s_0)$ due to $\sigma$.

Each iteration round extends the matched play $s_0..s$ obtained so far in three ways:

• by two states, say $s_1$ and $s_2$ where $env (s, s_1)$ and $prog (s_1, s_2)$,

• by a state, say $s_1$ where $call (s, s_1)$, or

• by a sequence of states $s_1..s_2$ where we have $call (s, s_1)$, ${sum}(s_1,R_1)$, and $s_1..s_2$ is a play from $s_1$ to one of its FURs $s_2 \in R_1$.

We maintain a condition that for the last state $s$ of each such play, ${sum}(s_0,s,R)$ and $aux (s)$ where $s_0= entry (s)$, i.e., $s_0$ is the entry state of the calling context of s.

Let $s$ be the last state of the play $\pi$ constructed so far, and $s_0= entry (s)$. Due to our condition, we have ${sum}(s_0,s,R)$ and $aux (s)$. We iteratively construct a play $\pi$ taking one of the following steps at a time:

• $\sigma$ determines a successor state $s_1$ such that $env (s, s_1)$, and T2 guarantees that there exists a state $s_2$ such that $prog (s_1, s_2)$, $round (s, s_2)$, and ${sum}(s_0,s_2,R_2)$ such that $R_2 \subseteq R$. The play is extended by $s_1,s_2$. Furthermore, $aux (s_2)$ due to G.

• $\sigma$ determines a successor state $s_1$ such that $call (s, s_1)$, and T3 guarantees that there exists a set of FURs $R_1$ of $s_1$ such that ${sum}(s_1,s_1,R_1)$, and also $descent (s_0,s_1)$. The play is extended by $s_1$. Furthermore, $aux (s_1)$ due to $\sigma$.

• $\sigma$ determines a sequence of successor state $s_1$ such that $call (s, s_1)$, where ${sum}(s_1,s_1,R_1)$ is given together with some $s_2 \in R_1$. Here, T4 guarantees that there exists a set of FURs $R_2$ for $s_2$ such that ${sum}(s_0,s_2,R_2)$ where $R_2 \subseteq R$, and also $round (s, s_2)$. The play is extended by $s_1..s_2$. Furthermore, $aux (s_2)$ due to $\sigma$.

By iteratively constructing $\pi$ following the above steps, we obtain a play that satisfies the strategy $\sigma$. Hence, one of the following follows:

• there exists an infinite sequence of Env states at some procedural level if the infinite play is due to infinite intra-procedural steps by Env which contradicts with T6.

• there exists an infinite sequence of entry states if the infinite play is due to infinite call steps by Env which contradicts with T7

Relative Completeness. Let us assume that Prog has a winning strategy, say $\sigma$. We show how to construct ${sum}(v_1,v_2,R)$, $round (v_1,v_2)$ and $descent (v_1,v_2)$ satisfying the premises of the rule by taking an arbitrary play $\pi$ determined by $\sigma$.

Let ${sum}(v_1,v_2,R)$ be the set of all triplets $(s_0,s,R)$ such that $s$ is a state in$\pi$ for which $\sigma$ provides a universally chosen successor w.r.t. Env, $s_0$ = $entry (s)$, and $R$ is the set of FURs in $\sigma$ starting at $s$. Let $round (v_1,v_2)$ be the set of all pairs of states $(s_1, s_2)$ such that $s_1$ and $s_2$ are consecutive Env states on the same procedural level. Let $descent (v_1,v_2)$ be the set of all pairs of states $(s_1, s_2)$ such that $s_1$ and $s_2$ are entry states of two consecutive procedural levels.

Since an initial state is an Env state, ${sum}(v_1,v_2,R)$ is defined for any initial state, satisfying T1.

Let us take an arbitrary summary ${sum}(s_0,s_1,R_1)$. $\sigma$ guarantees that for every successor $s_2$ of $s_1$ wrt. Env there exists a successor $s_3$ wrt. Prog. For every such $s_3$, ${sum}(s_0,s_3,R_3)$. Since the set of FURs may only shrink across intra-procedural steps, $R_3 \subseteq R_1$. In addition, we have $round (s_1,s_3)$ since $s_1$ and $s_3$ are consecutive Env states on the same procedural level, i.e. ${sum}(v_1,v_2,R)$ and $round (v_1,v_2)$ satisfy T2.

For an arbitrary Env state $s_1$ with ${sum}(s_0,s_1,R_1)$ and a state $s_2$ such that $call (s_1,s_2)$, we get ${sum}(s_2,s_2,R_2)$ since $s_2$ is an Env state. Since $s_0$ and $s_2$ are entry states to the caller and callee context respectively, we have $descent (s_0,s_2)$,i.e. T3 is satisfied.

Let us consider a pair of states $s_1$ and $s_2$ such that ${sum}(s_0,s_1,R_1)$, ${sum}(s_2,s_2,R_2)$, and $call (s_1,s_2)$. For any $s_3 \in R_2$, we have ${sum}(s_0,s_3,R_3)$ since $s_3$ is an Env state by definition of FURs, and $s_0$ is in the same procedural level with all states in $R_1$ including $s_2$. It follows that any FUR of $s_2$ is also FUR of $s_0$ implying $R_2 \subseteq R_0$. In addition, we have $round (s_1,s_3)$ since $s_1$ and $s_3$ are consecutive Env states on the same procedural level, i.e. T4 is satisfied.

Now let us consider a state $s_1$ such that ${sum}(s_0,s_1,R_1)$ for $s_0 = entry (s_1)$ and $ret (s_1,s_2)$ for some state $s_2$. By definition of FURs, we see that $s_2$ is in $R_1$, satisfying T5.

Now we show by contradiction that $round (v_1,v_2)$ is well-founded. Assume otherwise, i.e., there exists an infinite sequence of states s1, s2, . . . induced by $round (v_1,v_2)$ and Prog still terminates. As noted previously, for each pair of consecutive Env states $s_i$ and $s_{i+1}$ there exists an intermediate sequence of state $s_i'...s_i''$ such that the sequence $s_1, s_1',..,s_1'', s_2, . . . , s_i, s_i',..,s_i'', s_{i+1}, . . .$ is a play. Since this play does not terminate, we obtain a contradiction to the assumption. Hence, we conclude that $round (v_1,v_2)$ is well-founded, satisfying T6.

Similarly, we show by contradiction that descent(u, v) is well-founded, satisfying T7.    $\square$