lean-mlir
lean-mlir copied to clipboard
chore: mark div/rem instructions as .impure, with Id monad
This lets us say the following:
We accurately model all semantics in LLVM. For operations that are side-effectful (divisions and remainders), we mark them as such in our framework, which ensures that the peephole rewrite never rewrites such operations. We choose the side effecting monad to be $Id$, thereby effectively freezing undefined behaviour into poison, which is a safe semantic refinement to do.