An on-demand pointer analysis integrated with symbolic execution that is instantiated with an abstraction of the dynamic state on which it is invoked.
Overview
We propose a novel fine-grained integration of pointer analysis with dynamic analysis, including dynamic symbolic execution. This is achieved via past-sensitive pointer analysis, an on-demand pointer analysis instantiated with an abstraction of the dynamic state on which it is invoked. We evaluate our technique in three application scenarios: chopped symbolic execution, symbolic pointer resolution, and write integrity testing. Our preliminary results show that the approach can have a significant impact in these scenarios, by effectively improving the precision of standard pointer analysis with only a modest performance overhead.
Teaser
Artefact
The artefact page is available here.
Source code is available here.
Publications
-
Past-Sensitive Pointer Analysis for Symbolic Execution
David Trabish, Timotej Kapus, Noam Rinetzky, Cristian Cadar
European Software Engineering Conference / ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2020)