lean-llvm icon indicating copy to clipboard operation
lean-llvm copied to clipboard

feat: make opcode tags less brittle, work with more LLVM versions

Open pnwamk opened this issue 3 years ago • 0 comments

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.

pnwamk avatar Sep 09 '21 22:09 pnwamk