A Clause Matching Based Approach To Reuse Constraint Solutions In Symbolic Execution

Symbolic execution is an effective program analysis technique for test generation and error detection in software applications.Constraint solving is the most timeconsuming task in symbolic execution and reusing previously solved solutions is an effective way to optimize constraint solving in symbolic execution.Existing approaches have exploited different strategies of solution reuse.However,all these strategies assume that one constraint is an atomic entity for reuse.This universally accepted atomic assumption severely limits opportunities of solution reuse in symbolic execution and when the scale of programs grows or constraints in programs are complex,it is hard to find a matching solution in a whole.On the other hand,there exists an obvious regularity in the constraints imposed by symbolic execution: many constraints are composed of a series of identical or similar clauses,each of which refers to a condition of a specific program branch.The path condition of the program is composed of different branch conditions,so the constraint is imposed of identical or similar clauses.This phenomenon inspires us to reuse based on clauses rather than the entire constraint,which may be a better reuse strategy and can achieve better reuse.We propose ClauseCache,an approach that reuses solutions to clauses rather than solutions to entire constraints.ClauseCache reuses solutions based on decomposed storage and combined reuse.ClauseCache splits a constraint solution into clause solutions for reuse.For a new constraint that looks for a reusable solution,ClauseCache finds a feasible composition of candidate clause solutions.Compared with solution reuse methods based on the whole constraint,ClauseCache reuses solutions at a finer granularity and then has stronger reuse capacity.In theory,we also prove that the ClauseCache exceeds the three reuse methods based on equivalence,subset/superset,and logical subset/superset in reuse capacity.To reduce the huge search space of compositing solutions,ClauseCache achieves fast search by two fast filtering and a heuristic exploration.When searching for reusable solutions for the constraint to be solved,ClauseCache first selects the candidate values for each variable based on the rule: the value of the same variable must be the same in different clauses,and then uses the candidate values of the variables to further filter the candidate solutions of each clause.Through these two steps,ClauseCache filters the search space and effectively reduces the search space of the composition clause solutions.Finally,ClauseCache searches filtered candidate solution combination with a heuristic strategy to find a set of feasible solutions.Since a lot of set operations are used in fast filtering,we adopt two BitSet-based indexes reduce the complexity of the set operations to a constant level.We implement ClauseCache in java and integrate it into jConcolic,which is a java dynamic symbolic execution engine,to achieve the solution reuse in the actual dynamic symbol execution.In jConcolic,a series of pre-processing is performed on the constraints to support solution reuse before checking reusable solution of constraints,including simplification of array constraints,constraint slice,constraint normalization,constraint reduction.The pre-processing makes the constraints to be solved shorter and simpler,which is beneficial to improve the possibility of solution reuse.We evaluate ClauseCache on the real program benchmark as to absolute reuse capacity and reuse capacity on actual dynamic symbolic execution.In the actual dynamic symbol execution,the effective and efficiency of ClauseCache are evaluated in three typical reuse scenarios:(1)reuse in a single program;(2)reuse across program versions;(3)reuse cross programs;Experiments show that,ClauseCache could reuse more solutions than GreenTrie,Klee's reuse method and Green,Also,ClauseCache can significantly improve the reuse rate and query time,and further improve the efficiency of symbol execution,compared to the most advanced reuse methods: Green,GreenTrie,Utopia and KLEE's reuse method.