version of SVF used

[yuyuyuyuuu]

Hi, Hello when I compile with SVG found that the newer version is not very compatible, could you please tell me which version of SVF you use in this project? Thanks

[lzaoral]

Hi, what version of SVF did you try to use? We regularly test the compatibility with the latest release (2.4 at the moment) on our CI: https://github.com/mchalupa/dg/blob/cf5178c49d3c5499875b6dae4b0977a984714dc1/.github/workflows/svf.yml#L24

[yuyuyuyuuu]

Hi, Thanks, after replacing the version of SVF the problem was successfully solved. By the way, When I use dg to perform pointer analysis on the symbolic execution tool KLEE, the following error message appears, could you please to help see what caused it? Code snippets:

/*TODO*/
LLVMPointerAnalysis *PTA; 
PTA = new DGLLVMPointerAnalysis(mainModule, "main", Offset::UNKNOWN); 
PTA->run();

Error message：

 #0 0x00007f8901a254ff llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/lib/x86_64-linux-gnu/libLLVM-10.so.1+0x9814ff)
 #1 0x00007f8901a23782 llvm::sys::RunSignalHandlers() (/lib/x86_64-linux-gnu/libLLVM-10.so.1+0x97f782)
 #2 0x00007f8901a25ac5 (/lib/x86_64-linux-gnu/libLLVM-10.so.1+0x981ac5)
 #3 0x00007f8900ba70c0 (/lib/x86_64-linux-gnu/libc.so.6+0x430c0)
 #4 0x0000000000478783 std::__detail::_Mod_range_hashing::operator()(unsigned long, unsigned long) const /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/bits/hashtable_policy.h:433:20
 #5 0x0000000000478783 std::__detail::_Hash_code_base<dg::pta::PSNode*, std::pair<dg::pta::PSNode* const, dg::STLHashMap<dg::Offset, unsigned long> >, std::__detail::_Select1st, std::hash<dg::pta::PSNode*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, false>::_M_bucket_index(dg::pta::PSNode* const&, unsigned long, unsigned long) const /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/bits/hashtable_policy.h:1297:16
 #6 0x0000000000478783 std::_Hashtable<dg::pta::PSNode*, std::pair<dg::pta::PSNode* const, dg::STLHashMap<dg::Offset, unsigned long> >, std::allocator<std::pair<dg::pta::PSNode* const, dg::STLHashMap<dg::Offset, unsigned long> > >, std::__detail::_Select1st, std::equal_to<dg::pta::PSNode*>, std::hash<dg::pta::PSNode*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::_M_bucket_index(dg::pta::PSNode* const&, unsigned long) const /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/bits/hashtable.h:676:34
 #7 0x0000000000478783 std::_Hashtable<dg::pta::PSNode*, std::pair<dg::pta::PSNode* const, dg::STLHashMap<dg::Offset, unsigned long> >, std::allocator<std::pair<dg::pta::PSNode* const, dg::STLHashMap<dg::Offset, unsigned long> > >, std::__detail::_Select1st, std::equal_to<dg::pta::PSNode*>, std::hash<dg::pta::PSNode*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::find(dg::pta::PSNode* const&) const /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/bits/hashtable.h:1469:25
 #8 0x0000000000478783 std::unordered_map<dg::pta::PSNode*, dg::STLHashMap<dg::Offset, unsigned long>, std::hash<dg::pta::PSNode*>, std::equal_to<dg::pta::PSNode*>, std::allocator<std::pair<dg::pta::PSNode* const, dg::STLHashMap<dg::Offset, unsigned long> > > >::find(dg::pta::PSNode* const&) const /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/bits/unordered_map.h:926:21
 #9 0x0000000000478783 dg::PointerIDLookupTable::get(dg::pta::Pointer const&) const /data/dg/include/dg/PointerAnalysis/PointsToSets/LookupTable.h:53:28
#10 0x0000000000478783 dg::PointerIDLookupTable::getOrCreate(dg::pta::Pointer const&) /data/dg/include/dg/PointerAnalysis/PointsToSets/LookupTable.h:34:20
#11 0x0000000000477e5d dg::pta::PointerIdPointsToSet::getPointerID(dg::pta::Pointer const&) /data/dg/include/dg/PointerAnalysis/PointsToSets/PointerIdPointsToSet.h:29:28
#12 0x0000000000477e5d dg::pta::PointerIdPointsToSet::pointsTo(dg::pta::Pointer const&) const /data/dg/include/dg/PointerAnalysis/PointsToSets/PointerIdPointsToSet.h:99:29
#13 0x0000000000477e5d dg::pta::PointerIdPointsToSet::count(dg::pta::Pointer const&) const /data/dg/include/dg/PointerAnalysis/PointsToSets/PointerIdPointsToSet.h:125:53
#14 0x0000000000477e5d dg::pta::PointerIdPointsToSet::has(dg::pta::Pointer const&) const /data/dg/include/dg/PointerAnalysis/PointsToSets/PointerIdPointsToSet.h:127:49
#15 0x0000000000477e5d dg::pta::PointerIdPointsToSet::add(dg::pta::Pointer const&) /data/dg/include/dg/PointerAnalysis/PointsToSets/PointerIdPointsToSet.h:52:13
#16 0x00007f8906ecd201 dg::pta::PointerGraph::initStaticNodes() /data/dg/lib/PointerAnalysis/PointerGraph.cpp:49:34
#17 0x0000000000477935 dg::pta::PointerGraph::PointerGraph() /data/dg/include/dg/PointerAnalysis/PointerGraph.h:175:5
#18 0x0000000000476bf5 std::_Hashtable<llvm::Value const*, std::pair<llvm::Value const* const, dg::pta::PSNode*>, std::allocator<std::pair<llvm::Value const* const, dg::pta::PSNode*> >, std::__detail::_Select1st, std::equal_to<llvm::Value const*>, std::hash<llvm::Value const*>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::_Hashtable() /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/bits/hashtable.h:327:38
#19 0x0000000000476bf5 std::unordered_map<llvm::Value const*, dg::pta::PSNode*, std::hash<llvm::Value const*>, std::equal_to<llvm::Value const*>, std::allocator<std::pair<llvm::Value const* const, dg::pta::PSNode*> > >::unordered_map() /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/bits/unordered_map.h:141:7
#20 0x0000000000476bf5 dg::pta::PointsToMapping<llvm::Value const*>::PointsToMapping() /data/dg/include/dg/PointerAnalysis/PointsToMapping.h:15:7
#21 0x0000000000476bf5 dg::pta::LLVMPointerGraphBuilder::LLVMPointerGraphBuilder(llvm::Module const*, dg::LLVMPointerAnalysisOptions const&) /data/dg/include/dg/llvm/PointerAnalysis/PointerGraph.h:209:5
#22 0x0000000000476bf5 dg::DGLLVMPointerAnalysis::DGLLVMPointerAnalysis(llvm::Module const*, dg::LLVMPointerAnalysisOptions) /data/dg/include/dg/llvm/PointerAnalysis/PointerAnalysis.h:208:28
#23 0x000000000047146b dg::AnalysisOptions::~AnalysisOptions() /data/dg/include/dg/AnalysisOptions.h:27:8
#24 0x000000000047146b dg::LLVMPointerAnalysisOptions::~LLVMPointerAnalysisOptions() /data/dg/include/dg/llvm/PointerAnalysis/LLVMPointerAnalysisOptions.h:9:8
#25 0x000000000047146b dg::DGLLVMPointerAnalysis::DGLLVMPointerAnalysis(llvm::Module const*, char const*, unsigned long, bool) /data/dg/include/dg/llvm/PointerAnalysis/PointerAnalysis.h:201:15
#26 0x000000000047146b main /data/klee/tools/klee/main.cpp:1283:15
#27 0x00007f8900b880b3 __libc_start_main /build/glibc-sMfBJT/glibc-2.31/csu/../csu/libc-start.c:342:3
#28 0x000000000046e00e _start (/usr/local/bin/klee+0x46e00e)
fish: Job 1, 'klee get_branch.bc' terminated by signal SIGFPE (Floating point exception)

[mchalupa]

Does this error pop up only if you use DG from KLEE?

[yuyuyuyuuu]

Thanks, I solved this problem, because of the inconsistent compiler version I used to compile dg and klee.

[mchalupa]

Seems to be resolved, so I'm closing this issue.