fse_talk_v12

Synthesizing Data Structure Manipulations from Storyboards: 

Synthesizing Data Structure Manipulations from Storyboards Rishabh Singh and Armando Solar- Lezama

Programming with Code: 

Programming with Code dllDelete (Node v) { n = v.next ; p = v.prev ; p.next = n; n.prev = p; } b x next prev a next prev v

Heap Structure: 

Heap Structure b next prev a next prev next prev b x next prev a next prev next prev next prev v x n

Bridging the semantic gap: 

Bridging the semantic gap b x next prev a next prev b next prev a n dllDelete (Node v) { n = v.next ; p = v.prev ; p.next = n; n.prev = p; } WHAT? HOW? Program Synthesis

Programming with Scenarios: 

Programming with Scenarios A scenario is more powerful than an example each scenario represents an infinite set of examples It is also less powerful Partial specification, ambiguous for … b next prev a b x next prev a next prev n b x next prev a next prev n next prev next prev next prev next prev

Synthesis with Scenarios: 

Synthesis with Scenarios Idea: combine many simple specs to constrain behavior Abstract Scenarios Structural Info Concrete Scenarios Synthesizer Storyboard Framework Correct Code Storyboard

Example: 

Example

Linked List Reversal: 

Linked List Reversal next f e mid a b e’ f’ mid’ a b head next next next head

Scenarios for LL-reversal: 

Scenarios for LL-reversal a b next head a b head next a head a head head head f e mid a b head next next e’ f’ mid’ a b next next head

Inductive structure with fold/unfold: 

Inductive structure with fold/unfold f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ Unfold:

Inductive structure with fold/unfold: 

Inductive structure with fold/unfold f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ Unfold: f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ F old:

Loop Sketch: 

void llReverse( Node head) { ?? /*1*/ while ( ?? /*p*/ ) { ?? /*2*/ } ?? /*3*/ } Loop Sketch

Loop Sketch: 

void llReverse( Node head) { cstmt * /*1*/ while ( cond /*p*/ ) { cstmt * /*2*/ } cstmt * /*3*/ } Loop Sketch

Conditional Statements : 

Conditional Statements cstmt : if (COND) then STMT var (. ptr ? ) op var (. ptr ? ) | null var (. ptr ? ) = var (. ptr ? ) unfold/fold var

Storyboard Constraints: 

Storyboard Constraints f e mid a b head next next e’ f’ mid’ a b next next head f e mid f’ e’ mid x’ next x’ x’ = f x’= e x’ = f e = e’ Abstract Scenarios a b next head a b head next a head a head head head Concrete Scenarios void llReverse( Node head) { ?? /*1*/ while ( ?? /*p*/ ) { ?? /*2*/ } ?? /*3*/ } Structural Info

Synthesized Implementation: 

Synthesized Implementation void llReverse( Node head) { Node temp1 = null , temp2 = null , temp3 = null ; temp1 = head; while (temp1 != null ) { // unfold temp1; head = temp1; temp1 = temp1.next; head.next = head; head.next = temp3; temp3 = head ; // fold temp3; } }

Demo: 

Demo

How it Works: 

How it Works

Data flow equations: 

Data flow equations s in s 1 s 3 s 2 s out f 1 f 2 f 3 f p true false

Synthesis vs. Verification: 

Synthesis vs. Verification Verification known : f, s in unknown : s out Synthesis known : s in, s out unknown : f

Synthesis Challenges: 

Synthesis Challenges Find values for Can’t give to solver w e are interested in LFP s i are sets of shapes Key: a void set reasoning

1 : Loop unrolling: 

1 : Loop unrolling f 1 f 2 f 3 f p true false f 1 f 3 f p false path 0 f 1 f 3 f p false f p f 3 true path 1 f 1 f p f 3 true f 3 f p false . . . k iters path k

Slide 23: 

f 1 f 3 f p false path 0 f 1 f 3 f p false f p f 3 true path 1 f 1 f p f 3 true f 3 f p false . . . path k

2: Non-deterministic Functions: 

2: Non-deterministic Functions f Parameterize the non-deterministic choice n n

Solving the constraint: 

Solving the constraint Rewrite as subset constraints:

Quantifier alternation constraint: 

Quantifier alternation constraint

Quantifier alternation constraint: 

Quantifier alternation constraint Sketch solver

Experiments: 

Experiments

Data Structure Manipulations: 

Linked lists : insert, delete, reverse, swap-first-last Doubly Linked lists : reverse, traverse Binary Search Trees : search, min, rotate, insert, delete User-defined : AIG (And-Inverter-Graph) insertion Complex data structures : Red Black Tree Insertion Data Structure Manipulations

Red Black Tree Insertion: 

Red Black Tree Insertion 4 cases to fix red black tree invariant after insertion

Red Black Tree Insertion: 

Red Black Tree Insertion fixRBTree (Node root, Node x){ w hile(x.p != null && x.p.p != null){ y = x.p; z = x.p.p ; if(cond1) //case1 elsif (cond2) //case2 elsif (cond3) //case3 elsif (cond4) //case4 else break; x = z; } color[root] = black; }

And-Inverter Graph (AIG): 

And-Inverter Graph (AIG) DAG Two-input AND gates and inverters Encodes logical functionality of circuits Logic synthesis, technology mapping, physical synthesis, verification f : pointer to its father node m: pointer to its mother node nf : pointer to father’s next child nm: pointer to mother’s next child c h : pointer to its first child f m nf nm ch x

And-Inverter Graph (AIG): 

And-Inverter Graph (AIG) x ch

And-Inverter Graph (AIG): 

And-Inverter Graph (AIG) x ch

And-Inverter Graph (AIG): 

And-Inverter Graph (AIG) x ch f nf m nm

AIG Insertion: 

AIG Insertion z F x 1 x 2 x n ch f/m f/m f/m nf /nm nf /nm M y n y 2 y 1 ch nf /nm nf /nm f/m f/m f/m z F x 1 x 2 x n ch f/m f/m f/m nf /nm nf /nm M y n y 2 y 1 ch nf /nm nf /nm f/m f/m f/m nf /nm nf /nm f m

Case studies - I: 

Case studies - I Manipulation #Clauses Memory # Scen Time ll -insertion 1.99M 0.75G 4 2m9s ll -deletion 1.88M 0.54G 4 1m48s ll -reverse 1.30M 0.35G 4 1m49s ll -find-last 1.02M 0.29G 4 0m56s ll -swap-first-last 1.08M 0.31G 4 4m18s dll -traversal 1.72M 0.88G 4 1m58s dll -reversal 2.04M 0.49G 4 3m47s

Case studies - II: 

Case studies - II Manipulation #Clauses Memory # Scen Time bst -search(contains) 0.62M 0.37G 1 1m02s bst -search 0.77M 0.45G 1 6m07s bst -find-min 0.63M 0.45G 1 0m58s bst -find-max 0.57M 0.18G 1 0m23s bst -left-rotate 1.41M 0.50G 3 3m18s bst -right-rotate 1.47M 0.43G 3 3m15s bst -insertion 1.04M 0.46G 3 1m52s bst -deletion 0.63M 0.62G 6 3m13s Manipulation #Clauses Memory # Scen Time aig -insertion 0.17M 0.31G 4 1m04s

BST Deletion: 

BST Deletion Simple storyboard was under-constrained Two additional concrete instances were required Synergy b/w abstract and concrete scenarios s ix concrete scenarios do not scale

Research Questions: 

Research Questions Interactivity Debugging storyboards Corner cases Automated fuzzing of scenarios Encoding Symmetry reduction Concurrent data structures

Conclusion: 

Conclusion

Thanks!: 

Thanks! Questions/Comments rishabh@csail.mit.edu www.storyboardprogramming.com