alive2
alive2 copied to clipboard
Add support for non-0 address spaces
define i32 @src(ptr addrspace(1) %ptr) {
%load = load i32, ptr addrspace(1) %ptr
ret i32 %load
}
define i32 @tgt(ptr addrspace(1) %ptr) {
%load = load i32, ptr addrspace(1) %ptr
ret i32 %load
}
ERROR: Could not translate 'src' to Alive IR
Seems to give up on any pointer value with a non-0 address space, no matter what you're doing with it. Care needs to be taken for null handling, but address spaces (except for non-integral address spaces) aren't total magic and should behave normally.
Currently the opt plugin has little practical use for AMDGPU since optimized IR has few addrspace(0) pointers. Manually fixing up tests to only use flat pointers is annoying and not a sustainable testing strategy.
Yep, only the default address space is supported ATM. There's no ETA for implementing this, sorry.
We needed non-0 address spaces, plus 256-bit pointers, so I started experimenting by simply changing the address space assertions to warnings, and raising the naked 64 limits. (Given the seriousness of misoptimization for financial applications, I was willing to tolerate a lot of false positives to find even a small number of bugs. Obviously I had to accept the possibility of false negatives for now.)
I couldn’t get tv.dylib
to work with our 17.0.6 fork, but the simple changes allowed some testing with the current alive-tv
on one of our LLVM IR tests, splitting the output from --print-after-all
with our fork, and testing the transitions. There were a manageable number of false positives, some of which were understandable; the apparently unjustified ones went away when I massaged the file with regexes to use only the default address space and 64-bit pointers. So far no more bugs found in our code.
Testing on the entire -O3
optimization for the LLVM IR generated from a sample smart contract currently asserts "cast<Ty>() argument of incompatible type" in hasNoSignedWrap
in llvm-project/llvm/include/llvm/IR/Instruction.h, called from llvm2alive.cpp:1753. My next step is to split up that optimization as well, and see whether any individual transition gives an unsoundness report which looks genuine.