No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other.
No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other.
Ah, interesting. I went with Ghidra p-code which seems ok but what I didn't really appreciate going in was how much of the platform API surface you have to describe before you can prove pretty much anything at all.