Keywords

1 Introduction

Automatic synthesis of program has long been considered as one of the most central problems in computer science. It is the task of automatically finding programs from the underlying language that satisfy user intent expressed in some form of (formal) constraints [15]. Usually, we need to perform certain kind of search over the state space of all potential programs in order to generate one that meets the constraints.

Fruitful studies have achieved a lot of progress for program synthesis in many communities. Beginning in 1957, Alonzo Church defines the problem to synthesize a circuit from mathematical requirements. Reactive synthesis is a special case of program synthesis that aims to produce a controller that reacts to environment’s inputs satisfying a given temporal logic specification [5]. An international competition called the Reactive Synthesis Competition is held annually since 2014.Footnote 1 Camacho et al. establish the correspondence of planning problems with temporally extended goals to reactive synthesis problems [8]. Building on this correspondence, synthesis can be realized more efficiently via planning. A pattern-based code synthesis approach is presented to assemble an application from existing components [12]. The code patterns are expressed by planning domain models. Recently, the application of AI techniques especially deep learning methods in program synthesis becomes an active research topic. DeepCoder, developed by Microsoft, is to train a neural network to predict properties of program that generated the outputs from the inputs [1]. Empirically, DeepCoder is able to help generate small programs only containing several lines. Gu et al. propose a deep learning based approach to generate API usage sequences for a given natural language query [14]. The work in [2] transforms a graphical user interface screenshot created by a designer into computer code by deep learning methods. Various codes for three different platforms can be generated with the accuracy over 77%. In addition, other techniques from different perspectives such as inductive programming [16] and genetic programming [20] are also applied in program synthesis. However, synthesizing a program is still a challenging problem due to the large search space.

AI planning, or planning for short, has been successfully applied in many fields. Planning is the problem of finding a sequence of actions that leads from an initial state to a goal state [13]. Classical planning is the problem such that each action has deterministic outcome. If the outcomes of some actions are uncertain, the problem is referred to as a non-deterministic planning problem. The non-deterministic actions give rise to the exponential growth in the search space and hence make the problem more difficult even in the simplest situation where the states of the world are full observable. A plan to a non-deterministic planning problem may have loops or branches which are similar to basic programming language constructs. Inspired by this, we obtain the idea to bridge the gap between program synthesis and non-deterministic planning.

Programs that manipulate heaps are called pointer programs. Pointer operations allow dynamic heap allocation and deallocation, pointer reference and dereference etc. These characteristics make pointer programs more error prone. Separation logic is an extension of Hoare logic addressing the task of reasoning about pointer programs [19]. Its key power lies in the separating conjunction \(\varSigma _{1} * \varSigma _{2}\), which asserts that \(\varSigma _{1}\) and \(\varSigma _{2}\) hold for separate portions of heaps, leading the reasoning in a modular way. Starting from the pioneer work [4], which presents a symbolic execution of a fragment of separation logic formulas called symbolic heaps, many researchers exploit symbolic execution techniques to build formal proofs of pointer programs [7, 10, 17]. The most famous tool, Infer [6], is a static analyzer developed at Facebook rooting on symbolic execution.

This paper focusses on the pointer program synthesis. We propose a compilation based approach to simulate the symbolic execution process of pointer programs by non-deterministic planning. The compilation result is specified in the Planning Domain Definition Language (PDDL) [11] that is a standard input to the state-of-the-art planners. The major contribution of our work is the encoding approach from symbolic execution rules to non-deterministic planning models. To the best of our knowledge, it is unique in using non-deterministic planners as program synthesizers.

The rest of the paper is organized as follows. Section 2 and Sect. 3 review the notations of non-deterministic planning and symbolic heaps; Sect. 4 shows symbolic execution theory of pointer programs with symbolic heaps; Sect. 5 describes how to compile symbolic execution rules into non-deterministic planning problems; Sect. 6 gives the experimental results; the last section concludes our work.

2 FOND Planning

We assume environments are fully observable. Following [13], a Fully Observable Non-Deterministic (FOND) planning problem \(\mathcal {P}\) is a tuple \((\mathcal {F}, \mathcal {I}, \mathcal {G}, \mathcal {A})\), where \(\mathcal {F}\) is a set of fluents, \(\mathcal {I} \subseteq F\) characterizes what holds initially, \(\mathcal {G} \subseteq \mathcal {F}\) characterizes the goal, and \(\mathcal {A}\) is the set of actions. The set of literals of \(\mathcal {F}\) is \(Lits(\mathcal {F}) = \mathcal {F} \cup \{\lnot f \mid f \in \mathcal {F}\}\). Each action \(a \in \mathcal {A}\) is associated with a pair \((pre(a), \textit{eff}(a))\), where \(pre(a) \subseteq Lits(\mathcal {F})\) is the precondition and \(\textit{eff}(a)\) is a set of outcomes of a. An outcome \(o \in \textit{eff}(a)\) is a set of conditional effects (with, possibly, an empty condition), each of the form \(C \vartriangleright l\), where \(C \subseteq Lits(\mathcal {F})\) and \(l \in Lits(\mathcal {F})\). Briefly speaking, \(C \vartriangleright l\) expresses the meaning that after applying a in the current state, l becomes true in the next state if current state satisfies C. A planning state s is a subset of \(\mathcal {F}\) that are true.Footnote 2 Given \(s \subseteq \mathcal {F}\) and \(f \in \mathcal {F}\), we say that s satisfies f, denoted \(s \models f\) iff \(f \in s\). In addition, \(s \models \lnot f\) iff \(f \not \in s\), and \(s \models L\) for a set of literals L, if \(s \models l\) for every \(l \in L\). An action a is applicable in state s if \(s \models pre(a)\). We say \(s'\) is a result of applying a in s iff for one outcome o in \(\textit{eff}(a)\), \(s' = s \backslash \{f \mid (C \vartriangleright \lnot f) \in o, s \models C \} \cup \{f \mid (C \vartriangleright f) \in o, s \models C \}\).

Solutions to a FOND planning problem are referred to as policies. A policy p is a partial mapping from states to actions. We say a is applicable in s if \(p(s) = a\). An execution \(\sigma \) of a policy p in state s is a finite sequence \(\langle (s_{0},a_{0}),\ldots ,(s_{n-1},a_{n-1}),s_{n} \rangle \) or an infinite sequence \(\langle (s_{0},a_{0}),(s_{1},a_{1}),\ldots \rangle \), where \(s_{0} = s\), and all of its state-action-state substrings \(s,a,s'\) satisfy \(p(s)=a\) and \(s'\) is a result of applying a in s. Finite executions ending in a state s if p(s) is undefined. A state trace \(\pi \) can be yielded from an execution \(\sigma \) by removing all the action symbols from \(\sigma \).

An infinite execution \(\sigma \) is fair iff whenever s, a occurs infinitely often within \(\sigma \), then for every \(s'\) that is a result of applying a in s, \(s,a,s'\) occurs infinitely often. A solution to \(\mathcal {P}\) is strong cyclic iff each of its executions in \(\mathcal {I}\) is either finite and ends in a state that satisfies \(\mathcal {G}\) or is infinite and unfair [9]. Intuitively speaking, the execution fairness of a strong cyclic solution guarantees that a goal state can eventually be reached from every reachable state with no effect that is always ignored. There are also strong solutions and weak solutions to a FOND planning problem, but we will not need those definitions in this paper.

3 Symbolic Heaps

We assume a set of programs variables Var (ranged over by \(x,y,\ldots \)), and a set of primed variables \(Var'\) (ranged over by \(x',y',\ldots \)). All variables are restricted as pointer type. The primed variables can only be used within logical formulas. The concrete heap models contain a set of locations Loc and a special notation nil which indicates a null pointer value. Let \(Val = Loc \cup \{nil\}\). We then define stack \(\mathcal {S}\) and heap \(\mathcal {H}\) as:

$$\begin{aligned} \mathcal {S} : (Var \cup Var') \rightarrow Val \qquad \qquad \mathcal {H} : Loc \rightharpoonup Val \end{aligned}$$

A heap maps a location to a location or nil representing a heap cell. The syntax of symbolic heap is defined below [4] which is a strict subset of separation logic [19].

$$\begin{aligned} e&\,{:}{:}{=} \,x \mid x' \mid nil \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text {expression} \\ \varPi&\,{:}{:}{=} \,e_{1} = e_{2} \mid e_{1} \ne e_{2} \mid true \mid \varPi _{1} \wedge \varPi _{2} \qquad \qquad \;\;\;\text {pure formula}\\ \varSigma&\,{:}{:}{=}\, emp \mid e_{1} \mapsto e_{2} \mid ls(e_{1},e_{2}) \mid true \mid \varSigma _{1} * \varSigma _{2} \;\;\;\;\,\text {spatial formula}\\ P&\,{:}{:}{=} \,\varPi \wr \varSigma \mid \exists x' : P \,\qquad \qquad \qquad \qquad \qquad \qquad \qquad \text {symbolic heap} \end{aligned}$$

Note that the assertions are restricted without negations and universal quantifiers. A symbolic heap \(\varPi \wr \varSigma \) can be divided into pure part \(\varPi \) (heap independent) and spatial part \(\varSigma \) (heap dependent), where \(\varPi \) is essentially an \(\wedge \)-separated sequence of pure formulas, and \(\varSigma \) a \(*\)-separated sequence of spatial formulas. The pure part is straightforward to understand, and the spatial part characterize spatial features of heaps. \(e_{1} \mapsto e_{2}\) is read as \(e_{1}\) points-to \(e_{2}\). It can hold only in a singleton heap, where \(e_{1}\) is the only active cell holding the value \(e_{2}\). \(ls(e_{1},e_{2})\) denotes a linked list segment with head pointer \(e_{1}\) and \(e_{2}\) holding in the tail cell. A complete linked list is one that satisfies ls(e, nil).

The semantics of symbolic heaps is given by a relation \(\mathcal {S},\mathcal {H} \models _{\tiny \text{ SH }} P\). \(\mathcal {H}=\mathcal {H}_{1} \bullet \mathcal {H}_{2}\) indicates that the domains of \(\mathcal {H}_{1}\) and \(\mathcal {H}_{2}\) are disjoint, and \(\mathcal {H}\) is their union.

For simplicity, symbolic heap we define only allows to reason about linked lists. The field can be regarded as the next pointer. For other linked shapes such as binary trees, we can extend the points-to assertion as \(e_{1} \mapsto e_{2}, e_{3}\). The semantics of list segment is given informally, saying that it holds of given heap containing at least one heap cell. Therefore it is equivalent to the least predicate satisfying:

$$\begin{aligned} ls(e_{1},e_{2}) \Leftrightarrow e_{1} \mapsto e_{2} \vee \exists x' : e_{1} \ne e_{2} \wedge e_{1} \mapsto x' * ls(x',e_{2}) \end{aligned}$$

4 Symbolic Execution

In this section we give symbolic execution rules for a pointer programming language. The grammar of commands is given by:

$$\begin{aligned} b&\,{:}{:}{=}\, e_{1}=e_{2} \mid e_{1} \ne e_{2} \;\;\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text {Boolean terms} \\ c&\,{:}{:}{=}\, x := e \mid x := [e] \mid [e] := e' \mid new(x) \mid dispose(e) \,\qquad \text {Primitive commands} \\ \mathcal {C}&\,{:}{:}{=}\, c \mid \mathcal {C}_{1};\mathcal {C}_{2} \mid while \; (b) \; do \; \{\mathcal {C}\} \mid if \; (b) \; then \; \{\mathcal {C}_{1}\} \; else \; \{\mathcal {C}_{2}\} \;\;\quad \qquad \text {Commands} \end{aligned}$$

The heap dereferencing operator \([\cdot ]\) is similar to symbolic heaps, that refers to the “next” field. \(x := e\) is the assignment, \(x := [e]\) and \([e] := e'\) are called lookup and mutation respectively, new(x) and dispose(e) are heap allocation and deallocation commands.

Shown in Table 1, the symbolic execution semantics \(P, \mathcal {C} \Longrightarrow P'\) takes a symbolic heap P and a primitive command \(\mathcal {C}\) as input, and transforms it into a new symbolic heap \(P'\) as an output. The primed variables \(x', y'\) are fresh primed variables in these rules.

Table 1. Symbolic execution rules
Full size table

We use notation A(e) for primitive commands that access heap cell e:

$$\begin{aligned} A(e) \,{:}{:}{=}\, [e] := e' \mid x := [e] \mid dispose(e) \end{aligned}$$

When executing A(e), we expect its precondition to be in a particular form \(\varPi \wr \varSigma * e \mapsto e'\). That is, the value holds in e should be explicitly exposed in order to fire the rule. Therefore, we have to equivalently rearrange the precondition whenever current symbolic heap do not match the rule.

Rearrangement rules are listed below. The Switch rule simply makes use of equalities to recognize that a dereferencing step is possible. The other two rules correspond to unrolling a list segment. To do so, we need to unroll the list to be a single heap cell (Unroll List2) or more cells (Unroll List1).

$$\begin{aligned}&{{} \mathbf{Rearrangement}\,\,Rules } \\&\text {Switch} \quad \frac{\varPi _{1} \wr \varSigma _{1} * e_{1} \mapsto e_{3}, A(e_{1}) \Longrightarrow \varPi _{2} \wr \varSigma _{2}}{\varPi _{1} \wr \varSigma _{1} * e_{2} \mapsto e_{3}, A(e_{1}) \Longrightarrow \varPi _{2} \wr \varSigma _{2}} \quad \varPi _{1} \vdash e_{1}=e_{2} \\&\text {Unroll List1} \quad \frac{\exists x': e_{1} \ne e_{2} \wedge \varPi _{1} \wr \varSigma _{1} * e_{1} \mapsto x' * ls(x', e_{2}), A(e_{1}) \Longrightarrow \varPi _{2} \wr \varSigma _{2}}{\varPi _{1} \wr \varSigma _{1} * ls(e_{1}, e_{2}), A(e_{1}) \Longrightarrow \varPi _{2} \wr \varSigma _{2}} \\&\text {Unroll List2} \quad \frac{\varPi _{1} \wedge e_{1} \mapsto e_{2} \wr \varSigma _{1}, A(e_{1}) \Longrightarrow \varPi _{2} \wr \varSigma _{2}}{\varPi _{1} \wr \varSigma _{1} * ls(e_{1}, e_{2}), A(e_{1}) \Longrightarrow \varPi _{2} \wr \varSigma _{2}} \end{aligned}$$

Generally, the number of symbolic heaps is infinite since primed variables can be introduced during symbolic execution. For example, in a loop that includes allocation (e.g., \(while \; (true) \; do \; \{ \ldots ;new(x);\ldots \}\)). An arbitrary length of symbolic heap can be generated, i.e., \(x \mapsto x' * x' \mapsto x'' \cdots \). In order to achieve fixed-point convergence, abstraction rules \(\varPi _{1} \wr \varSigma _{1} \rightsquigarrow \varPi _{2} \wr \varSigma _{2}\) are introduced.

The main effort of abstraction rules is to reduce primed variables. The abstraction rules are reported below. On one hand, we can remove primed variables from the pure parts of formulas (Abs1). On the other hand, we can gobble up primed variables by merging lists, swallowing single cells into lists, and abstracting two cells by a list (Abs2 and Abs3). We use the notation \(H(e_{1},e_{2})\) to stand for a formula in either of the form \(e_{1} \mapsto e_{2}\) or \(ls(e_{1},e_{2})\).

$$\begin{aligned}&\mathbf{Abstraction\,\,Rules } \\&\text {Abs1} \, e = x' \wedge \varPi \wr \varSigma \rightsquigarrow (\varPi \wr \varSigma )(e/x') \text { or } x' = e \wedge \varPi \wr \varSigma \rightsquigarrow (\varPi \wr \varSigma )(e/x') \\&\text {Abs2} \, \frac{\varPi \vdash e_{2} = nil \qquad x' \text { not in } \{\varPi , \varSigma , e_{1}, e_{2}\}}{\varPi \wr \varSigma * H_{1}(e_{1},x') * H_{2}(x',e_{2}) \rightsquigarrow \varPi \wr \varSigma * H(e_{1},nil)} \\&\text {Abs3} \, \frac{\varPi \vdash e_{2} = e_{3} \qquad x' \text { not in } \{\varPi , \varSigma , e_{1}, e_{2}, e_{3}, e_{4}\}}{\varPi \wr \varSigma * H_{1}(e_{1},x') * H_{2}(x',e_{2}) * H_{3}(e_{3},e_{4}) \rightsquigarrow \varPi \wr \varSigma * ls(e_{1},e_{2}) * H_{3}(e_{3},e_{4})} \end{aligned}$$

The \(*\)-conjunct \(H_{3}(e_{3}, e_{4})\) cannot be left out by considerations of soundness as Berdine and Calcagno pointed out [3, 4]. If we want to abstract \(H_{1}(-,-)\) and \(H_{2}(-,-)\) into one, the end of the second should not point back into the first.

Fig. 1.
figure 1

The encoding approach

Full size image

5 Compiling Symbolic Execution into FOND Planning

In this section we compile a pointer program synthesis problem into a FOND planning problem. The former is formalized as follows.

Definition 1 (Pointer Program Synthesis)

Given symbolic heaps \(P_{in}\) and \(P_{out}\) as input and output respectively, the task of pointer program synthesis is to generate a pointer program \(\mathcal {C}\) that satisfies \(P_{in}\) and \(P_{out}\).

Figure 1 illustrates the key idea of our approach. There are three modes after compilation, i.e., Command mode, Check mode and Abstraction mode. The order of their executions is reflected by black arrows. The Command mode contains a set of planning actions encoded from primitive command. We do not encode the rearrangement rules into a separate phase. Instead, the rearrangement step is embedded in the encoding of A(e). The actions in the Check mode are used to check the existence of an abstraction action that can fire. The abstraction rules are compiled into a set of abstraction actions.

Suppose the resulting FOND planning problem is \(\mathcal {P} = (\mathcal {F}, \mathcal {I}, \mathcal {G}, \mathcal {A})\), where each component is described as follows. The initial state \(\mathcal {I}\) and goal \(\mathcal {G}\) are determined by \(P_{in}\) and \(P_{out}\) of specific synthesis problems.

Fluents: The set of fluents \(\mathcal {F}\) is listed in Table 2, where \(int_{0}\) represents the null value. Moreover, we use the fluents command(), check(), choose(), abstraction() to represent different phases, and \(abs_{1}(),abs_{2}(),abs_{3}()\) to denote which abstraction rule can be activated.

Table 2. Fluents of the encoded problem
Full size table

Command Mode: Command mode is the first phase that a primitive command action is performed along with a possible rearrangement. Different from symbolic execution, here we do not distinguish rearrangement and command execution, only do rearrangement when it is needed. The encoded actions are shown in Table 3. For instance, there are two dispose actions corresponding to the dispose command, i.e., \(dispose_{1}\) and \(dispose_{2}\). The precondition of the former includes an explicit heap cell \(pt(x_{2},x_{3})\), and that of the latter includes a list \(ls(x_{2},x_{3})\) which needs to be unrolled as non-deterministic effects. The keyword “oneof” is used to express the non-deterministic effects in a planning model.

Table 3. Compilation of primitive commands
Full size table

Check Mode: The definition actions in Check mode are shown in Table 4. Action \(check\text {-}act\) alters the truth value of flags \(abs_{i}(), i = 1,2,3\) according to the current state whenever a corresponding abstraction rule is enabled. Then the \(choose\text {-}act\) will be executed to determine the next phase to be switched with respect to \(abs_{i}()\). When no abstraction rules can be applied, the next phase is the command mode, otherwise it is still turned to the abstraction mode.

Table 4. Actions in Check mode
Full size table

Abstraction Mode: Table 5 shows the set of abstraction actions encoded from abstraction rules. The first two actions correspond to the abstraction rules. The last rule is used to free a logical variable in use, and make it available. When after applying an abstraction rule, we will go back to the Check mode until no abstraction rules can fire.

Table 5. Compilation of abstraction rules
Full size table

6 Case Study and Experiment

In this section, we conduct a series of experiments to evaluate our approach. Further, we illustrate an example on synthesis of a disposal program which aims to dispose a linked list. The following code is the disposal program.

figure a

The initial state of this program is ls(x, nil). Using the symbolic execution rules, the symbolic execution process is shown in Fig. 2. Note that the loop arrow from bottom to up means that ls(x, nil) is the invariant of the program. At the beginning, we know x does not equal to nil since ls(x, nil) at least contains one cell. Hence the first assignment command in the loop body is executed. When executing the second command, we do not know what holds in address x according to the spatial part ls(x, nil) of the symbolic heap. Therefore a rearrangement step should be applied to distinguish the symbolic heap into a couple of situations. After executing \(x :=[x]\), we need to try to abstract the obtained symbolic heap since some primed variables are introduced. Then the last deallocation command is executed. In one situation, the loop exits. In the other, we find an invariant that is the same to the initial state. At this time the process terminates.

Fig. 2.
figure 2

Symbolic execution process for disposal program

Full size image

In practice, we encode the program into standard PDDL which can be accepted by existing planners. The details are omitted here. We evaluate our approach on several list manipulated program. The non-deterministic planner PRP [18] is used as the FOND planner. Experiments are conducted on a laptop running Ubuntu 16.04 on an Intel\(^{\circledR }\) Core\(^{\text {TM}}\) i7-8550U CPU 1.80 GHz and 8 GB of RAM. The results are shown in Table 6. “Insert” is to synthesize a program that inserts a cell before the head, “Remove” is the list disposal program, “Traverse” is to travel a list, “Append” is to append two lists into one. Sometimes we cannot synthesize a list program by our approach. For instance, reversing a list is impossible to be synthesized since the initial state and the goal are both an abstract list. Whether the list is reversed or not finally is never known. The second column is the search time in seconds. The third column is length of a policy. Note that the length includes additional actions (check actions and abstraction actions) except primitive command actions.

Table 6. Experimental results on list program
Full size table
Fig. 3.
figure 3

Policy for synthesizing the disposal program

Full size image

PRP generates a sequential plan for “Insert” and constructs loops for the other three programs. Consider the performance, we can see that synthesizing loop programs is not easy since the search time is much more than synthesizing sequential ones. More efforts needs to be made in order to find a loop for a planner. The essential reason is the quantifiers in the encoded actions especially in the effects of abstractions and preconditions of check actions. In practice, the quantifiers are expanded that will result in the explosion of the state space.

The solution generated for disposal program is shown in Fig. 3. We preserve the command actions and remove rest. Therefore, we obtain a compact policy much closer to a pointer program. Obviously, the policy is similar to the disposal program mentioned before. The boolean condition at the start of the loop must be specified manually.

7 Conclusion

Synthesizing programs is a difficult and central problem in computer science. In this paper, we propose an automated planning based method for pointer program synthesis. Inspired by symbolic execution of separation logic, we compile this process into a FOND planning problem, mainly including primitive command compilation, rearrangement compilation and abstraction compilation. In future work, we plan to synthesize larger scale programs. This is feasible from the theoretical point of view because of the modular reasoning feature of separation logic. Furthermore, we have to find a way that can reduce the number of quantifiers in the encoded actions to improve the performance of planners.