[klee-dev] Why can't we use ExecutionState object in vector or map templates in cpp

Adarsh Sudheer adarshs2023 at gmail.com
Wed Apr 3 20:06:01 BST 2024


Please forgive me for some grammatical errors. I just was in a hurry.

On Thu, Apr 4, 2024 at 12:32 AM Adarsh Sudheer <adarshs2023 at gmail.com>
wrote:

> Hi all,
>
> Recently i tried to map the current the executionstate to it's left and
> right nodes using execution tree and all seemed fine until I encountered
> various segmentation errors. Firsty, in the ExecutionState class
> definition, i defined my new attribute as like this
>
>                                std::vector<ExecutionState*> NextStates;
>
> I tried to then insert the states like this
>
> if(IS_OUR_NODE_VALID(p->left) && IS_OUR_NODE_VALID(p->right)){
> p->state->NextStates.push_back(p->left.getPointer()->state);
> p->state->NextStates.push_back(p->right.getPointer()->state);
> }
> else if(IS_OUR_NODE_VALID(p->left)){
> p->state->NextStates.push_back(p->left.getPointer()->state);
> p= p->left.getPointer();
> }
> else{
> p->state->NextStates.push_back(p->right.getPointer()->state);
> p= p->right.getPointer();
> }
>
>
> I was relieved when the build didn't raised any error but when i tried to
> get the intermediate results (not included) , I repeatedly get seg-fault.
>
> Here is the error logs
> #0 0x00007f719c63fd01 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int)
> (/usr/lib/llvm-14/lib/libLLVM-14.so.1+0xe3fd01)
>  #1 0x00007f719c63da0c llvm::sys::RunSignalHandlers()
> (/usr/lib/llvm-14/lib/libLLVM-14.so.1+0xe3da0c)
>  #2 0x00007f719c640236 (/usr/lib/llvm-14/lib/libLLVM-14.so.1+0xe40236)
>  #3 0x00007f719b042520 (/lib/x86_64-linux-gnu/libc.so.6+0x42520)
>  #4 0x000055757d0c292e std::vector<klee::ExecutionState*,
> std::allocator<klee::ExecutionState*> >::push_back(klee::ExecutionState*
> const&) /usr/include/c++/11/bits/stl_vector.h:1189:20
>  #5 0x000055757d0c292e klee::RandomPathSearcher::selectState()
> /home/adarsh2023/research/klee/lib/Core/Searcher.cpp:331:37
>  #6 0x000055757d0a0008 klee::KInstIterator::operator klee::KInstruction*()
> const
> /home/adarsh2023/research/klee/include/klee/Module/KInstIterator.h:35:45
>  #7 0x000055757d0a0008 klee::Executor::run(klee::ExecutionState&)
> /home/adarsh2023/research/klee/lib/Core/Executor.cpp:3619:30
>  #8 0x000055757d0a0dbf std::__uniq_ptr_impl<klee::ExecutionTree,
> std::default_delete<klee::ExecutionTree> >::reset(klee::ExecutionTree*)
> /usr/include/c++/11/bits/unique_ptr.h:179:16
>  #9 0x000055757d0a0dbf std::unique_ptr<klee::ExecutionTree,
> std::default_delete<klee::ExecutionTree> >::reset(klee::ExecutionTree*)
> /usr/include/c++/11/bits/unique_ptr.h:456:12
> #10 0x000055757d0a0dbf std::unique_ptr<klee::ExecutionTree,
> std::default_delete<klee::ExecutionTree> >::operator=(std::nullptr_t)
> /usr/include/c++/11/bits/unique_ptr.h:397:7
> #11 0x000055757d0a0dbf klee::Executor::runFunctionAsMain(llvm::Function*,
> int, char**, char**)
> /home/adarsh2023/research/klee/lib/Core/Executor.cpp:4700:19
> #12 0x000055757d050b44 main
> /home/adarsh2023/research/klee/tools/klee/main.cpp:1520:5
> #13 0x00007f719b029d90 __libc_start_call_main
> ./csu/../sysdeps/nptl/libc_start_call_main.h:58:16
> #14 0x00007f719b029e40 call_init ./csu/../csu/libc-start.c:128:20
> #15 0x00007f719b029e40 __libc_start_main ./csu/../csu/libc-start.c:379:5
> #16 0x000055757d060f45 _start
> (/home/adarsh2023/research/klee/build/bin/klee+0x40f45)
> Segmentation fault
>
>
> When i went to the vector.h file as mentioned in 4 point, I encountered
> this condition
>
> void
> push_back(const value_type& __x)
> {
> if (this->_M_impl._M_finish != this->_M_impl._M_end_of_storage)
> {
> _GLIBCXX_ASAN_ANNOTATE_GROW(1);
> _Alloc_traits::construct(this->_M_impl, this->_M_impl._M_finish,
> __x);
> ++this->_M_impl._M_finish;
> _GLIBCXX_ASAN_ANNOTATE_GREW(1);
> }
> else
> _M_realloc_insert(end(), __x);
> }
>
>
> I think this is some memory storage issue if so, what i can do and if not
> why?
> How can i include execution state as a template in maps and vectors
>
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list