POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 11:41 - 12:03 at Sala II - Abstract Interpretation Chair(s): David Naumann

Algebraic program analyses compute information about a program’s behavior by first (a) computing a valid path expression—i.e., a regular expression that recognizes all feasible execution paths (and usually more)—and then (b) interpreting the path expression in a semantic algebra that defines the analysis. There are an infinite number of different regular expressions that qualify as valid path expressions, which raises the question “Which ones should we choose?” While any choice yields a sound result, for many analyses the choice can have a drastic effect on the precision of the results obtained. This paper investigates the following two questions: (1) What does it mean for one valid path expression to be “better” than another? (2) Can we compute a valid path expression that is “best,” and if so, how? We show that it is not satisfactory to compare two path expressions $E_1$ and $E_2$ solely by means of the languages that they generate. Counter to one’s intuition, it is possible for $L(E_2) \subsetneq L(E_1)$, yet for $E_2$ to produce a less-precise analysis result than $E_1$—and thus we would not want to perform the transformation $E_1 \rightarrow E_2$. However, the exclusion of paths so as to analyze a smaller language of paths is exactly the refinement criterion used by some prior methods.

In this paper, we develop an algorithm that takes as input a valid path expression $E$, and returns a valid path expression $E’$ that is guaranteed to yield analysis results that are at least as good as those obtained using $E$. While the algorithm sometimes returns $E$ itself, it typically does not: (i) we prove a a no-degradation result for the algorithm’s base case—for transforming a leaf loop (i.e., a most-deeply-nested loop); (ii) at a non-leaf loop $L$, the algorithm treats each loop $L’$ in the body of $L$ as an indivisible atom, and applies the leaf-loop algorithm to $L$; the no-degradation result carries over to (ii) as well. Our experiments show that the technique has a substantial impact: the loop-refinement algorithm allows the implementation of Compositional Recurrence Analysis to prove over 25% more assertions for a collection of challenging loop micro-benchmarks.

The algorithm can be used to improve the precision of essentially any algebraic program analysis. Moreover, thanks to recent work that extends algebraic program analysis to interprocedural problems, our approach also applies to programs with recursive procedure calls (albeit this feature is not yet supported in our implementation).

 Refinement of Path Expressions for Static Analysis (Refinement of Path Expressions.pptx) 1.16MiB

#### Fri 18 JanDisplayed time zone: Belfast change

 10:35 - 12:03 Abstract InterpretationResearch Papers at Sala II Chair(s): David Naumann Stevens Institute of Technology 10:3522mTalk A^2 I: Abstract^2 InterpretationDistinguished PaperResearch PapersPatrick Cousot , Roberto Giacobazzi University of Verona and IMDEA Software Institute, Francesco Ranzato University of Padova Link to publication DOI Media Attached File Attached 10:5722mTalk Concerto: A Framework for Combined Concrete and Abstract InterpretationResearch PapersJohn Toman University of Washington, Seattle, Dan Grossman University of Washington Link to publication DOI Media Attached 11:1922mTalk Skeletal Semantics and their InterpretationsResearch PapersMartin Bodin Imperial College London, Philippa Gardner Imperial College London, Thomas P. Jensen INRIA Rennes, Alan Schmitt Inria Link to publication DOI Pre-print Media Attached File Attached 11:4122mTalk Refinement of Path Expressions for Static AnalysisResearch PapersJohn Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Link to publication DOI Media Attached File Attached