Context-sensitive pointer analysis often generates excessive spurious points-to relations, causing inefficiency and imprecision. We introduce stack filtering, a novel approach using Rust’s stack object lifetime information to address this issue. It eliminates points-to relations involving variables pointing to inactive stack objects beyond their lifetimes. Stack filtering is a lightweight two-phase process. It first assesses stack object liveness using a call graph from Rapid Type Analysis (RTA). Then, this filtering is applied during the main pointer analysis. Evaluations on real-world Rust applications show that stack filtering enhances analysis efficiency, reducing time and memory consumption while improving precision. This makes it a vital tool for Rust’s program analysis and verification, given Rust’s reliance on automatic memory management and a preference for static stack allocation.

Tue 4 Mar

Displayed time zone: Pacific Time (US & Canada) change

10:00 - 11:00
Program Analysis & SynthesisMain Conference at Casuarina Ballroom (Level 2)
Chair(s): Jose Nelson Amaral University of Alberta
10:00
20m
Talk
Automatic Synthesis of Specialized Hash Functions
Main Conference
Renato B Hoffmann PUC-RS, Leonardo Gibrowski Faé PUC-RS, Dalvan Griebler Pontifícia Universidade Católica do Rio Grande do Sul - PUCRS, David Li Google, Fernando Magno Quintão Pereira Federal University of Minas Gerais
10:20
20m
Talk
Stack Filtering: Elevating Precision and Efficiency in Rust Pointer Analysis
Main Conference
Wei Li UNSW, Dongjie He Chongqing University, China, Wenguang Chen Tsinghua University; Pengcheng Laboratory, Jingling Xue UNSW Sydney
10:40
20m
Talk
SkipFlow: Improving the Precision of Points-to Analysis using Primitive Values and Predicate Edges
Main Conference
David Kozak Brno University of Technology & Oracle Labs, Christian Wimmer Amazon Web Services, Codrut Stancu Oracle Labs, Tomas Vojnar Masaryk University