Thu 19 Jan 2023 13:30 - 13:55 at Grand Ballroom A - Program Analysis & Parsing Chair(s): David Pichardie

Static single assignment (SSA) form is a popular intermediate representation that helps implement useful static analyses, including global value numbering (GVN), sparse dataflow analyses, or SMT-based abstract interpretation or model checking. However, the precision of the SSA translation itself depends on static analyses, and a priori static analysis is even indispensable in the case of low-level input languages like machine code.

To solve this chicken-and-egg problem, we propose to turn the SSA translation into a standard static analysis based on abstract interpretation. This allows the SSA translation to be combined with other static analyses in a single pass, taking advantage of the fact that it is more precise to combine analyses than applying passes in sequence.

We illustrate the practicality of these results by writing a simple dataflow analysis that performs SSA translation, optimistic global value numbering, sparse conditional constant propagation, and loop-invariant code motion in a single small pass; and by presenting a multi-language static analyzer for both C and machine code that uses the SSA abstract domain as its main intermediate representation.

Thu 19 Jan

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

13:30 - 14:45
Program Analysis & ParsingPOPL at Grand Ballroom A
Chair(s): David Pichardie Meta
SSA Translation Is an Abstract InterpretationDistinguished Paper
Matthieu Lemerre Université Paris-Saclay - CEA LIST
DOI Pre-print
Dynamic Race Detection with O(1) SamplesDistinguished Paper
Mosaad Al Thokair University of Illinois at Urbana-Champaign, Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur National University of Singapore, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
Statically Resolvable Ambiguity
Viktor Palmkvist KTH Royal Institute of Technology, Elias Castegren Uppsala University, Philipp Haller KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology