Allen School Colloquium: PLSE Research Group

Presentation title: egg: e-graphs good with Max Willsey
Have you ever wanted to turn a program into a better program? Or maybe show that two programs are equal? One classic way to do these kinds of things is with term rewriting. But term rewriting suffers from a whole host of issues, all stemming from the fact that you have to make choices (I know, right?). What if you never had to make any choices? Instead, you could simultaneously consider all possible pasts and presents (future is future work) and thereby avoid committing yourself to anything at all. Sounds good right? We'll talk about e-graphs, data structures that (much like the elephant) never forget anything. Originally built for use in theorem provers, I’ll show you how we can repurpose them to do program optimization, synthesis, and verification in a really effective way. All of this stuff is packaged up in a library, egg, which is powering a lot of super cool work across a bunch of domains like machine learning, CAD, floating point, compilers, testing, and more.

Presentation title: Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations with Chandrakana Nandi
Recent program synthesis techniques help users customize 3D CAD models by decompiling low-level triangle meshes to Constructive Solid Geometry (CSG) expressions. However, without loops or functions, editing CSG can require many coordinated changes, and existing mesh decompilers often use heuristics that can obfuscate high-level structure. In this talk, I propose a second decompilation stage to robustly shrink unstructured CSG expressions into more editable programs with map and fold operators. I will present our tool, Szalinski, that uses Equality Saturation with semantics-preserving CAD rewrites to efficiently search for smaller equivalent programs. Szalinski relies on Inverse Transformations, a novel way for solvers to speculatively add equivalences to the E-graph data structure to mitigate the "AC-matching problem". I will show some results generated by Szalinski when it is composed with a mesh decompiler and also present a large-scale evaluation of Szalinski on thousands of real models from a popular online 3D model forum.

Presentation title: Verified Object Construction via Accumulation Analysis with Martin Kellogg
In object-oriented languages, constructors often have a combination of required and optional formal parameters. Rather than writing constructors for every possible combination of parameters, programmers often use design patterns that enable more flexible object construction, such as the builder pattern. However, the builder pattern can be too flexible: not all combinations of logical parameters lead to the construction of well-formed objects. When a client uses the builder pattern to construct an object, the compiler does not check that a valid set of values was provided. Incorrect use of builders can cause security vulnerabilities, run-time crashes, and other problems. This work shows how to statically verify uses of object construction, such as the builder pattern. Using a simple specification language, programmers specify which combinations of logical arguments are permitted. Our compile-time analysis detects client code that may construct objects unsafely. Our analysis is based on a special case of typestate checking that modularly reasons about accumulations of method calls. It scales to industrial programs. We evaluated it on over 9 million lines of code, discovering defects which include previously-unknown security vulnerabilities and potential null-pointer violations in heavily-used open-source codebases. It has a low false positive rate and low annotation burden.

Presentation title: Falx: Synthesis-powered data visualization with Chenglong Wang
Modern visualization tools aim to allow data analysts to easily create expressive visualizations. When the input data layout conforms to the visualization design, users can easily specify visualizations by mapping data columns to visual channels of the design. However, when there is a mismatch between data layout and the design, users need to spend significant effort on data transformation. We propose Falx, a synthesis-powered visualization tool, that allows users to specify expressive visualizations in a similarly simple way but without needing to worry about data layout. In Falx, users specify visualizations using examples of how concrete values in the input are mapped to visual channels, and Falx automatically infers the visualization specification and transforms the data to match the design. In a study with 33 data analysts on 4 visualization tasks involving data transformation, we found that users can effectively adopt Falx to create visualizations they can't implement.

[olivierfaure]

All three of these presentations are amazing. I feel like each of them just opens a new world of possibilities for compilers and developers and how they interact with their code.