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
13:30
25m
Talk
SSA Translation Is an Abstract InterpretationDistinguished Paper
POPL
Matthieu Lemerre Université Paris-Saclay - CEA LIST
DOI Pre-print
13:55
25m
Talk
Dynamic Race Detection with O(1) SamplesDistinguished Paper
POPL
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
14:20
25m
Talk
Statically Resolvable Ambiguity
POPL
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
DOI