ACL2 Seminar, May 28, 2013

Codewalker -- Version 1
J Strother Moore

Abstract:

Codewalker is a ``meta de-compiler''.  It was designed to explore a piece of
machine code relative to a user-supplied operational semantics written in
ACL2.  In particular, codewalker takes a description of a state-transition
semantics and an initial state (which includes an initial integer program
counter and an initial memory containing the code to analyze) and attempts to
produce high-level abstract pseudocode (ACL2) that captures all the effects
of running the program.  

This cannot always be done in a way that produces an answer more
perspicacious than the code itself.  I content myself to do what I can and to
hope that this project leads to others that elaborate and improve the tool.
Indeed, I see Codewalker Version 1 merely as a prototype that establishes a
framework that allows (and will in fact require) us to develop many important
elaborations to render it practical for realistic models

Codewalker is designed to handle an arbitrary ``clocked, single-step,
pc-based state-transition'' semantics defined in ACL2.  That is, codewalker
assumes that there is an ACL2 representation of the machine state, that an
ACL2 step function defines the state transitions, that a numeric program
counter determines where the next instruction is, and that every analysis
will focus on determining the ``final'' state produced by repeated stepping
from some initial state -- where either we step until we reach some
particular (kind of) instruction (e.g., a RETURN) or until we have taken some
specified number of steps.

I illustrate codewalker with two simple examples, both operating on different
formalizations of the same simple model: the M1 model of the JVM presented in
two different formalization styles.  In both cases, I show the analysis of a
simple factorial code.  I conclude by discussing some limitations and future
work.