an intermediate representation listing showing a few dozen instructions with numeric identifiers assigned to them. at the end, a few green rows with a plus symbol are appended. in the middle, some of the rows are paired red and green with a minus and plus symbol. the listing looks like the output of diff

Notices where this attachment appears

1. Embed this notice
   ✧✦✶✷Catherine✷✶✦✧ (whitequark@mastodon.social)'s status on Saturday, 08-Feb-2025 22:21:40 JST ✧✦✶✷Catherine✷✶✦✧

   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?