Selective Symbolic Execution Based Patch Validation

Validating patches correctly and efectively is critical to both software quality im-provement and programmers’ productivity. Static analysis approaches can often detectpart of the possibly incorrect errors without even executing it. While in the meantime,dynamicsymbolicexecutiontoolscanbeusedtogeneratetestcaseswithhighcoverageautomatically. However both of them are restricted to the size of the software undertesting, thus lacking the scalability. In reality, neither of them are applicable to largescale software; instead they generally act as auxiliary means of quality assurance. Thestandard practice in industry is to write various test cases to reduce the occurrencesof bugs for their products; however the validation process is not only slow, but alsoincomplete.There is almost always a need for bug fx during a regular software evolutionprocess; and the typical case is that the patch is usually local to its error site, relativelysmall and rarely changes core program semantics. Based on this key insight, this paperpresents a new approach that combines the strengths of static analysis approaches anddynamic symbolic execution, with the beneft of being more scalable. The basic ideais to localize the scope of validation by performing static analysis that aggressivelyprune away irrelevant paths and statements; by instrumenting symbolic semantics anda program drivers, a standard dynamic symbolic execution engine performs exhaustivetesting and do the validation for the patch.Thispaperhasbuiltaworkingprototype, called SERAPH,ontopofopen-sourcedcompilerframeworkLLVMandsymbolicexecutionengineKLEEwiththehelpofSTPconstraint solver. During evaluation, for tens of patches we impartially selected fromGNU Coreutils programs, SERAPH successfully detects all the incorrect patches; inaddition, there is at most a great enhancement in performance compared to symbolicexecution against the whole program, with at most1000x speedup.