Imperative Program Synthesis by Abstract Static Analysis and SMT Mutations

Imperative Program Synthesis by Abstract Static Analysis and SMT Mutations

연구 분야: Strategies

학회: GPCE '25: Proceedings of the 24th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences

This paper introduces a novel technique for synthesizing imperative programs that meet behavioral specifications given in the form of assumptions and assertions (logic formulas). In particular, we combine basic statement-directed enumerative search, static analysis via abstract interpretation, and expression-directed enumerative search via (incremental) SMT-based mutations to efficiently explore all candidate complete programs generated from an input program template (with statement and expression holes) until a solution is found. Firstly, the algorithm uses a basic enumerative search through the space of all possible statements, thus filling in all statement holes. In effect, we obtain partial programs with only missing (arithmetic and boolean) expressions, which are subsequently classified by a static analysis either as potential solutions or as definite failures. Finally, we repeatedly mutate the missing expressions in potential solutions and check if the resulting complete programs become bounded correct with respect to the given assertions. We have implemented our technique in a prototype tool and evaluated it on a set of introductory C programs. The experimental results confirm the effectiveness of our technique for synthesizing various interesting C programs.