CSE411: Introduction to Compilers

Program Synthesis

Jooyong Yi (UNIST)

20% Rule

Synthesizing a Lexer

           regular expression
                    ↓
             |-------------|    
             |    Lexer    |        
             | Synthesizer |
             |-------------|
                    |
               synthesizes   
                    ↓
                |-------|            
int val = 10; → | Lexer | → int ID ASSIGN NUM ;
                |-------|                          

Synthesizing a Program

              specification
                    ↓
             |-------------|    
             |   Program   |        
             | Synthesizer |
             |-------------|
                    |
               synthesizes   
                    ↓
               |---------|            
               | Program |
               |---------|                          

Concrete Example of Program Synthesis

• Excel Flash Fill

Under the Hood of Flash Fill

Running Example

Under the Hood of Flash Fill (Step 1)

Use a Domain-specific language (DSL) to limit the synthesis space.

Under the Hood of Flash Fill (Step 2)

Sub-problems

• When , how to define and ?

Under the Hood of Flash Fill (Step 3)

Inverse Semantic Operator

• When , how to define and ?
• We can define the semantics of and .

Under the Hood of Flash Fill (Step 4)

Under the Hood of Flash Fill (Step 5)

Use VSA (Version Space Algebra) for compact representation.

Version Space Algebra

Syntax

Semantics

Under the Hood of Flash Fill (Step 6)

The second IO example:

Under the Hood of Flash Fill (Step 7)

Intersection of VSAs