A Flow-Insensitive-Complete Program Representation
When designing a static analysis, choosing between a flow-insensitive or a flow-sensitive analysis often amounts to favor scalability over precision. It is well known than specific program representations can help to reconcile the two objectives at the same time. For example the SSA representation is used in modern compilers to perform a constant propagation analysis flow-insensitively without any loss of precision.
This paper proposes a provably correct program transformation that reconciles them for any analysis. We formalize the notion of Flow-Insensitive-Completeness with two collecting semantics and provide a program transformation that permits to analyze a program in a flow insensitive manner without sacrificing the precision we could obtain with a flow sensitive approach.
Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 11:50
Static Analysis and Abstract InterpretationVMCAI at Salon I
Chair(s): Thomas Wies New York University
|Relational String Abstract DomainsRemote|
Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences, Martina Olliaro Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics, Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy
|Lightweight Shape Analysis based on Physical TypesInPerson|
Olivier Nicole CEA LIST, France, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris
|A Flow-Insensitive-Complete Program RepresentationRemote|
Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Facebook Paris