TracerX

Dynamic Symbolic Execution with Interpolation

TracerX: Dynamic Symbolic Execution with Interpolation

Our work concerns Symbolic Execution for program analysis. While there are now many practical Symbolic Execution systems, they all face the fundamental problem of path explosion, and only small programs can be comprehensively analyzed. We developed the algorithm of Abstraction Learning in 2009 link, which enabled a significant optimization of Symbolic Execution via the use of interpolation. This allows, for the first time, a systematic way to prune the search space of Symbolic Execution.

Our first research project developed the TRACER system in 2012 link. It was successfully used to perform analyses, particularly for quantitative analyses, at a new level of accuracy. However, TRACER’s engineering did not allow it to scale to large programs. Our current work is in developing the TracerX system.

Overview

TracerX is built on top of KLEE, with the main feature of abstraction learning. This method more popularly known as “lazy annotations” (McMillan 2010, McMillan 2014). The core feature is subsumption of paths whose traversals are deemed to no longer be necessary due to similarity with already-traversed paths. The technique first employs interpolation (Craig 1957) to abstract the already-traversed paths such that more paths later traversed can be subsumed. This abstraction is in principle non-lossy in the sense that if a bug is to be found by traversing the subsumed path, the bug should have been found in one of the already-traversed paths. Subsumptions can be expected to mitigate the traversal complexity of path enumeration, although in some instances we pay a higher price for extra constraint solver calls.

Abstraction learning has mainly been described for path enumeration performed in depth-first search. That is, the next path to be considered is the one from the “latest choicepoint”. This is too restrictive in a testing environment, where we are always able to perform full exploration. The work (Jaffar et al. 2013) introduced the notion of “half-interpolation” whereby paths can be enumerated in any order, but this time producing half-interpolants instead of traditional (full) interpolants. Eventually, when sufficient half-interpolants are constructed, full interpolants can be constructed. In TracerX, we present this idea in a more general form and call it fractional interpolation. That is, interpolants associated with fraction can be constructed, and such interpolants can be combined to produce new interpolants assoicated with a higher fraction. When an interpolant’s fraction becomes 1, it can then be used to subsume or prune other paths.

Example

For a list of examples running with TracerX visit here.

List of Publications & Presentations

For more information on what TracerX is and what it can do, see the following publications

  1. Arpita Dutta, Rasool Maghareh, Joxan Jaffar, Sangharatna Godboley, Xiao Liang Yu, “TracerX: Pruning Dynamic Symbolic Execution with Deletion and Weakest Precondition Interpolation” (Competition Contribution), In Int. Conf. on Fundamental Approaches to Software Engineering, (FASE’24), Luxembourg, 2024. [Link to Paper] [Zenodo]
  2. Arpita Dutta, Rasool Maghareh, Joxan Jaffar, “TracerX-Pruning Dynamic Symbolic Execution with Weakest Precondition Interpolation”, In 4th International KLEE Workshop on Symbolic Execution, Lisbon, 2024, [Co-located with ICSE’24] [Slides] [Poster]
  3. Sangharatna Godboley, Joxan Jaffar, Rasool Maghareh, Arpita Dutta, “Toward Optimal MC/DC Test Case Generation”, In 3rd International KLEE Workshop on Symbolic Execution, 2022, London, UK. [Slides]
  4. Sangharatna Godboley, Joxan Jaffar, Rasool Maghareh, Arpita Dutta, “Toward Optimal MC/DC Test Case Generation”, In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2021. [Link to Paper] [Zenodo]
  5. Test-comp 2021 slides for TracerX [Link]
  6. Joxan Jaffar, Rasool Maghareh, Sangharatna Godboley, and Xuan-Linh Ha. “TracerX: Dynamic Symbolic Execution with Interpolation”, arXiv:2012.00556v1, 2020. [Link]
  7. Joxan Jaffar, Rasool Maghareh, Sangharatna Godboley, and Xuan-Linh Ha. “TracerX: Dynamic Symbolic Execution with Interpolation (Competition Contribution).” In FASE, pp. 530-534. 2020. [Link]
  8. Joxan Jaffar, Rasool Maghareh. “The TRACER-X System”, KLEE Workshop, 2018. [Link]
  9. TracerX poster, National University of Singapore, 2020. [Link]

Installing TracerX

Wiki

For more information on the class diagrams for Klee (Version 1.0) and TracerX (TX), visit here.

Team Members

The project is led by Joxan Jaffar. Other team members are: Rasool Maghareh, Arpita Dutta, Sangharatna Godboley, Xuan-Linh Ha, Chew Wei Ze Alvin.