Comments (15)
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.
Related Issues (20)
- Problematic copy of metadata in RemovePtrToIntPass HOT 3
- Question: sea-dsa does not produce memory graph when main function has internal linkage type. HOT 4
- Disable warning messages HOT 2
- Missing nodes for pointer variables HOT 3
- Upgrading to LLVM 11? HOT 12
- Dead link HOT 1
- Upgrade sea-dsa to support LLVM 12 HOT 1
- Selecting program entry point HOT 3
- How to query DsaInfo for Context Sentitive information HOT 6
- Combination of O3 and UBSan makes seadsa crash on input analysis HOT 2
- transfersNoPointers in DsaLocal mishandles opaque types
- Constructing paths from memory object to use-pointers HOT 1
- Question on realloc function. HOT 1
- Question about "function never returning" HOT 6
- Upgrade sea-dsa to support LLVM 13 HOT 1
- Upgrade sea-dsa to support LLVM 14 HOT 1
- README.md suggests to use `sudo pip` HOT 1
- Tea-dsa or sea-dsa? HOT 3
- CRASH: can't handle vectorTy in LoadInst / Gep
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from sea-dsa.