一句话：提出加权自动机模型对字符串约束解计数，保持与输入字符串值的一一对应，修正传统自动机模型的计数错误。
概率符号执行通过路径约束解计数来计算路径执行概率，其正确性取决于计数方法以及路径约束与程序输入值是否一一对应。已有字符串域工作主要关注基于自动机的字符串模型的高效精确计数，却未考察自动机编码的字符串与输入字符串值是否保持一一对应。本文证明传统基于自动机的字符串模型会破坏这种一一对应关系，并提出加权自动机模型，使路径约束编码与输入字符串值保持一一对应。作者基于该模型实现字符串约束求解器，在非平凡合成基准上验证正确性，并在真实字符串约束上比较传统与加权自动机求解器。评估表明，加权自动机模型虽效率较低，但能维持正确的解计数。
As an important extension of symbolic execution (SE), probabilistic symbolic execution (PSE) computes execution probabilities of program paths. Using this information, PSE can prioritize path exploration strategies. To calculate the probability of a path PSE relies on solution counting approaches for the path constraint. The correctness of a solution counting approach depends on the methodology used to count solutions and whether a path constraint maintains a one-to-one relation with program input values. This work focuses on the latter aspect of the solution counting correctness for string constraints. In general, maintaining a one-to-one relation is not always possible, especially in the presence of non-linear constraints. To deal with this issue, researchers that work on PSE for numerical domains either analyze programs with linear constraints, or develop novel techniques to handle solution counting of non-linear constraints. For the string domain, however, previous work on PSE mainly focuses on efficient and accurate solution counting for automata-based string models and has not investigated whether a one-to-one relationship between the strings encoded by automata and input string values is preserved. In this work we demonstrate that traditional automata-based string models fail to maintain one-to-one relations and propose to use the weighted automata model, which preserves the one-to-one relation between the path constraint it encodes and the input string values. We use this model to implement a string constraint solver and show its correctness on a set of non-trivial synthetic benchmarks. We also present an empirical evaluation of traditional and proposed automata solvers on real-world string constraints. The evaluations show that while being less efficient than traditional automata models, the weighted automata model maintains correct solution counts.
DOI 原文 ·
@inproceedings{paperbot5301,
title = {Accurate String Constraints Solution Counting with Weighted Automata},
author = {Elena Sherman and Andrew Harris},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00049}
}