1Symbolic ExecutionSaswat Anand22/09/2009Limitation of Dataflow Analysisif(p < 10)x = 1i =10if(p > 10)x=x+1j = i+1Is the DU pair involvingvariables I real?No, because the pathis infeasible.2Outline• Background– feasible and infeasible program paths– constraints, and constraint satisfiability • Symbolic execution– base idea– handling of symbolic references• Overview of compositional symbolic execution• Overview of implementation of symbolic execution • Limitations of symbolic execution• SummaryFeasible and Infeasible Paths•A path refers to a path in the (inter-procedural) control-flow graph of the program.• A path is feasible if there exists an input I to the program that covers the path; i.e., when program is executed with I as input, the path is taken.• A path is infeasible if there exists no input I that covers the path.3Infeasible Paths• Infeasible path does not imply dead code; However dead code implies infeasible path.• In all real software, a very large portion of the total no. of paths are infeasible.• Automatic test-input generation does not scale when there are large no. of infeasible paths to the target location that needs to be covered.If(sameGoto)newTarget = ((IfStmt) stmtSeq[5]).getTarget();else {newTarget = next;oldTarget = ((IfStmt) stmtSeq[5]).getTarget();}…If(!sameGoto)b.getUnits().insertAfter(…);…An example of infeasible path from soot. A path that goes through the then branchesof both conditional stmt.s is infeasible.ConstraintsX > Y Λ Y+X ≤ 10• X, Y are called free variables.•A solution of the constraint is a set of assignments, one for each free variable that makes the constraint satisfiable. • {X = 3, Y=2} is a solution. • {X = 6, Y=5} is not a solution.More types of constraints1. Linear constraint•X > Y Λ Y+X ≤ 102. Non-linear constraint•X * Y < 100•X % 3 Λ Y > 10•(X >> 3) < Y 3. Use of function symbols•f(X)> 10 Λ (forall a. f(a) = a + 10)4Constraints (contd.)•A decision procedure is a tool that can decide if a constraint is satisfiable.•A constraint solver is a tool that finds satisfying assignments for a constraint, if it is satisfiable. • In general, checking constraint satisfiability is undecidable.Symbolic Execution• Symbolic execution refers to execution of program with symbols as argument.• Unlike concrete execution, where the taken path is determined by the input, in symbolic execution the program can take any feasible path.• During symbolic execution, program state consists of– symbolic values for some memory locations– path condition• Path condition is a condition on the input symbols such that if a path is feasible its path-condition is satisfiable.• Solution of path-condition is an test-input that covers the respective path.5Symbolic Execution1 int x, y;2 if(x > y){3 x = x+y;4 y = x – y;5 x = x – y;6 if(x > y)7 assert false; 8 }9 printf(x,y);inputs that cover else branch at stmt. 2:x = ? y = ?inputs that cover then branch at 2 and else at 6:x = ? y = ?x=A,y=Bx=A+B,y=AA>Bx=A+B,y=BA>Bx=B,y=AA>Bx=A,y=BA>Bx=B,y=AA>BΛB≤Ainputs that cover else branch at stmt. 2:x = 3 y = 4One solution of the constraint A>B Λ B≤A is A = 5, B = 1 inputs that cover then branch at 2 and else at 6:x = 5 y = 1Symbolic Execution1 int x, y;2 if(x > y){3 x = x+y;4 y = x – y;5 x = x – y;6 if(x > y)7 assert false; 8 }9 printf(x,y);inputs that cover else branch at stmt. 2:x = ? y = ?inputs that cover then branch at 2 and else at 6:x = 5 y = 1inputs that cover then branch at 2 and then at 6:x = ? y = ?x=A,y=Bx=A+B,y=AA>Bx=A+B,y=BA>Bx=B,y=AA>Bx=B,y=AA>BΛB>AUNSAT!x=A,y=BA>Binputs that cover else branch at stmt. 2:x = 3 y = 4Does not exist!6All-paths Symbolic Executionint x, y;if(x > y){x = x+y;y = x – y;x = x – y;if(x > y)assert false; }printf(x,y);input: x = 4, y = 3output: 3, 4input: x = A, y = Boutput: A, BPath-condition: A ≤ Boutput: B, APath-condition: A>B Λ B ≤ ANormal executionSymbolic executionx=A,y=BPC: truex=A,y=BPC: A≤Bx=A+B,y=APC: A>Bx=A+B,y=BPC: A>Bx=B,y=APC: A>Bx=B,y=APC: A>BΛB>AUNSAT!x=A,y=BPC: A>Bx=B,y=APC: A>BΛB≤AHandling Symbolic References1 class Node {2 int elem;3 Node next;4 foo(Node n1, Node n2){5 if(n1 == null) return;6 if(n2 == null) return;7 if (n2.elem == 0) 8 return;9 if (n1.next != null)10 n1.next.elem = n1.elem -10;11 assert(n2.elem != 0);12 }7Handling Symbolic References• setElem(H,n,e) – updates the elem field of node n in heap H to value e; returns the updated heap• getElem(H,n) – returns the value of elem field of node n in heap H• setNext(H,n,e), getNext(H,n) – likewise for next fieldforall H, n. getElem(setElem(H,n,v),n) = vforall H, n. getNext(setNext(H,n,v),n) = vInvariants:Handling Symbolic References 1 class Node {2 int elem;3 Node next;4 foo(Node n1, Node n2){5 if(n1 == null) return;6 if(n2 == null) return;7 if (n2.elem == 0) 8 return;9 if (n1.next != null)10 n1.next.elem = n1.elem -10;11 assert(n2.elem != 0);12 }n1 ≠ null Λn2 ≠ null ΛgetElem(H1,n2) ≠ 0 ΛgetNext(H1,n1) ≠ null ΛH2 = setElem(H1,getNext(H1,n1),getElem(H1,n1)-10) ΛgetElem(H2,n2) = 0Path condition for the path 4-5-6-7-9-10-118Compositional Symbolic Execution• Goal: generate an input that covers leads to execution of error()• No. of paths to error() = 250• Symbolically executing each path and checking its feasibility does not scale!• Key idea: compute function summaries to be used at all call-sites of the functionint abs(int x){if(x >= 0)return x;elsereturn –x;}int sumAbs(int[] a){int sum = 0;for(int i = 0; i < 50; i++)sum += abs(a[i]);if(sum == 13)error();return sum;}Compositional Symbolic Execution (contd.)• Symbolically execute all paths of callee function (e.g., abs) and compute a function summary. • For each path in a function, the summary encodes path-condition of each path and the value returned on the path.• When symbolically executing paths in caller function (e.g., sumAbs) reuse the summary of the callee instead of symbolically executing paths in callee repeatedly.int abs(int x){if(x >= 0)return x;elsereturn –x;}int sumAbs(int[] a){int sum = 0;for(int i = 0; i < 50; i++)sum += abs(a[i]);if(sum == 13)error();return sum;}9Compositional Symbolic Execution (contd.)int abs(int x){if(x >= 0)return x;elsereturn –x;}int sumAbs(int[] a){int sum = 0;for(int i = 0; i < 50; i++)sum += abs(a[i]);if(sum == 13)error();return sum;}forall x. (x ≥ 0 Λ abs(x) = x) V (x < 0 Λ abs(x) = -x)summary of abs