Conversation

hey, compiler folks, check this out

in Project Unnamed we have a way to automatically verify transformations using an SMT solver. we do this by collecting calls to replace-all-uses-with in a staging area, checking it while using the before-after correspondence to make the SMT query more tractable, then applying in bulk

if the query fails, we print the design with diff markup, which gets highlighted like the below

the verifier will also tell you which RAUW calls were illegal

how cool is this?