Path SlicingOutlineUse of Path SlicesExample of CFAControl Flow AutomataWeakest PreconditionsExample of PathsPaths and SlicesCompletenessSoundnessExamplePath Slice AlgorithmExperimental ResultsConclusionPath SlicingPresentation by Massimiliano MenariniRanjit Jhala and Rupak Majumdar, “Path Slicing” PLDI 05 (June 2005, Chicago, Illinois)OutlineUse of Path SlicesModel checking and counter examplesControl Flow Automata Weakest Preconditions Properties of Path SlicesCompletenessSoundnessPath Slice AlgorithmExperimental ResultsConclusionUse of Path SlicesModel checkingAllow for the exploration of the execution space of an application to find some errorReturn a counter example: an execution path form the start state to an error stateMotivation for using Path Slicing techniques The returned counter example can be very longFor example the paper presents an experiment where a property checked on gcc returned a 82,695 basic blocks counter exampleObtain understandable counter examplesWe are interested in only the operations that affect the reachability of the error state (potentially a fraction of the full counter example)Example of CFASourceEx() {0: if(a>0)1: x=1;2: c=0;3: for(i=1;i<1000;i++)4: c=c+f(i);5: if(a>0){6: if(x==0){ ERR: }} ... }CFA01233’456Err Exit[a>0][a≤0]x=1c=0i=1[i<1000][i≥1000]c=c+f(i)i++[a>0][a≤0][x==0]Control Flow AutomataIt is a CFG with operations on the edges and program counter on the vertexesFormallyOperations (Ops) of 2 typesAssignment: l:=eassume: assume(p)CFA Cf=(PCf, pc0, pcout, Ef, Vf)PCf is a set of locations (program counters)pc0PCf is the start locationpcoutPCf is the exit locationEf set of edges, Ef PCf Ops PCf Vf set of variables (?)Weakest PreconditionsGiven a logical formula over a set of variables X. represents all X-states where the values of X satisfy The weakest precondition (WP) of with regard to the operation op Ops (WP..op) is the set of states that can reach a state in after executing op X={a}Ops={a=0, a=1} =[a==1]Therefore identifies {a=1}WP..(a=1)={all}WP..(a=0)={Ø}Example of PathsCFA01233’456Err Exit[a>0][a≤0]x=1c=0i=1[i<1000][i≥1000]c=c+f(i)i++[a>0][a≤0][x==0]Path to pc=601233’56[a>0]x=1c=0i=1[i≥1000][a>0]Trace[a>0]x=1c=0i=1[i≥1000][a>0]VariablesacixCannot execute: this is an unfeasible pathTo execute must be a>0 ()Paths and SlicesA path from pc to pc’ is a sequence of edges of the CFA such that: the destination of one and the source of the next coincide, the source of the first edge is pc and the destination of the last is pc’A trace is the sequence of operations on the edges of a pathA path is feasible if there is some state that can execute itA state s can reach a location pc if there exist a path from pc0 to pc that can be executed by sA Path Slice ’ is a subsequence of a path Completeness’ is a complete slice of (path from pc0 to an error location pc) if for every sWP.true.Tr.’ either:there exist a program path ’’ from pc0 to pc such that s can execute ’’, orS cannot reach pcoutTherefore if there is a complete slice to an error location and it is feasible (therefore executable for some state), we are guaranteed that for each state that can execute the slice there exist an executable path that reach the error locationSoundnessA path slice ’ of is a sound slice if WP.true.(Tr.) WP.true.(Tr.’)So a state that can execute the trace of a path can execute the trace if a sound slice of itExampleCFA01233’456Err Exit[a>0][a≤0]x=0c=0i=1[i<1000][i≥1000]c=c+f(i)i++[a>0][a≤0][x==0]Slice01233’56Err[a>0]x=0c=0i=1[i≥1000][a>0][x==0]4[i<1000]c=c+f(i)i++Slice01233’56Err[a>0]x=0c=0i=1[i≥1000][a>0][x==0]4[i<1000]c=c+f(i)i++Not Sound sliceThe path could execute in s={a>0} the slice only in s’={a>0, x=0}Complete and Sound SlicePath Slice AlgorithmBackward traversal of the CFAKeep 2 informationlvalues set L (the set of lives values)Step location pcs An edge is added to the slice ifIt assign one of the lvaluesIf there is a branch that can bypass the current stepIf there is a path from the current edge to the step edge that assign one of the lvaluesExperimental ResultsTested correctens of files handling in real programs (fcron, wuftpd, make, privoxy, ijpeg, openssh, gcc)In average the length of the Slice was 5% of the length of the original traceIn case of longer traces the slices where much shorter (0.1%)ExamplesShortest trace 47 operations: output 27 operations (57%)Longest trace 82,695 operations: output 43 operations (less that 0.1%)ConclusionPath Slicing is an interesting technique to reduce the size of a counter exampleAn linear algorithm that return a Sound and Complete path slice is providedImplemented in the Blast model checkerExperimental results on real programs proved the benefit of that approachLimitationsThe implementation use a depth first search for counter examples that returns very long tracesImprecise model of the heap creates problems in the verification of certain programsSlow implementation of WrBt and By functions used by the algorithm, don’t scale
View Full Document