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

Crashes on SV-COMP benchmarks #66

Closed shaobo-he closed 4 years ago

shaobo-he commented 4 years ago

Hello sea-dsa developers,

I'm testing our sea-dsa integration on SV-COMP benchmarks and encountered some crashes. I'll list them gradually in this issue.

To reproduce these crashes, please run,

seadsa -sea-dsa=ci -sea-dsa-type-aware -sea-dsa-dot <.ll file>
  1. Cell not found for gep

This crash manifests on the following .ll file. https://drive.google.com/open?id=1Xqi8l9ZmekSPqSUfvPTNCHlBYXRgl4B0

The output is as follows,

WARNING: inttoptr @ addr 0x55f1b5d8ea68 is allocating a new cell.
Sea-Dsa type aware!
WARNING: inttoptr @ addr 0x55f1b5dd42f8 is allocating a new cell.
Cell not found for gep:   %369 = getelementptr inbounds [100 x %struct._TRACK_DATA], [100 x %struct._TRACK_DATA]* getelementptr inbounds (%struct._CDROM_TOC, %struct._CDROM_TOC* null, i32 0, i32 3), i32 0, i32 %368, !dbg !3203
        in CdAudioNECDeviceControl

    ptr: [100 x %struct._TRACK_DATA]* getelementptr inbounds (%struct._CDROM_TOC, %struct._CDROM_TOC* null, i32 0, i32 3)No cell for gep'd ptr
UNREACHABLE executed at /mnt/local/smack-project/smack/sea-dsa/src/DsaLocal.cc:708!
/usr/lib/llvm-8/lib/libLLVM-8.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamE+0x1f)[0x7f363d2ac59f]
/usr/lib/llvm-8/lib/libLLVM-8.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x7f363d2aa9c2]
/usr/lib/llvm-8/lib/libLLVM-8.so.1(+0x9719a8)[0x7f363d2ac9a8]
/lib/x86_64-linux-gnu/libc.so.6(+0x3ef20)[0x7f363bc49f20]
/lib/x86_64-linux-gnu/libc.so.6(gsignal+0xc7)[0x7f363bc49e97]
/lib/x86_64-linux-gnu/libc.so.6(abort+0x141)[0x7f363bc4b801]
/usr/lib/llvm-8/lib/libLLVM-8.so.1(+0x8e04b1)[0x7f363d21b4b1]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xd93a2)[0x55f1b4e393a2]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xd9b8b)[0x55f1b4e39b8b]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xeb275)[0x55f1b4e4b275]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xe8333)[0x55f1b4e48333]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xe53af)[0x55f1b4e453af]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xe1b00)[0x55f1b4e41b00]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xde3ba)[0x55f1b4e3e3ba]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xf3422)[0x55f1b4e53422]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0x251c5)[0x55f1b4d851c5]
/usr/lib/llvm-8/lib/libLLVM-8.so.1(_ZN4llvm6legacy15PassManagerImpl3runERNS_6ModuleE+0x2ee)[0x7f363d39fcae]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0x177e8)[0x55f1b4d777e8]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7)[0x7f363bc2cb97]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0x14b0a)[0x55f1b4d74b0a]
Stack dump:
0.  Program arguments: smack-project/smack/sea-dsa/build/run/bin/seadsa -sea-dsa=ci -sea-dsa-type-aware -sea-dsa-dot cdaudio.i.cil-1.ll 
1.  Running pass 'SeaHorn Dsa analysis: entry point for all clients' on module 'cdaudio.i.cil-1.ll'.
Aborted
caballa commented 4 years ago

This is a well known issue. When we analyze GEP instructions we require to have already a cell for the pointer operand, otherwise something went wrong. In SVCOMP, there are many cases where there is some GEP instruction for which the pointer operand is NULL. Not sure if this undefined behavior but it's for sure if the result of GEP is used to load or store.

We have currently some defensive assertions in the code to make sure that GEP's pointer operands have already a cell assigned to, and then we check for code patterns that we have seen in SVCOMP to skip the code assertion. In this case the pointer operand looks a constant expression which is another GEP. Probably we don't check for that case but it's easy to do that.

This is by the way an example of how painful is to try to analyze SVCOMP programs. They are full of undefined behavior that makes the implementation more complex that it should be.

shaobo-he commented 4 years ago

This is a well known issue. When we analyze GEP instructions we require to have already a cell for the pointer operand, otherwise something went wrong. In SVCOMP, there are many cases where there is some GEP instruction for which the pointer operand is NULL. Not sure if this undefined behavior but it's for sure if the result of GEP is used to load or store.

We have currently some defensive assertions in the code to make sure that GEP's pointer operands have already a cell assigned to, and then we check for code patterns that we have seen in SVCOMP to skip the code assertion. In this case the pointer operand looks a constant expression which is another GEP. Probably we don't check for that case but it's easy to do that.

This is by the way an example of how painful is to try to analyze SVCOMP programs. They are full of undefined behavior that makes the implementation more complex that it should be.

Thanks for the clarification. However, it seems this particular GEP instruction is not used for memory accesses; instead, it's converted into an integer. I think it should be fine with respect to the C standards. I was wondering if it's easy to avoid the defensive assertions for this case.

caballa commented 4 years ago

I'll avoid the defensive assertion for that case as we do already for other cases. Btw, I think pointer arithmetic on NULL is undefined behavior https://stackoverflow.com/questions/54232894/c-null-pointer-arithmetic

agurfinkel commented 4 years ago

assertions are only enabled in debug mode. Please use release build on svcomp

On Thu, Feb 27, 2020 at 18:15 Jorge Navas notifications@github.com wrote:

I'll avoid the defensive assertion for that case as we do already for other cases. Btw, I think pointer arithmetic on NULL is undefined behavior https://stackoverflow.com/questions/54232894/c-null-pointer-arithmetic

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/seahorn/sea-dsa/issues/66?email_source=notifications&email_token=ABOM3Z4CILY7QVT3DJ6VYKTRFBCQVA5CNFSM4K5EXMI2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOENGKORA#issuecomment-592226116, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABOM3ZZMNSNSYRY7AAYZD6LRFBCQVANCNFSM4K5EXMIQ .

-- On the move ...

shaobo-he commented 4 years ago

@caballa @agurfinkel Thank you for the instruction. Here's another crash,

.ll file: https://drive.google.com/open?id=1-r1fL6ezV9aHhYmfzea79Ofu3R0a5zWc

WARNING: inttoptr @ addr 0x55e93fdb5428 is allocating a new cell.
Sea-Dsa type aware!
WARNING: inttoptr @ addr 0x55e93fdd3d58 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fdd5978 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fdd7778 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fdd9428 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fddb278 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fddd0a8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fde9498 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fded728 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e9408a68a8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e9408afd88 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e9408b2eb8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e9408b9608 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e9401511d8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e94017b6d8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e94017e808 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e940184f58 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fdf9338 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe12668 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e9408e0ec8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe276b8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe2d768 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe3f4e8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe40048 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe43e78 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fecc658 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe5d388 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93ff1dfe8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93ff1eb48 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fedfe18 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fee1798 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fee3118 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fef87c8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93ff01cd8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe593f8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe5b258 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93feb8b18 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe7ed48 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe87458 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe89be8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe90078 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe929a8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe742e8 is allocating a new cell.
WARNING: inttoptr @ addr 0x55e93fe58448 is allocating a new cell.
seadsa: /mnt/local/smack-project/smack/sea-dsa/src/DsaLocal.cc:328: void {anonymous}::InterBlockBuilder::visitPHINode(llvm::PHINode&): Assertion `!c.isNull()' failed.
/usr/lib/llvm-8/lib/libLLVM-8.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamE+0x1f)[0x7f14d56ae59f]
/usr/lib/llvm-8/lib/libLLVM-8.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x7f14d56ac9c2]
/usr/lib/llvm-8/lib/libLLVM-8.so.1(+0x9719a8)[0x7f14d56ae9a8]
/lib/x86_64-linux-gnu/libc.so.6(+0x3ef20)[0x7f14d404bf20]
/lib/x86_64-linux-gnu/libc.so.6(gsignal+0xc7)[0x7f14d404be97]
/lib/x86_64-linux-gnu/libc.so.6(abort+0x141)[0x7f14d404d801]
/lib/x86_64-linux-gnu/libc.so.6(+0x3039a)[0x7f14d403d39a]
/lib/x86_64-linux-gnu/libc.so.6(+0x30412)[0x7f14d403d412]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xd7079)[0x55e93f022079]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xebf39)[0x55e93f036f39]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xe8b8b)[0x55e93f033b8b]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xe5445)[0x55e93f030445]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xe1b5c)[0x55e93f02cb5c]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xde454)[0x55e93f029454]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0xf3422)[0x55e93f03e422]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0x251c5)[0x55e93ef701c5]
/usr/lib/llvm-8/lib/libLLVM-8.so.1(_ZN4llvm6legacy15PassManagerImpl3runERNS_6ModuleE+0x2ee)[0x7f14d57a1cae]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0x177e8)[0x55e93ef627e8]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7)[0x7f14d402eb97]
smack-project/smack/sea-dsa/build/run/bin/seadsa(+0x14b0a)[0x55e93ef5fb0a]
Stack dump:
0.  Program arguments: smack-project/smack/sea-dsa/build/run/bin/seadsa -sea-dsa=ci -sea-dsa-type-aware -sea-dsa-dot floppy2.i.cil.ll 
1.  Running pass 'SeaHorn Dsa analysis: entry point for all clients' on module 'floppy2.i.cil.ll'.
Aborted

This is also an assertion failure. Should I ignore it and go ahead to use release mode?

shaobo-he commented 4 years ago

assertions are only enabled in debug mode. Please use release build on svcomp On Thu, Feb 27, 2020 at 18:15 Jorge Navas @.***> wrote: I'll avoid the defensive assertion for that case as we do already for other cases. Btw, I think pointer arithmetic on NULL is undefined behavior https://stackoverflow.com/questions/54232894/c-null-pointer-arithmetic — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#66?email_source=notifications&email_token=ABOM3Z4CILY7QVT3DJ6VYKTRFBCQVA5CNFSM4K5EXMI2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOENGKORA#issuecomment-592226116>, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABOM3ZZMNSNSYRY7AAYZD6LRFBCQVANCNFSM4K5EXMIQ . -- On the move ...

I rebuilt sea-dsa with -DCMAKE_BUILD_TYPE=Release and reran sea-dsa on this example. This time I got segmentation faults instead.

shaobo-he commented 4 years ago

Btw, the assertion failure seadsa: /mnt/local/smack-project/smack/sea-dsa/src/DsaLocal.cc:328: void {anonymous}::InterBlockBuilder::visitPHINode(llvm::PHINode&): Assertion!c.isNull()'` seems to be harmless once I switch to the release build.

agurfinkel commented 4 years ago

The two examples seem to be related to undefined behavior. In that case, we do not guarantee soundness of the result, but should not crash with a segfault either. Assertion failures in debug mode in such cases are useful as a reminder that the results should not be trusted.

It would help if you can use something like c-reduce to create minimal crash that we can add to our unit tests.

At this point, I'm no longer sure whether there are outstanding issues (e.g., crashes in release mode), or all issues are related to assertions in debug mode.

agurfinkel commented 4 years ago

I fixed the crashes. They are mostly in debug/warning print statements. Works without crashes on the two examples in this issue in both debug and release mode, and with and without --log=dsa verbosity option.

shaobo-he commented 4 years ago

@agurfinkel

We still observed crashes on SV-COMP-like benchmarks. I ran c-reduce on one of them and got the following C program,

enum a { b };
struct c {
  volatile d;
  enum a e
} f() {
  ((struct c *)804608)->e;
}

I was using llvm-8.0 branch of sea-dsa. To reproduce the crash, please use the following commands,

clang floppy_true.i.cil.c -O0 -emit-llvm -S
seadsa -sea-dsa=ci -sea-dsa-dot floppy_true.i.cil.ll

I think this problem is not meaningless. Some driver programs could just use constant pointer addresses.

agurfinkel commented 4 years ago

SeaDsa is not sound in presence of fixed pointer addresses. While such code is often perfectly legal in device drivers, it is not supported. Usually, supporting it requires a driver-specific memory model, for example, by taking into account linking scripts. These are unfortunately missing in sv-comp case.

None-the-less, I would very much prefer SeaDsa not to crash, no matter what. It would help greatly if you can also provide the ll file causing the problem and a stack trace of the failure.

Also, please submit it as a new open issue so that it is easier to track.

shaobo-he commented 4 years ago

SeaDsa is not sound in presence of fixed pointer addresses. While such code is often perfectly legal in device drivers, it is not supported. Usually, supporting it requires a driver-specific memory model, for example, by taking into account linking scripts. These are unfortunately missing in sv-comp case.

None-the-less, I would very much prefer SeaDsa not to crash, no matter what. It would help greatly if you can also provide the ll file causing the problem and a stack trace of the failure.

Also, please submit it as a new open issue so that it is easier to track.

Thank you for your reply. I just realized #72 fixes this issue as it's the same with #71. Is that possible that you could sync the llvm-8.0 branch with the master branch w.r.t. the fix?

I'd be happy to contribute a regression for #71 and #72.

agurfinkel commented 4 years ago

@caballa please move your fix to llvm8 as well.

@shaobo-he we are working on porting seahorn up, so hopefully all new changes will go to newer llvm branch.

shaobo-he commented 4 years ago

@shaobo-he we are working on porting seahorn up, so hopefully all new changes will go to newer llvm branch.

Awesome. I'm looking forward to seeing it.

shaobo-he commented 4 years ago

@caballa please move your fix to llvm8 as well.

@caballa, thank you for doing it. You can also use the tiny program in my comment as a regression for your recent changes.