Function extraction

AbstractLow-level imperative programming languages typically have complex operational semantics (e.g. derived from an underlying processor architecture). In this paper, we describe an automatic method for extracting recursive functions from such low-level programs. The functions are derived by formal deduction from the semantics of the programming language. For each function extracted, a proof of correspondence to the original program is automatically constructed. Subsequent program verification can then be done without referring to the details of the low-level programming language semantics at all: it suffices to prove properties of the extracted function. The technique is explained for simple while programs and also for the machine code of a widely used processor. We show how heuristics can enhance the output from the function extractor/decompiler and how the technique aids implementation of a trustworthy compiler. Our tools have been implemented in the HOL4 theorem prover