Using the Executable Semantics for CFG Extraction and Unfolding
Abstract
The longest path search problem is important in low-level worst-case execution time analysis and implies that all program executions are exhibited and inspected, via convenient abstractions, for their timing behavior. In this paper we present a definitional program unfolded that is based on the formal executable semantics of a target language. We work with K, a rewrite-based framework for the design and analysis of programming languages. Our methodology has two phases. First, it extracts directly from the executable semantics of the language, via reach ability analysis, a safe control-flow graph (CFG) approximation. Second, it unfolds the control-flow graph, using loop bounds annotations and outputs the set of all possible program executions. The two-phased definitional program un folder is implemented using the K-Maude tool, a prototype implementation of the K framework.
Related Papers
- → Extracting safe and precise control flow from binaries(2002)119 cited
- → Detecting Exception Handling Bugs in C++ Programs(2023)7 cited
- → Using the Executable Semantics for CFG Extraction and Unfolding(2011)
- Control Flow Analysis Based on Intermediate Representation of Executable Code(2010)
- Executable program structural representation tool based on flow analysis(2007)