Static Analysis Under Non-Deterministic Program Assumptions

TL;DR

This paper introduces a static analysis method that incorporates user-supplied, location-specific assumptions to reduce imprecision, broadening the applicability of static analysis tools.

Contribution

It proposes a non-deterministic static analysis framework that uses local assumptions, enabling optimization over assumption spaces for improved analysis precision.

Findings

Enables broader application of static analysis with assumptions.

Demonstrates optimization over assumption search space.

Shows utility in two practical scenarios.

Abstract

Static analyses overwhelmingly trade precision for soundness and automation. For this reason, their use-cases are restricted to situations where imprecision isn't prohibitive. In this paper, we propose and specify a static analysis that accepts user-supplied program assumptions that are local to program locations. Such assumptions can be used to counteract imprecision in static analyses, enabling their use in a much wider variety of applications. These assumptions are taken by the analyzer non-deterministically, resulting in a function from sets of accepted assumptions to the resulting analysis under those assumptions. We also demonstrate the utility of such a function in two ways, both of which showcase how it can enable optimization over a search space of assumptions that is otherwise infeasible without the specified analysis.