2006 | OriginalPaper | Chapter
Existential Label Flow Inference Via CFL Reachability
Authors : Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks
Published in: Static Analysis
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In programming languages, existential quantification is useful for describing relationships among members of a structured type. For example, we may have a list in which there
exists
some mutual exclusion lock
l
in each list element such that
l
protects the data stored in that element. With this information, a static analysis can reason about the relationship between locks and locations in the list even when the precise identity of the lock and/or location is unknown. To facilitate the construction of such static analyses, this paper presents a context-sensitive
label flow analysis
algorithm with support for existential quantification. Label flow analysis is a core part of many static analysis systems. Following Rehof et al, we use context-free language (CFL) reachability to develop an efficient
O
(
n
3
) label flow inference algorithm. We prove the algorithm sound by reducing its derivations to those in a system based on polymorphically-constrained types, in the style of Mossin. We have implemented a variant of our analysis as part of a data race detection tool for C programs.