Hal: A Language-General Framework for Analysis of User-Specified Monotone Frameworks [DRAFT]

TL;DR

This paper introduces a language-agnostic, user-driven framework for dataflow analysis that minimizes user input while automatically inferring analysis details, enabling flexible and general analysis across different programming languages.

Contribution

It presents the theoretical and practical design of a universal framework for dataflow analysis that requires minimal user input and is applicable to multiple programming languages.

Findings

Framework successfully infers analysis details with minimal user input

Implemented in Java for practical use

Applicable to both intraprocedural and interprocedural analyses

Abstract

Writing dataflow analyzers requires both language and domain-specificity. That is to say, each programming language and each program property requires its own analyzer. To enable a streamlined, user-driven approach to dataflow analyzers, we introduce the theoretical framework for a user-specified dataflow analysis. This framework is constructed in such a way that the user has to specify as little as possible, while the analyzer infers and computes everything else, including interprocedural embellishments. This theoretical framework was also implemented in Java, where users can specify a program property alongside minimal extra information to induce a dataflow analysis. This framework (both theoretical and in implementation) is language-general, meaning that it is independent of syntax and semantics (as all necessary syntactic and semantic information is provided by the user, and this information is provided only once for a given language). In this paper, we introduce basic notions of intraprocedural and interprocedural dataflow analyses, the proposed "Implicit Monotone Framework," and a rigorous framework for partial functions as a property space.