Symbolic Computation via Program Transformation

TL;DR

This paper introduces a compiler-based transformation technique that converts standard programs into semantically equivalent programs capable of symbolic computation, simplifying symbolic analysis and verification tasks.

Contribution

It presents a practical, compiler-driven approach to enable symbolic computation within standard programs, bypassing the need for specialized symbolic interpreters.

Findings

Transformation is feasible and practical at the LLVM bitcode level.

Transformed programs support symbolic computation without external symbolic tools.

Experimental evaluation demonstrates effectiveness in symbolic verification tasks.

Abstract

Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead. Using compiler tooling, we propose and implement a transformation which takes a standard program and outputs a program that performs semantically equivalent, but partially symbolic, computation. The transformed program maintains symbolic values internally and operates directly on them hence the program can be processed by a tool without support for symbolic manipulation. The main motivation for the transformation is in symbolic verification, but there are many other possible use-cases, including test generation and concolic testing. Moreover using the transformation simplifies tools, since the symbolic computation is handled by the program directly. We have implemented the transformation at the level of LLVM bitcode. The paper includes an experimental evaluation, based on an explicit-state software model checker as a verification backend.