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

Attempted to upgrade sea-dsa to support LLVM 11 #118

Closed shaobo-he closed 3 years ago

agurfinkel commented 3 years ago

please squash history.

Why is Align() argument to Alloca empty. Is that desired new form or should proper alignment based on DataLayout be used?

shaobo-he commented 3 years ago

@agurfinkel I used LLVM debug build to root cause the crash and got the message,

seadsa: /tmp/llvm-11/src/lib/IR/Instructions.cpp:1273: llvm::Align computeAllocaDefaultAlign(llvm::Type*, llvm::Instruction*): Assertion `I && "Insertion position cannot be null when alignment not provided!"' failed.

Relevant C++ code is listed below. It seems computeAllocaDefaultAlign requires its pointer argument not being NULL. So I think the current implementation using Align seems reasonable. Should I go ahead to squash the commits?

1277 AllocaInst::AllocaInst(Type *Ty, unsigned AddrSpace, const Twine &Name,         
1278                        Instruction *InsertBefore)                               
1279   : AllocaInst(Ty, AddrSpace, /*ArraySize=*/nullptr, Name, InsertBefore) {}     
1280                                                                                 
1281 AllocaInst::AllocaInst(Type *Ty, unsigned AddrSpace, const Twine &Name,         
1282                        BasicBlock *InsertAtEnd)                                 
1283   : AllocaInst(Ty, AddrSpace, /*ArraySize=*/nullptr, Name, InsertAtEnd) {}      
1284                                                                                 
1285 AllocaInst::AllocaInst(Type *Ty, unsigned AddrSpace, Value *ArraySize,          
1286                        const Twine &Name, Instruction *InsertBefore)            
1287     : AllocaInst(Ty, AddrSpace, ArraySize,                                      
1288                  computeAllocaDefaultAlign(Ty, InsertBefore), Name,             
1289                  InsertBefore) {}                                               
1290                                                                                 

The stack trace is also listed here,

seadsa: /tmp/llvm-11/src/lib/IR/Instructions.cpp:1273: llvm::Align computeAllocaDefaultAlign(llvm::Type*, llvm::Instruction*): Assertion `I && "Insertion position cannot be null when alignment not provided!"' failed.
 #0 0x0000000001e13271 llvm::sys::PrintStackTrace(llvm::raw_ostream&) /tmp/llvm-11/src/lib/Support/Unix/Signals.inc:564:22
 #1 0x0000000001e13304 PrintStackTraceSignalHandler(void*) /tmp/llvm-11/src/lib/Support/Unix/Signals.inc:625:1
 #2 0x0000000001e110b7 llvm::sys::RunSignalHandlers() /tmp/llvm-11/src/lib/Support/Signals.cpp:68:20
 #3 0x0000000001e12bf1 SignalHandler(int) /tmp/llvm-11/src/lib/Support/Unix/Signals.inc:406:1
 #4 0x00007f71e191a980 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x12980)
 #5 0x00007f71e0378fb7 raise /build/glibc-S9d2JN/glibc-2.27/signal/../sysdeps/unix/sysv/linux/raise.c:51:0
 #6 0x00007f71e037a921 abort /build/glibc-S9d2JN/glibc-2.27/stdlib/abort.c:81:0
 #7 0x00007f71e036a48a __assert_fail_base /build/glibc-S9d2JN/glibc-2.27/assert/assert.c:89:0
 #8 0x00007f71e036a502 (/lib/x86_64-linux-gnu/libc.so.6+0x30502)
 #9 0x0000000000ee55c7 computeAllocaDefaultAlign(llvm::Type*, llvm::Instruction*) /tmp/llvm-11/src/lib/IR/Instructions.cpp:1274:54
#10 0x0000000000ee56a2 llvm::AllocaInst::AllocaInst(llvm::Type*, unsigned int, llvm::Value*, llvm::Twine const&, llvm::Instruction*) /tmp/llvm-11/src/lib/IR/Instructions.cpp:1289:30
#11 0x0000000000ee5629 llvm::AllocaInst::AllocaInst(llvm::Type*, unsigned int, llvm::Twine const&, llvm::Instruction*) /tmp/llvm-11/src/lib/IR/Instructions.cpp:1279:75
#12 0x00000000015b80d4 seadsa::ShadowMemImpl::getShadowForField(seadsa::Node const&, unsigned int) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:381:13
#13 0x00000000015c3691 seadsa::ShadowMemImpl::getShadowForField(seadsa::Cell const&) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:389:5
#14 0x00000000015b93ac seadsa::ShadowMemImpl::mkShadowStore(llvm::IRBuilder<llvm::ConstantFolder, llvm::IRBuilderDefaultInserter>&, seadsa::Cell const&, llvm::Optional<unsigned int>) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:478:17
#15 0x00000000015b004c seadsa::ShadowMemImpl::visitStoreInst(llvm::StoreInst&) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:1040:13
#16 0x00000000015cc080 llvm::InstVisitor<seadsa::ShadowMemImpl, void>::visitStore(llvm::StoreInst&) /tmp/llvm-11/install/include/llvm/IR/Instruction.def:173:1
#17 0x00000000015cb722 llvm::InstVisitor<seadsa::ShadowMemImpl, void>::visit(llvm::Instruction&) /tmp/llvm-11/install/include/llvm/IR/Instruction.def:173:1
#18 0x00000000015cb3a2 void llvm::InstVisitor<seadsa::ShadowMemImpl, void>::visit<llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::Instruction, true, false, void>, false, false> >(llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::Instruction, true, false, void>, false, false>, llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::Instruction, true, false, void>, false, false>) /tmp/llvm-11/install/include/llvm/IR/InstVisitor.h:89:5
#19 0x00000000015cb322 llvm::InstVisitor<seadsa::ShadowMemImpl, void>::visit(llvm::BasicBlock&) /tmp/llvm-11/install/include/llvm/IR/InstVisitor.h:106:3
#20 0x00000000015cb2c2 void llvm::InstVisitor<seadsa::ShadowMemImpl, void>::visit<llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::BasicBlock, true, false, void>, false, false> >(llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::BasicBlock, true, false, void>, false, false>, llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::BasicBlock, true, false, void>, false, false>) /tmp/llvm-11/install/include/llvm/IR/InstVisitor.h:89:5
#21 0x00000000015b7a12 llvm::InstVisitor<seadsa::ShadowMemImpl, void>::visit(llvm::Function&) /tmp/llvm-11/install/include/llvm/IR/InstVisitor.h:102:3
#22 0x00000000015ae4de seadsa::ShadowMemImpl::runOnFunction(llvm::Function&) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:853:9
#23 0x00000000015bb312 seadsa::ShadowMemImpl::runOnModule(llvm::Module&) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:665:18
#24 0x00000000015b53ac seadsa::ShadowMem::runOnModule(llvm::Module&) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:1785:8
#25 0x00000000015b59e3 seadsa::ShadowMemPass::runOnModule(llvm::Module&) /tmp/sea-dsa/build/../lib/seadsa/ShadowMem.cc:1844:8
#26 0x0000000000f2a579 (anonymous namespace)::MPPassManager::runOnModule(llvm::Module&) /tmp/llvm-11/src/lib/IR/LegacyPassManager.cpp:1617:20
#27 0x0000000000f25574 llvm::legacy::PassManagerImpl::run(llvm::Module&) /tmp/llvm-11/src/lib/IR/LegacyPassManager.cpp:614:13
#28 0x0000000000f2ae23 llvm::legacy::PassManager::run(llvm::Module&) /tmp/llvm-11/src/lib/IR/LegacyPassManager.cpp:1738:1
#29 0x0000000000412883 main /tmp/sea-dsa/build/../tools/seadsa.cc:232:16
#30 0x00007f71e035bbf7 __libc_start_main /build/glibc-S9d2JN/glibc-2.27/csu/../csu/libc-start.c:344:0
#31 0x00000000004112ea _start (/tmp/sea-dsa/build/run/bin/seadsa+0x4112ea)
PLEASE submit a bug report to https://bugs.llvm.org/ and include the crash backtrace.
Stack dump:
0.  Program arguments: /tmp/sea-dsa/build/run/bin/seadsa -sea-dsa-shadow-mem --sea-dsa=cs /tmp/sea-dsa/tests/shadow_mem_2.ll -oll /tmp/sea-dsa/tests/shadow_mem_2.ll.inst.ll 
1.  Running pass 'ShadowMemSeaDsa' on module '/tmp/sea-dsa/tests/shadow_mem_2.ll'.
Aborted (core dumped)
agurfinkel commented 3 years ago

I see the comment about missing alignment. So this is trickier than I thought. Looks like in LLVM11 alignment is not defined by the Module but by individual function. So looks like we need to replicate some of the code in computeAllocaDefaultAlign locally to get the right alignment.

shaobo-he commented 3 years ago

I see the comment about missing alignment. So this is trickier than I thought. Looks like in LLVM11 alignment is not defined by the Module but by individual function. So looks like we need to replicate some of the code in computeAllocaDefaultAlign locally to get the right alignment.

I squashed the commits. However, I'm a little confused by your comment here. It seems computeAllocaDefaultAlign computes a per-type default alignment (https://llvm.org/doxygen/Instructions_8cpp_source.html#l01314). I was wondering if all we need here is the default alignment for the type m_Int32Ty.

agurfinkel commented 3 years ago

You should use DL.getPrefTypeAlign(Ty); for alignment. We should have the right DL available.

LLVM code extracts DL from instructions. At this point, we don't have an instruction, but we do know the DL. So just follow the code.

shaobo-he commented 3 years ago

You should use DL.getPrefTypeAlign(Ty); for alignment. We should have the right DL available.

LLVM code extracts DL from instructions. At this point, we don't have an instruction, but we do know the DL. So just follow the code.

Thank you for the pointer. I checked in the changes requested. If it looks good, I will squash the commits again.

shaobo-he commented 3 years ago

@agurfinkel I just squashed the commits. Please let me know if there are any changes I need to make.

agurfinkel commented 3 years ago

@shaobo-he this looks good. I just had a few clarifying comments.

shaobo-he commented 3 years ago

@agurfinkel Thank you for your feedback. I made the changes you requested and squashed the commits. Could you take a look at them and let me know if there are further changes I need to make?

shaobo-he commented 3 years ago

this is good to go

Thank you. A minor issue is that CMake's find_package(LLVM 11) won't work for the LLVM 11 Debian package (see https://github.com/banach-space/llvm-tutor/commit/72cb20d058b9b3f51717c7a17607f7a4c7398642). So for SMACK's LLVM 11 support, I had to change the version number from 11 to 11.1. Please let me know if it makes sense or not. If you have better solutions, please let me know as well.

agurfinkel commented 3 years ago

using llvm 11.1 as default is ok with me

shaobo-he commented 3 years ago

using llvm 11.1 as default is ok with me

Sounds good. Let me add this and squash commits.

shaobo-he commented 3 years ago

using llvm 11.1 as default is ok with me

Sounds good. Let me add this and squash commits.

Done.

agurfinkel commented 3 years ago

manually merged into branch dev11

@shaobo-he thank you!