Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Static Analysis Under Non-Deterministic Program Assumptions

Abdullah H. Rasheed

TL;DR

The paper tackles imprecision in static analyses by introducing a parameterized framework that allows user-supplied, location-specific assumptions to be treated nondeterministically. It defines a parameterized domain $Par(\Sigma)$ and an Injective Normal Form (INF) to maintain a unique, compact representation of assumption-driven states, along with non-deterministic splitting via $splitPair$ and a one-pass analysis function $F: 2^\mathcal{A} \to \Sigma^n$ that preserves a strong correspondence with the unparameterized analysis. A correctness theorem shows that the parameterized analysis matches the standard analysis under any assumption set, and the approach extends to sound abstract interpreters. For scalability, the method introduces Approximate Merging as a tunable precision-loss mechanism and demonstrates the framework for assumption synthesis to satisfy asserts and for pruning inconsistent assumption sets, tying into lifted analyses, trace partitioning, and assumption-based AG reasoning. Overall, the work provides a principled, semantically grounded path to optimize over assumption spaces in static analysis while preserving soundness and enabling practical use in synthesis and verification tasks.

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.

Static Analysis Under Non-Deterministic Program Assumptions

TL;DR

The paper tackles imprecision in static analyses by introducing a parameterized framework that allows user-supplied, location-specific assumptions to be treated nondeterministically. It defines a parameterized domain and an Injective Normal Form (INF) to maintain a unique, compact representation of assumption-driven states, along with non-deterministic splitting via and a one-pass analysis function that preserves a strong correspondence with the unparameterized analysis. A correctness theorem shows that the parameterized analysis matches the standard analysis under any assumption set, and the approach extends to sound abstract interpreters. For scalability, the method introduces Approximate Merging as a tunable precision-loss mechanism and demonstrates the framework for assumption synthesis to satisfy asserts and for pruning inconsistent assumption sets, tying into lifted analyses, trace partitioning, and assumption-based AG reasoning. Overall, the work provides a principled, semantically grounded path to optimize over assumption spaces in static analysis while preserving soundness and enabling practical use in synthesis and verification tasks.

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.
Paper Structure (18 sections, 8 theorems, 32 equations, 1 figure, 1 algorithm)

This paper contains 18 sections, 8 theorems, 32 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Program Assumptions
  4. Parameterized Analysis
  5. Parameterized Abstract Domain
  6. Injective Normal Form
  7. Analysis Constraint Functions
  8. Correctness
  9. Remark.
  10. Soundness with Abstract Interpreters
  11. Approximate Merging
  12. Approximate Merging.
  13. Additional Remarks.
  14. Assumption Synthesis
  15. Remarks.
  16. ...and 3 more sections

Key Result

Lemma 2

Applying Exact Merging and Redundancy Elimination to any finite $X \in Par(\Sigma)$ to a fixed point results in a state $\hat{X} \in Par(\Sigma)$ such that $\hat{X}$ is in INF and $\hat{X} \sim X$.

Figures (1)

  • Figure 1: Sample program and its corresponding CFG.

Theorems & Definitions (16)

  • Definition 1: Injective Normal Form (INF)
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • Corollary 4
  • Lemma 5
  • proof
  • Theorem 6
  • proof
  • ...and 6 more