Modular, compositional, and executable formal semantics for LLVM IR