Abstract Interpretation and Synthesis in Software Development

Lecture 19 Synthesis with Abstract Interpretation Armando Solar-Lezama

History POPL 77 paper by Patrick Cousot and Radhia Cousot Brings together ideas from the compiler optimization community with ideas in verification Provides a clean and general recipe for building analyses and reasoning about their correctness

Key idea 1: Abstract domain Concrete semantics New concrete states Concrete states x=5 x=7 x=6 x=8 x=-2 x=0 x=4 x=6 x := x + 2 x=-7 x=-5 x=-5 x=-3 x=7 x=9 x=9 x=11 ? ? ? + 2 ? ? + 2 {?}

Key idea 1: Abstract domain New abstract states Abstract states Abstract semantics x=5 x=7 x=6 x=8 x=-2 x=0 Odd Odd x=4 x=6 x := x + 2 x=-7 x=-5 x=-5 x=-3 x=7 x=9 Even ??? + ??? = ???? ??? + ???? = ??? ???? + ???? = ???? ???? + ??? = ??? Even x=9 x=11

Abstract values form a lattice Often called ???? ??? ???? ???? ??? ??? ???? ??? ???? ??? ??? ??? ???? ??? ??? ??? ??? ??? Often called

Abstract Domain An abstract domain is a lattice Although some analysis relax this restriction. Elements in the lattice are called Abstract Values Need to relate elements in the lattice with states in the program Abstraction Function: ?:? ??? Maps a value in the program to the best abstract value Concretization Function:?:??? ?(?) Maps an abstract value to a set of values in the program Example: Parity Lattice

Concretization ???? ??? x=5 x=6 x=-2 x=4 ??? ???? x=-7 x=-5 ??? ??? x=7 x=9

Abstraction ???? ??? x=5 x=6 x=-2 x=4 ??? ???? ` x=-7 x=-5 ??? ??? x=7 x=9

Key idea 2: Abstract Interpretation Compute an abstract value for every program point Abstraction of the set of states possible at that point Iterate until computation converges

Example ? = ? = L0 x = _input(); x = x * 2; L0 y = 0; x = _input(); L1 x = x * 2; y = 0; X<16 L1 while(x < 16){ L2 L2 x = x y; x = x y; y = 2 + x; L3 y = 2 + x; } L3 L4 L4 end

Example ? = ? = L0 x = _input(); x = x * 2; L0 y = 0; ? = ???? ? = ???? x = _input(); L1 x = x * 2; y = 0; ? = ???? ? = ???? X<16 L1 while(x < 16){ L2 L2 x = x y; x = x y; y = 2 + x; L3 y = 2 + x; } L3 L4 L4 ? = ???? ? = ???? end ? = ???? ? = ????

Some useful domains Ranges Useful for detecting out-of-bounds errors, potential overflows Linear relationships between variables ?1?1+ ?2?2+ + ???? ? Problem: Both of these domains have infinite chains!

Widening Key idea: You have been running your analysis for a while A value keeps getting bigger and bigger but refuses to converge Just declare it to be (or some other big value) This loses precision but it s always sound Widening operator: ?:??? ??? ??? ?1 ? ?2 ?1,?2

Abstract Interpretation for Synthesis

Example ? = ? = L0 x = _input(); x = x * ??1; y = 0; L1 L0 x = _input(); ? = ??1 ? = ??1 x = x * ??1; y = 0; ? = ??2 ? = ??2 X<16 L1 while(x < 16){ L2 L2 x = x y; x = x y; y = ??2 + x; assert even(y) L3 y = ??2 + x; L3 } ? = ??3 ? = ??3 L4 L4 end

Storyboard Programming head mid next next a f e b head mid next next a e f b

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

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

Inductive insights with fold/unfold Unfold: x = f x = e x mid f e mid x = f e = e next x f e Fold: x = f x = e x mid f e mid x = f e = e next x f e

Fold/Unfold These rules are part of the specification without them the scenarios are too imprecise They can also serve to communicate insights val > y.val y f=y b=b f stuff val ==y.val f=b=y stree b y f stree stuff stuff val < y.val b y f=y b=b f Underspecified summary node stuff stree b

Fold/Unfold These rules are part of the specification without them the scenarios are too imprecise They can also serve to communicate insights v next next next lleft a x b prev prev prev lright next next lleft a b prev prev lright

Concrete Domain Memory locations: # Variables: ?0,?1, ?? Variable predicates: ??: # Bool??(?) indicates that variable ?? points to loc ? Fields: ???0,???1, ???? Field predicates : ???0: # # ???? ?????1,?2 indicates that there is a field ???? from object ?1 to object ?2 # = {?,?} ??? ? = ???? ??? ? = ????? head next a b ???? ? ? ? false true ? false false

Inductive insights with fold/unfold Unfold: x = f x = e x mid f e mid x = f e = e next x f e Fold: x = f x = e x mid f e mid x = f e = e next x f e

Unfold mid x = f x = e x f e ???? ?? ? ???? ???? ? ? ? ??? ? ? ? ? false ? false true F T / / F tail head ? ? ? false ? false false F F F / F mid next next a f e b ? ? ? false ? false false F F F F T ??? ??? ??? {?,?} ??? false ??? true false F F / F / ? ? ? true ? false false F F F F F Unfold(head.next) ???? ?? ? ???? ???? ? ? ? tail head ? ? ? false ? false true F T F next next b a x ? ? ? false ? false false F F T ? ? ? true ? false false F F F

Unfold mid mid x = f e = e next f e x f e ???? ?? ? ???? ???? ? ? ? ??? ? ? ? ? false ? false true F T / / F ? ? ? false ? false false F F F / F tail head ? ? ? false ? false false F F F F T mid next next a f e b ??? ??? ??? {?,?} ??? false ??? true false F F / F / ? ? ? true ? false false F F F F F Unfold(head.next) ???? ?? ? ???? ???? ? ? ? ? ??? ? ? ? ? false ? false true F F F T F F tail head ? ? ? false ? false false F F F F / F mid next next next a x f e b ? ? ? false ? false false F F F F F T ? ? ? false ? false false F T / F / F ??? ??? ??? {?,?} ??? false ??? F true false F / F F / ? ? ? true ? false false F F F F F F

Example head mid next f e b x = head; while (x.next != null){ x = x.next; } x head mid next f e b

Example head mid next f e b head mid x next f e b x = head; while (x.next != null){ unfold(x); p = x; x = x.next; fold(p); } head head x mid x next next mid x f e b next next x f e b p head head x x next x b next p x b head x p mid mid next f e b f e x head head x mid next mid f e b p next b f e

Example head mid next f e b head mid x next f e b head x = head; while (x.next != null){ unfold(x); p = x; x = x.next; fold(p); } mid x next next x f e b head x mid head next next x f e b p x next x b head x head next x p x b p mid mid next x f e b f e head x p mid mid next f e b f e x head head x mid next mid f e b p next b f e

Example head head mid mid x next next f e b f e b head x head mid x = head; while (x.next != null){ unfold(x); p = x; x = x.next; fold(p); } next next mid x f e b p x next next x f e b head x head next p x b x next x b head x p head mid mid x next p x f e b f e mid mid next x f e b f e head x p mid mid next f e b f e x head mid head x next f e b mid p next b f e

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

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

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

Data flow equations sin ?1= ?1??? ?2?2 f1 ?2= ???1 f2 s1 ?3= ???1 false true fp s3 ????= ?3?3 s2 f3 sout

Synthesis vs. Verification Verification known : f, sin unknown : sout ?1= ?1??? ?2?2 ?2= ???1 ?3= ???1 Synthesis known : sin, sout unknown : f ????= ?3?3

Synthesis Challenges Find values for ?? ?1= ? ???,?1 ? ?2,?2 Can t give to solver we are interested in LFP si are sets of shapes ?2= ???1,?? ?3= ???1,?? Key: avoid set reasoning ????= ? ?3,?3

1 : Loop unrolling P f1 m iterations fp f2 Abstract Interpreter false true f3 m : fixpoint bound of P

1 : Loop unrolling f1 fp f1 f1 f1 true fp f3 k true . . . iters fp f2 f3 fp false false true fp fp f3 f3 ? ? false false f3 f3 path0 path1 pathk

f1 f1 fp f1 true fp f3 true f3 ????= ? ??? ?(??, ? ) . . . fp false fp fp false f3 false f3 f3 path1 path0 pathk

2: Non-deterministic Functions head mid next next a f e b ??? ?(??, ? ) f unfold head ?(??, ? ) ??? ? n head head mid next next next next next f e a x b a x b ?(??, ? ) ????= ? ? ??? ?

Solving the constraint ?(??, ? ) ????= ? ? ??? ? ?(??, ? ) ???? ? ? ??? ? ?(??, ? ) ???? ? ? ??? ?

Quantifier alternation constraint ?(??, ? ) ???? ? ? ??? ? ???, ? ???? ? ? ??? ? ?(??, ? ) ???? ? ? ??? ? ???, ? = ???? ? ? ??? ?

Quantifier alternation constraint ?(??, ? ) ???? ? ? ??? ? ???, ? ???? ? ? ??? ? ?(??, ? ) ???? ? ? ??? ? ???, ? = ???? ? ? ??? ? ???????????