Segmentation fault when running smack (MacOS)

[hernanponcedeleon]

I updated the smack version in my Mac (everything worked in Linux) and now I'm getting some segmentation fault problems when running the tool (I get the same result in branches master, develop and v2.7.0):

SMACK program verifier version 2.7.0
0  llvm2bpl                 0x0000000107bdc775 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 37
1  llvm2bpl                 0x0000000107bdcbec SignalHandler(int) + 200
2  libsystem_platform.dylib 0x00007fff205ddd7d _sigtramp + 29
3  libsystem_platform.dylib 0x00007fe37443c0a0 _sigtramp + 18446743954858042176
4  llvm2bpl                 0x000000010632fac5 seadsa::CompleteCallGraph::runOnModule(llvm::Module&) + 757
5  llvm2bpl                 0x00000001079f1dae llvm::legacy::PassManagerImpl::run(llvm::Module&) + 684
6  llvm2bpl                 0x0000000106247e10 main + 5408
7  libdyld.dylib            0x00007fff205b3f3d start + 1
PLEASE submit a bug report to https://bugs.llvm.org/ and include the crash backtrace.
Stack dump:
0.  Program arguments: llvm2bpl /Users/ponce/git/smack/b-1gbkldto.bc -bpl 1.bpl -warn-type imprecise -sea-dsa=ci -colored-warnings -source-loc-syms -entry-points main -mem-mod-impls -llvm-assumes=none 
1.  Running pass 'Complete Call Graph SeaDsa pass' on module '/Users/ponce/git/smack/b-1gbkldto.bc'.
Traceback (most recent call last):
  File "/usr/local/bin/smack", line 13, in <module>
    smack.top.main()
  File "/usr/local/bin/../share/smack/top.py", line 953, in main
    frontend(args)
  File "/usr/local/bin/../share/smack/top.py", line 689, in frontend
    return link_bc_files(bitcodes, libs, args)
  File "/usr/local/bin/../share/smack/frontend.py", line 482, in link_bc_files
    llvm_to_bpl(args)
  File "/usr/local/bin/../share/smack/top.py", line 741, in llvm_to_bpl
    try_command(cmd, console=True)
  File "/usr/local/bin/../share/smack/utils.py", line 90, in try_command
    raise Exception("segmentation fault")
Exception: segmentation fault

~1/5 of the times, the command works. Attached is the generated .bc file.

Any idea what the problem might be?

OS version: MacOS Big Sur (version 11.3)

Compiler version:

clang version 11.1.0
Target: x86_64-apple-darwin20.4.0
Thread model: posix
InstalledDir: /usr/local/Cellar/llvm@11/11.1.0_1//bin

b-1gbkldto.bc.zip

[shaobo-he]

Hi @hernanponcedeleon, I can't seem to reproduce the error on my WSL. I'll try it on a macOS tomorrow. In the meanwhile, I think vagrant or Docker is currently the preferred way to run SMACK on OSes other than Linux.

[ThomasHaas]

Hi, I run into the same exact problem on my Mac. The error I get is pretty much identical to that of @hernanponcedeleon.

[keram88]

This is the output of SMACK on macOS ran with address sanitizer:

Exception: =================================================================
==4080==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x000105d3c608 at pc 0x000101280cf4 bp 0x00016ee26250 sp 0x00016ee26248
READ of size 8 at 0x000105d3c608 thread T0
    #0 0x101280cf0 in seadsa::CompleteCallGraphAnalysis::runOnModule(llvm::Module&)+0x4048 (llvm2bpl:arm64+0x1002a8cf0)
    #1 0x101283930 in seadsa::CompleteCallGraph::runOnModule(llvm::Module&)+0x4dc (llvm2bpl:arm64+0x1002ab930)
    #2 0x106ac9738 in llvm::legacy::PassManagerImpl::run(llvm::Module&)+0x238 (libLLVM.dylib:arm64+0x1d9738)
    #3 0x100fdd194 in main llvm2bpl.cpp:276
    #4 0x1016250f0 in start+0x204 (dyld:arm64+0x50f0)
    #5 0xc1347ffffffffffc  (<unknown module>)

0x000105d3c608 is located 8 bytes to the left of 48-byte region [0x000105d3c610,0x000105d3c640)
allocated by thread T0 here:
    #0 0x1019e929c in wrap__Znwm+0x6c (libclang_rt.asan_osx_dynamic.dylib:arm64+0x4929c)
    #1 0x1075948a4 in llvm::CallGraph::getOrInsertFunction(llvm::Function const*)+0x54 (libLLVM.dylib:arm64+0xca48a4)
    #2 0x1075948f4 in llvm::CallGraph::addToCallGraph(llvm::Function*)+0x18 (libLLVM.dylib:arm64+0xca48f4)
    #3 0x1075947f8 in llvm::CallGraph::CallGraph(llvm::Module&)+0x94 (libLLVM.dylib:arm64+0xca47f8)
    #4 0x107595acc in llvm::CallGraphWrapperPass::runOnModule(llvm::Module&)+0x28 (libLLVM.dylib:arm64+0xca5acc)
    #5 0x106ac9738 in llvm::legacy::PassManagerImpl::run(llvm::Module&)+0x238 (libLLVM.dylib:arm64+0x1d9738)
    #6 0x100fdd194 in main llvm2bpl.cpp:276
    #7 0x1016250f0 in start+0x204 (dyld:arm64+0x50f0)
    #8 0xc1347ffffffffffc  (<unknown module>)

SUMMARY: AddressSanitizer: heap-buffer-overflow (llvm2bpl:arm64+0x1002a8cf0) in seadsa::CompleteCallGraphAnalysis::runOnModule(llvm::Module&)+0x4048
Shadow bytes around the buggy address:
  0x007020bc7870: fa fa 00 00 00 00 00 fa fa fa 00 00 00 00 00 00
  0x007020bc7880: fa fa 00 00 00 00 00 00 fa fa fd fd fd fd fd fa
  0x007020bc7890: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x007020bc78a0: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x007020bc78b0: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
=>0x007020bc78c0: fa[fa]00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x007020bc78d0: fa fa 00 00 00 00 00 fa fa fa 00 00 00 00 00 00
  0x007020bc78e0: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 fa
  0x007020bc78f0: fa fa fd fd fd fd fd fa fa fa 00 00 00 00 00 00
  0x007020bc7900: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x007020bc7910: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 fa
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07 
  Heap left redzone:       fa
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
  Shadow gap:              cc
==4080==ABORTING

And with SeaDSA in Debug

Assertion failed: (I != FunctionMap.end() && "Function not in callgraph!"), function operator[], file CallGraph.h, line 122.
Stack dump:
0.  Program arguments: llvm2bpl x.bpl -warn-type approximate -sea-dsa=ci -colored-warnings -source-loc-syms -entry-points main -mem-mod-impls -llvm-assumes=none
1.  Running pass 'Complete Call Graph SeaDsa pass' on module '...'.
2. ```

[rakamaric]

I am seeing the same problem on my Mac machine. @shaobo-he can you help us out here? It seems to be SeaDSA related.

[zvonimir]

This is now fixed in the develop branch. Thanks for reporting it!