Combining E-graphs with abstract interpretation
File(s)2203.09191v1.pdf (440.86 KB)
Accepted version
Author(s)
Coward, S
Constantinides, GA
Drane, T
Type
Conference Paper
Abstract
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.
Date Issued
2023-06-06
Date Acceptance
2023-04-25
ISBN
979-8-4007-0170-2
Publisher
ACM
Start Page
1
End Page
7
Journal / Book Title
SOAP 2023: Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis
Copyright Statement
© 2023 ACM. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in SOAP 2023: Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, Jun 2023. http://dx.doi.org/10.1145/3589250.3596144
Identifier
https://dl.acm.org/doi/pdf/10.1145/3589250
http://arxiv.org/abs/2203.09191v1
Source
State of the Art in Program Analysis (SOAP) 2023
Publication Status
Published
Start Date
2023-06-17
Finish Date
2023-06-17
Coverage Spatial
Orlando, Florida, USA
Date Publish Online
2023-06