lean-llvm
lean-llvm copied to clipboard
feat: make opcode tags less brittle, work with more LLVM versions
LLVM opcodes use unsigned integer tags to identify them (see llvm/IR/Instruction.def in LLVM's source), but unfortunately these can change between LLVM versions. Instead of having lean-llvm rely on these tags and try to match the Lean implementation's tags for the equivalent Lean type (i.e., LLVM.Code.Instr) we now have the instruction emit its opcode name and parse that. These names appear stable across LLVM versions and thus things won't unexplicably break if LLVM introduces a new constructor.