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

Segmentation fault on a program #96

Closed shaobo-he closed 4 years ago

shaobo-he commented 4 years ago

Hello sea-dsa developers,

I encountered a segmentation fault when using the f7658f8feb6ec6c664730053e3a2636b8df6ff9a commit. I attached the file, the command to invoke it is `seadsa -sea-dsa=ci -sea-dsa-dot file.ll.

file.txt

caballa commented 4 years ago

The segfault occurs after commit 6034037.

agurfinkel commented 4 years ago

The instance has undefined behavior (load from a null pointer). So there is no guarantee of soundness. However, sea-dsa no longer crashes on it.

zvonimir commented 4 years ago

Thanks @agurfinkel! I have a quick follow-up question. How would one build e.g. a null pointer dereference checker on top of SeaDsa? The kinds of bugs that people are often really interested in in C programs are often undefined behaviors (buffer overflow, etc.). If SeaDsa does not guarantee soundness in the presence of any kind of undefined behaviors, then this might be a bit problematic. Or do you have some kind of a way for handing undefined behaviors gracefully? Thanks!

agurfinkel commented 4 years ago

TL;DR; unsound for the whole program, but sound until first undef behavior, so there is always a cex that goes through the sound part of the analysis.

Full story in this wonderful paper: http://theory.stanford.edu/~barrett/pubs/CDN+08-TR.pdf

Caveat: undefined behavior might be exploited by clang. Then the LLVM IR already unsound relative to expected semantics of the source.