From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation

TL;DR

This paper explores translating imperative programs between big-step and small-step semantics using constrained Horn clauses and interpreter specialization, enabling flexible semantic representations and program analysis.

Contribution

It introduces a method to convert between big-step and small-step semantics via interpreter specialization and program transformation, demonstrating this on a subset of C.

Findings

Successful translation between big-step and small-step semantics

Use of partial evaluation to optimize and clarify program representations

Application of Tarjan's algorithm for path computation in program analysis

Abstract

We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as constrained Horn clause programs directly encoding the rules. We then specialise an interpreter with respect to a given source program to achieve a compilation of the source language to Horn clauses (an instance of the first Futamura projection). The process is described in detail for an interpreter for a subset of C, directly encoding the rules of big-step operational semantics for C. A similar translation based on small-step semantics could be carried out, but we show an approach to obtaining a small-step representation using a linear interpreter for big-step Horn clauses. This interpreter is again specialised to achieve the translation from big-step to small-step style. The linear small-step program can be transformed back to a big-step non-linear program using a third interpreter. A regular path expression is computed for the linear program using Tarjan's algorithm, and this regular expression then guides an interpreter to compute a program path. The transformation is realised by specialisation of the path interpreter. In all of the transformation phases, we use an established partial evaluator and exploit standard logic program transformation to remove redundant data structures and arguments in predicates and rename predicates to make clear their link to statements in the original source program.