��Program Synthesis�A Tutorial

Yingfei Xiong

Peking University

ISSTA Summer School 2019

Can grandmas program?

• The development of programming languages is to raise the level of abstraction

2

Level of

Abstraction

What is the next?

Haskell (1990), Prolog (1972)

Java

C

Assembly

Why cannot?

• Programming languages come with many guarantees
• Well-typed programs are guaranteed to compile
• Compiled programs have clear, well-defined semantics

​

• It is difficult to further raise the level of abstraction

3

Program

Compile

Executable

Program Synthesis saves grandmas

• Generate a program from a specification
• Specification can be fuzzy
• Generation is not guaranteed

​

​

4

Specification

Synthesize

Program

“One of the most central problems in the theory of programming.”

----Amir Pneuli

Turing Award Recipient

“The fundamental way to improve software productivity.”

----Jiafu Xu

Founder of Software Research in China

History of Program Synthesis

5

Application – Data Wrangling

6

Application – Superoptimization

7

i=round(i);

a = 6755399441055744.0;

i=(i+a)-a;

Application – Reducing Duplicated Programming

8

Application – Program Repair

9

Synthesize an expression to replace the buggy one

Application – Testing

10

Synthesize a unit test to cover a path

Application – Analysis

11

Synthesize a strategy for a class of problems

Defining Program Synthesis

12

Test Generation

Superoptimization

Program Repair

This Lecture

13

SyGuS: Syntax-Guided Synthesis

14

Example: max

• Grammar:

​

​

​

• Specification:

​

• Expected answer：ite (x <= y) y x

15

SyGuS format: Synth-Lib

• Synth-Lib uses a format similar to SMT-Lib
• http://sygus.seas.upenn.edu/files/SyGuS-IF.pdf

​

​

16

(set-logic LIA)

(synth-fun max2 ((x Int) (y Int)) Int

((Start Int (x y

(+ Start Start)

(ite StartBool Start Start)))……))

​

(declare-var x Int)

(declare-var y Int)

(constraint (>= (max2 x y) x))

……

​

(check-synth)

Program Synthesis as a Search Problem

17

Generate

Verify

Q1: How to generate the next program to be verified?

Q2: How to verify the correctness?

a program

correct

incorrect

Q1: How to verify correctness?

18

Fast

Slow

Can we combine

the two?

CEGIS: Counter-Example Guided Inductive Synthesis

• Constraint solvers give counter-examples
• Save counter-examples as tests
• First use tests to validate programs

19

Program

Counter-

Example

No Counter-

Example

Q2: How to generate the next program to be verified?

• Enumerative – exhaustive search
• Representation-based – manipulate sets of programs instead of single programs
• Constraint-based – convert to an SMT problem

20

Top-Down Enumeration

• Expand according to the grammar
• Expr
• x, y, Expr+Expr, if(BoolExpr, Expr, Expr)
• y, Expr+Expr, if(BoolExpr, Expr, Expr)
• Expr+Expr, if(BoolExpr, Expr, Expr)
• x+Expr, y+Expr, Expr+Expr+Expr, if(BoolExpr, Expr, Expr)+Expr, if(BoolExpr, Expr, Expr)
• …

21

Bottom-Up Enumeration

• Combine expressions from small to big
• size=1
• x, y
• size=2
• size=3
• x+y
• size=4
• size=5
• x+(x+y), (x+y)+y
• size=6
• if(x<=y, x, y), …

​

22

Optimization

• Discard a partial program early

​

• Pruning
• None of the expansions could satisfy the specification
• Ite BoolExpr x x

​

• Equivalence reduction
• Equivalent to a previous program
• Expr+x, x+Expr

​

23

Pruning

• Generate constraints from the partial program

​

​

​

• Generate constraints from each test

​

​

​

24

Ite BoolExpr x x

(declare-fun boolExpr () Int)

(declare-fun max2 ((x Int) (y Int)) Int

(ite boolExpr x x))

max2(1,2)=2

(assert (= (max2 1 2) 2))

(check-sat)

Needs to balance between the benefit and the cost.

Equivalence reduction: How to determine equivalence?

25

How to generate the next program to be verified?

• Enumerative – exhaustive search
• Representation-based – manipulate sets of programs instead of single programs
• Constraint-based – convert to an SMT problem

26

Representation-based

• Enumerative approaches manipulates single programs
• Inefficient: too many in number
• Can we manipulate sets of programs? e.g.
• Find a set that satisfies a specification
• Intersects sets for a conjunction of specifications
• Combine sets with program constructs to satisfy more complex specifications
• Representation-based
• Use data structures to represent such a set
• E.g. Grammars, Automata, Logic Formulas

​

27

FlashMeta: Basic Idea

• Grammar is a representation of sets
• Size of a grammar = O(log(#Represented Program))
• The original grammar is too coarse-grained

​

• Idea: Annotate a non-terminal with a synthesis goal
• [2]Expr – expressions that evaluates to 2

​

​

​

28

FlashMeta: Single Test

29

Intersection of grammars

30

FlashMeta: Multiple Tests

• Produce a grammar for each test
• Intersects the grammars

31

FlashMeta: Discussion

32

How to generate the next program to be verified?

• Enumerative – exhaustive search
• Representation-based – manipulate sets of programs instead of single programs
• Constraint-based – convert to an SMT problem

33

Component-Based Program Synthesis

34

o1

o2

o3

o4

o5

o6

o7

i11

i12

i21

i22

i31

i32

i41

i42

i51

i53

i52

1

2

3

4

5

6

7

8

9

Components

Connection

Points

Generate constraints

35

This Lecture

36

Program Estimation

37

Program Estimation as an Search Problem

38

Program

Probability

Enough?

Program with the highest probability

Learning to synthesis (L2S)

• A general framework to address program estimation

​

• Combining four tools
• Rewriting rules: defining a search problem
• Constraint solving: pruning off invalid choices in each step
• Machine-learned models: estimating the probabilities of choices in each step
• Search algorithms: solving the search problem

Example: Condition Completion

• Given a program without a conditional expression, completing the condition

​

​

​

​

• Useful in program repair
• Many bugs are caused by incorrect conditions
• Existing work could localize the faulty condition
• Can we generate a correct condition to replace the incorrect one?

40

Space of Conditions

Q3: Estimating the Probability

• Idea: Using machine learning
• To train over a set of programs and their contexts
• Problem: machine learning usually works for classification problems
• where the number of classes are usually small
• Idea: turn the generation problem into a set of classification problem along the grammar

41

Decomposing Generation

• In each step, we estimate the probabilities of the rules to expand the left-most non-terminal
• A classification problem

42

E

Expand E with E -> E “> 12”

Expand E with

E -> “hours”

Probability of the program

43

Training models

• Train a model for each non-terminal
• to classify rules expanding this non-terminal
• Training set preparation
• The original training set:
• A set of programs
• Their contexts
• Decomposing the training set:
• Parse the programs
• Extract the rules chosen for each non-terminal

​

44

Feature Engineering

45

…;if(

) throw new ArgException();

Can we use a different expansion order?

46

• Top-down

​

​

​

• Bottom-up

The order may greatly affect the performance of L2S.

Annotations

From Grammar to Rewriting Rules

�

Example

• Top-down

​

​

​

• Bottom-up

Unambiguity

50

Q4: How to find the most probable program?

51

0.6 * 0.2

= 0.12

0.3 * 0.8

= 0.24

Use Metaheuristic Search

• Beam Search:
• Keep n most probable partial programs
• Expand the programs to get new programs
• Genetic Search:
• Keep n most probably complete programs
• Mutate the programs to get new programs

52

Applications

• Application 1:
• Repairing Conditional Expressions
• Application 2:
• Generating Code from Natural Language Expression

53

Repairing Conditional Expressions

• Condition bugs are common

​

​

​

​

​

​

• Steps:
1. Localize a buggy if condition with SBFL and predicate switching
2. Synthesize an if condition to replace the buggy one
3. Validate the new program with tests

Missing boundary checks

- if (hours >= 24)

+ if (hours > 24)

withinOneDay=true;

Conditions too weak or too strong

lcm = Math.abs(a+b);

+ if (lcm == Integer.MIN_Value)

+ throw new ArithmeticException();

L2S Configuration

• Rewriting rules
• Bottom-up
• Estimate the leftmost variable first
• Machine learning
• Xgboost
• Manually designed features
• Constraints
• Type constraints & size constraints
• Search algorithm
• Beam search

​

​

​

​

55

Results

56

Also repaired 8 unique bugs that have never been repaired by any approach.

Benchmark: Defects4J

Generating Code from Natural Language Expression

• Can we generate code automatically to avoid repetitive coding?
• Existing approaches use RNN to translate natural language descriptions to programs
• Long dependency problem: work poorly on long programs

57

L2S Configuration

• Rewriting rules
• Top-down
• Machine learning
• A CNN-based network
• Constraints
• Size constraints
• Search algorithm
• Beam search

​

​

​

​

​

58

A CNN-based Network Architecture

59

Results

60

Benchmark: HearthStone

Newest Results

• Replacing CNN with Transformer
• Transformer: a new neural architecture at 2017
• The flexibility of L2S allows to easily utilize new models

61

Future Learning

• Surveys:
• Sumit Gulwani, Oleksandr Polozov, Rishabh Singh: Program Synthesis. Foundations and Trends in Programming Languages 4(1-2): 1-119 (2017)
• Rajeev Alur, Rastislav Bodík, et al.: Syntax-guided synthesis. FMCAD 2013: 1-8
• Tools:
• sygus.org – the SyGuS competition, a good place to look at
• Some tools we recently used
• EUSolver
• CVC4
• Second-Order Solver
• Course:
• Program Synthesis by Nadia Polikarpova@UCSD
• https://github.com/nadia-polikarpova/cse291-program-synthesis/

62

Reference

• Enumerative
• Sumit Gulwani, Oleksandr Polozov, Rishabh Singh: Program Synthesis. Foundations and Trends in Programming Languages 4(1-2): 1-119 (2017)
• Rajeev Alur, Rastislav Bodík, et al.: Syntax-guided synthesis. FMCAD 2013: 1-8
• FlashMeta
• Oleksandr Polozov, Sumit Gulwani: FlashMeta: a framework for inductive program synthesis. OOPSLA 2015: 107-126
• Componen-Based Program Synthesis
• Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari: Oracle-guided component-based program synthesis. ICSE (1) 2010: 215-224
• L2S
• Yingfei Xiong, Bo Wang, et al.: Learning to Synthesize. GI'18: Genetic Improvment Workshop, May 2018

​

63