Null graph node in context insensitive analysis about sea-dsa HOT 15 CLOSED

In general, we assume that programs do not have undef values. We treat structure values as though they are in memory (because they can contain pointers, like in your example). So this will require handling undef pointers.

The current solution is to crash (ouch). Alternative is to fix this to bail out and give no result, or a result with no guarantees.

If this is useful, I'll try to see what we can do to patch the crash.

Is there some deep reason why you need alias analysis in the presence of undefined pointer values? In other projects, we have a pass to simply rewrite them all to zero (or null).

from sea-dsa.

Hi @keram88, did we introduce the undefined value or it's simply emitted by the compiler frontends?

from sea-dsa.

Thanks for the response @agurfinkel. I don't think this is urgent given that for my use, these could be safely transformed into null values. One thing I didn't make clear earlier is that the undef pointer is never used, which may mean this specific program may not be problematic.

@shaobo-he This undef is emitted by the compiler front end.

from sea-dsa.

@agurfinkel Thanks for your response. I am catching up with emails after CAV deadline.

So this code comes from Rust. We are not sure why the Rust compiler does this, it seems to be maybe an optimization or something like that. However, it is important to note that this undef value never gets used, and so the program itself does not have undefined behaviors. Is this maybe a special case that you could handle without crashing? Since ultimately it does not lead to undefined behavior.

If not, then we'll look into rewriting them into null. Do you maybe have this pass you mentioned handy?

Thanks!

from sea-dsa.

sea-dsa is flow insensitive, so if it sees an undef value it assumes it might be used. The cleanest solution from my perspective is to have a pass that cleans this up. I know that LLVM tends to generate this kind of code (struct values are initialized with undef instead of zero). I'm not sure why that's a common pattern.

@caballa do you remember whether we have a pass to deal with this?

from sea-dsa.

yeah flow-insensitivity is the limitation for us. Everything is potentially reachable.
I don't think we have. We have a pass in SeaHorn that replaces some undef values with functions that return non-deterministic values (https://github.com/seahorn/seahorn/blob/dev10/lib/Transforms/Instrumentation/NondetInit.cc). However, this pass doesn't go inside structs or vector operations (which is another source of undef values). We could replace all undef with zero or null pointers

from sea-dsa.

Yes, for struct values, replacing with zero is the way to go. The meaning here is not uninitialized, but rather irrelevant. Even LLVM IR documentation has this pattern. I don't really see why it is a good idea to insert undef values in perfectly defined code, but that's how it is.

from sea-dsa.

Coming back to this. Is it possible that replacing undef with null everywhere could lead to soundess issues with SeaDSA? I would guess not, but I still wanted to double-check this.
Like is there a situation where replacing undef with null leads to less possible behaviors, which then in turn leads to unsound results being returned by SeaDSA (in terms of the original program that had undef)?
Thanks!

from sea-dsa.

@caballa I just looked at the NondetInit.cc pass you suggested. To me this seems like a better solution than replacing undef with null. Do you run this pass always when you run SeaDSA?
If you do, then to me it seems maybe we should simply extend it to handle @keram88's special case as well.
No?
We can work towards implementing this patch. It shouldn't be too hard to do it. Thanks!

from sea-dsa.

@zvonimir no, undef is not actually used, so replacing is with null makes no difference. Maybe we can just fix the segfault and treat undef in a struct as noop...

from sea-dsa.

@zvonimir how do I reproduce the issue, I do not get a crash using seadsa FILE.ll --sea-dsa-dot --sea-dsa=cs

from sea-dsa.

@agurfinkel Sorry if my earlier report was confusing. The crash arises in the 'SeaHorn Dsa analysis: entry point for all clients' pass. The segfault can be seen in seadsa FILE.ll --sea-dsa-viewer. Generating the call graph has always worked.

I tracked it down to a null node associated with the undef returning function during the bottom-up inlining phase of the analysis. I wasn't sure if this was unintended behavior or not.

from sea-dsa.

Hey @agurfinkel. So this is blocking us a little bit at this point. We started working on a pass to patch it on our end, but long term it would be great if this would get fixed in SeaDSA. Any plans to do it any time soon? We'll plan accordingly. Thanks!

from sea-dsa.

Oh, and if @keram88 wasn't really clear about this, we are mostly interested in this piece of code (commented out in his original example), which is what gets to SeaDSA in the end:

; As transformed by tool
; define internal { i8*, i8* } @fun(i8* %0) {
;   %2 = alloca { i8*, i8* }
;   %3 = getelementptr { i8*, i8* }, { i8*, i8* }* %2, i32 0, i32 0
;   store i8* null, i8** %3
;   %4 = getelementptr { i8*, i8* }, { i8*, i8* }* %2, i32 0, i32 1
;   store i8* undef, i8** %4
;   %5 = getelementptr { i8*, i8* }, { i8*, i8* }* %2, i32 0, i32 0
;   %6 = load i8*, i8** %5
;   %7 = insertvalue { i8*, i8* } undef, i8* %6, 0
;   %8 = getelementptr { i8*, i8* }, { i8*, i8* }* %2, i32 0, i32 1
;   %9 = load i8*, i8** %8
;   %10 = insertvalue { i8*, i8* } %7, i8* %9, 1
;   ret { i8*, i8* } %10
; }

We have passes that first translate what Mark called Original function into this piece of code, which then reaches SeaDSA. I hope this clarifies it.

from sea-dsa.

@zvonimir sorry for the delay. The original bug still does not reproduce for me. But, your comment made me look at the commented code. This code does cause a crash. The source is this instruction:

store i8* undef, i8** %4

No clue what the semantics of storing an undef pointer is. I've fixed the code to not crash and ignore the store.
This is unsound if the stored value is later read and dereferenced. There is a warning to that effect.

from sea-dsa.