Context-Updates Analysis and Refinement in Chisel

TL;DR

This paper introduces a method for synthesizing program slicers from language semantics focusing on context-updates, using overapproximation and refinement phases tested on imperative and assembly languages.

Contribution

It presents a novel approach combining overapproximating and underapproximating phases for context-updates synthesis in program analysis.

Findings

Effective synthesis of context-updates for different language paradigms

Successful testing on avionics benchmarks

Improved accuracy in program slicing

Abstract

This paper presents the context-updates synthesis component of Chisel--a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics. (By context-updates we understand programming language constructs such as goto instructions or function calls.) The context-updates synthesis follows two directions: an overapproximating phase that extracts a set of potential context-update constructs and an underapproximating phase that refines the results of the first step by testing the behaviour of the context-updates constructs produced at the previous phase. We use two experimental semantics that cover two types of language paradigms: high-level imperative and low-level assembly languages and we conduct the tests on standard benchmarks used in avionics.