kirancodes.me
To Proof Maintenance & Beyond!

TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis

Junghee Lim, Thomas W. Reps

Abstract

This article describes the design and implementation of a system, called T SL (for Transformer Specification Language), that provides a systematic solution to the problem of creating retargetable tools for analyzing machine code. T SL is a tool generator---that is, a metatool---that automatically creates different abstract interpreters for machine-code instruction sets. The most challenging technical issue that we faced in designing T SL was how to automate the generation of the set of abstract transformers for a given abstract interpretation of a given instruction set. From a description of the concrete operational semantics of an instruction set, together with the datatypes and operations that define an abstract domain, T SL automatically creates the set of abstract transformers for the instructions of the instruction set. T SL advances the state-of-the-art in program analysis because it provides two dimensions of parameterizability: (i) a given analysis component can be retargeted to different instruction sets; (ii) multiple analysis components can be created automatically from a single specification of the concrete operational semantics of the language to be analyzed. T SL is an abstract-transformer-generator generator . The article describes the principles behind T SL , and discusses how one uses T SL to develop different abstract interpreters.

Related papers