Abstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
Karoliine Holter, Juhan-Oskar Hennoste,
Patrick Lam, and
2 more authors In New Ideas, New Paradigms, and Reflections on Programming and Software, 2024
To appear
Traditional, or concrete, debuggers allow developers to step through programs and explore the corresponding concrete program states—developers can query (and modify) current values of program variables. This exploration enables developers to formulate and refine hypotheses about program behaviors. We propose the novel notion of abstract debuggers, which allow developers to explore abstract program states, as computed by sound static analyzers. Giving developers the ability to interactively explore abstract states (which encompass the program’s potential concrete states) empowers them to work with hypotheses that are true for all program executions: they can examine and rule out false positives, or better understand a static analysis’s declaration that some code is indeed safe. Abstract debuggers’ interfaces, reminiscent of conventional debuggers, aim to make navigating and interpreting static analysis results more straightforward. We have formalized the concept, applied it by implementing a tool that leverages the static analyzer Goblint, and illustrate its usefulness through case studies.