Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Possible Value Analysis based on Symbolic Lattice

Qi Zhan

TL;DR

This work tackles static reasoning about program behavior without executing code, proposing program behavior analysis that merges symbolic execution with abstract interpretation to derive possible symbolic expressions for every variable and memory cell at each program point. A novel symbolic lattice $\\mathcal{L}$ with a top element $\\top$ and a widening operator is designed to handle infinite-height constructs, and the analysis is formulated over a simple SSA-like language to support both intraprocedural and interprocedural analyses. Key contributions include the design of the infinite-height lattice interleaved with expressions, a depth-based widening scheme $\\nabla_i$, and a formal transfer-function framework that handles memory via a pointer-analysis component $\\Downarrow_{pa}$. The approach yields safe over-approximations of program behavior and enables comparisons of code semantics (e.g., code diffs) at the function and program level, with practical applicability to bug and vulnerability detection and program understanding; future work points to stronger pointer/control-flow analyses to improve precision and broader interprocedural handling.

Abstract

We propose a new static program analysis called program behavior analysis. The analysis aims to calculate possible symbolic expressions for every variable at each program point. We design a new lattice, transfer function, and widening operator to accommodate the analysis. Furthermore, we extend the analysis to interprocedural.

Possible Value Analysis based on Symbolic Lattice

TL;DR

This work tackles static reasoning about program behavior without executing code, proposing program behavior analysis that merges symbolic execution with abstract interpretation to derive possible symbolic expressions for every variable and memory cell at each program point. A novel symbolic lattice with a top element and a widening operator is designed to handle infinite-height constructs, and the analysis is formulated over a simple SSA-like language to support both intraprocedural and interprocedural analyses. Key contributions include the design of the infinite-height lattice interleaved with expressions, a depth-based widening scheme , and a formal transfer-function framework that handles memory via a pointer-analysis component . The approach yields safe over-approximations of program behavior and enables comparisons of code semantics (e.g., code diffs) at the function and program level, with practical applicability to bug and vulnerability detection and program understanding; future work points to stronger pointer/control-flow analyses to improve precision and broader interprocedural handling.

Abstract

We propose a new static program analysis called program behavior analysis. The analysis aims to calculate possible symbolic expressions for every variable at each program point. We design a new lattice, transfer function, and widening operator to accommodate the analysis. Furthermore, we extend the analysis to interprocedural.
Paper Structure (16 sections, 1 theorem, 6 equations, 6 figures, 1 table, 1 algorithm)

This paper contains 16 sections, 1 theorem, 6 equations, 6 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Possible Value Analysis
  3. Preliminary
  4. Overview
  5. Formalization
  6. Language.
  7. Lattice Design.
  8. Widening
  9. Abstract Domains.
  10. Join Operator
  11. Transfer Function
  12. Discussion
  13. Interprocedural Analysis
  14. Limitation
  15. Related Work
  16. ...and 1 more sections

Key Result

theorem 1

Suppose $\alpha$ is the function that represents the transfer function and join, $\llbracket f \rrbracket$ is the concrete semantic of the single function, and $\llbracket f \rrbracket^*$ is the abstract semantic of the function, Then we have

Figures (6)

  • Figure 1: A typical flow sensitive Andersen's algorithm
  • Figure 2: Syntax of language and lattice
  • Figure 3: Illustration of a subset of the lattice. For simplicity, we only consider the primitive $p$ and binary expressions and unop expressions. Function and phi expression can be added in a similar way. As the lattice is infinite height, we have to omit some elements, which are represented as a dashed line.
  • Figure 4: Partial order of lattice
  • Figure 5: Abstract domains
  • ...and 1 more figures

Theorems & Definitions (2)

  • definition 1: Possible Value Analysis
  • theorem 1: Soundness