Combining E-Graphs with Abstract Interpretation
E-graphs are a data structure that compactly represents equivalent expressions. They are constructed via the repeated application of rewrite rules. Often in practical applications, conditional rewrite rules are crucial, but their application requires the detection – at the time the e-graph is being built – that a condition is valid in the domain of application. Detecting condition validity amounts to proving a property of the program. Abstract interpretation is a general method to learn such properties, traditionally used in static analysis tools. We demonstrate that abstract interpretation and e-graph analysis naturally reinforce each other through a tight integration because (i) the e-graph clustering of equivalent expressions induces natural precision refinement of abstractions and (ii) precise abstractions allow the application of deeper rewrite rules (and hence potentially even greater precision). We develop the theory behind this intuition and present an exemplar interval arithmetic implementation, which we apply to the FPBench suite.
Sat 17 JunDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 11:00 | SOAP: Session 1 - Static AnalysisSOAP at Magnolia 18 Chair(s): Vincenzo Arceri University of Parma, Italy | ||
09:00 30mTalk | Combining E-Graphs with Abstract Interpretation SOAP Samuel Coward Imperial College London, UK / Intel Corporation, George A. Constantinides Imperial College London, UK, Theo Drane Intel Corporation, USA DOI | ||
09:30 30mTalk | Static Analysis of Data Transformations in Jupyter Notebooks (Virtual) SOAP Luca Negrini Ca’ Foscari University of Venice, Corvallis S.r.l., Guruprerana Shabadi École Polytechnique, Institut Polytechnique de Paris, Caterina Urban Inria & École Normale Supérieure | Université PSL DOI | ||
10:00 30mTalk | Speeding up Static Analysis with the Split Operator SOAP Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, Italy DOI | ||
10:30 30mTalk | When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in C SOAP Michael Schwarz Technische Universität München, Julian Erhard Technical University of Munich, Vesal Vojdani University of Tartu, Simmo Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München DOI Media Attached |