一句话：将符号变量扩展到函数并集成程序合成来求解二阶约束，缓解符号执行的路径爆炸。
传统符号执行通过求解路径条件来系统探索程序路径，其中符号变量通常取值于数字、数组和字符串。本文提出带存在性二阶约束的符号执行，允许符号变量取值为解释受用户自定义语言限制的函数，从而将符号执行与程序合成相结合。该技术有两个目标：一是提供可应用于程序修复和库建模等多个领域的通用分析框架；二是缓解传统一阶符号执行在某些应用中的路径爆炸问题。为实现该技术，作者提出一种二阶约束求解方法，能够高效证明不可满足性，这对符号执行的性能至关重要。评估表明，该技术能够通过缓解路径爆炸来修复含循环的程序，并能从使用上下文中对不可用的库进行建模，从而支持针对这些库所写应用的分析。
Symbolic execution systematically explores program paths by solving path conditions --- formulas over symbolic variables. Typically, the symbolic variables range over numbers, arrays and strings. We introduce symbolic execution with existential second-order constraints --- an extension of traditional symbolic execution that allows symbolic variables to range over functions whose interpretations are restricted by a user-defined language. The aims of this new technique are twofold. First, it offers a general analysis framework that can be applied in multiple domains such as program repair and library modelling. Secondly, it addresses the path explosion problem of traditional first-order symbolic execution in certain applications. To realize this technique, we integrate symbolic execution with program synthesis. Specifically, we propose a method of second-order constraint solving that provides efficient proofs of unsatisfiability, which is critical for the performance of symbolic execution. Our evaluation shows that the proposed technique (1) helps to repair programs with loops by mitigating the path explosion, (2) can enable analysis of applications written against unavailable libraries by modelling these libraries from the usage context.
DOI 原文 ·
@inproceedings{paperbot4672,
title = {Symbolic execution with existential second-order constraints},
author = {Sergey Mechtaev and Alberto Griggio and Alessandro Cimatti and Abhik Roychoudhury},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3236049}
}