search

seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

add flag to enable asserts in release mode (SEA_ENABLE_ASSERTIONS) #131

Closed pietroborrello closed 3 years ago

pietroborrello commented 3 years ago

Enable asserts with any CMAKE_BUILD_TYPE adding -DSEA_ENABLE_ASSERTIONS:BOOL=ON

agurfinkel commented 3 years ago

By default, sea-dsa uses the same compilation flags as LLVM that it is compiled against. What is the reason for enabling assertions only in sea-dsa and not in LLVM? Since NDEBUG flag is undefined, this will cause potential problems when linking against release version of LLVM libraries. For example, the Value::dump method is not defined in non-debug builds and will cause linking errors.

pietroborrello commented 3 years ago

I found it useful to debug seadsa when integrating it in out-of-tree passes that do not require compiling llvm, especially in debug mode which is resource and time consuming. Building only seadsa is much more quick, and exposing a way to enable assertions here allows to debug seadsa bugs in a nicer way. I'm actually linking with a release version of llvm (obtained from https://apt.llvm.org/llvm.sh), and see no errors. However I understand if you see it just as a limited use case, feel free to close this.

agurfinkel commented 3 years ago

If you find this useful, we can keep it, as long as you add lots of warnings and make it difficult to turn this option on (for example, by adding EXPERIMENTAL flag that has to be on for the option to be available).

In the past, I've spent many hours debugging strange problems due to my code being compiled under debug and LLVM code being compiled in release. The problem is that everything works fine until it does not. At least in the past, there were structs that have extra fields in debug mode. Thus, their layout is different between debug and release mode. If your code happens to access affected fields it is a mess to debug.

pietroborrello commented 3 years ago

Ok thank you for the feedback, I was not aware of such problems, and do not want to introduce any potential problem to the build system. I find it useful, but honestly, such bugs sound way scarier. Probably the best thing is to close this and avoid merging, to prevent people from using potentially unsafe versions of seadsa.

I'll just manually add it when needed since should be safe to toggle it just for specific tasks, but I agree that anyone that wants asserts to be enabled, should just go the hard way and compile the right version of llvm.

agurfinkel commented 3 years ago

Here is a concrete example: https://github.com/llvm/llvm-project/blob/release/10.x/llvm/include/llvm/IR/ValueHandle.h#L256

Looks like this has been fixed in new versions though.

pietroborrello commented 3 years ago

Oh wow, would have never expected something so cursed like literally changing class hierarchy based on a debug flag. Thanks for the clarification :)