Integrating String Reasoning in Symbolic Execution of C Programs
摘要
Symbolic execution is a powerful program analysis technique which explores new paths through a program by generating inputs that are guaranteed to exercise those paths. However, there is a lack of modern research on symbolic execution for programs that manipulate strings, especially for C programs. In this work, we develop an approach for symbolically executing string-manipulating C programs and implement it in a proof-of-concept tool called SymCC-str. SymCC-str is built on top of the concolic execution engine SymCC and the smt-switch SMT solving API, enabling it to make use of modern advancements in both symbolic execution and string solving. SymCC-str’s novelty lies in its hybrid data representation, expressing symbolic data both as SMT bitvectors and strings in order to balance the performance and expressivity of these respective theories. Through this novel approach, SymCC-str achieves a median 9.9% increase in branch coverage (up to 990% in the best case) compared to SymCC on 6 real-world benchmark programs.