Open
Description
CBMC version: cbmc-5.43.0 from develop branch, commit 07895efefd6780560dffdae10d83857714ae6b8e
Operating system: Ubuntu 20.04 64-bit
Exact command line resulting in the issue:
gdb --ex=run --args env CADICAL_API_TRACE=/scratch/exchange/cadical_api_trace.txt LD_PRELOAD=/usr/local/lib/libjemalloc.so.2 cbmc Sample2.c --trace --error-label success --symex-cache-dereferences
What behaviour did you expect: CBMC analyses the program correctly and passes its formula to SAT solver (Cadical)
What happened instead: a crash in CBMC
I found this bug while troubleshooting a crash in Cadical, but it seems that the memory may be corrupted by CBMC (the tools run within the same process). I built CBMC with Cadical as follows (I also built jemalloc for finding the memory corruption):
cd /scratch/install/src/jemalloc
export CFLAGS="-mavx2 -mfma -O3 -ggdb3"
export CXXFLAGS="-mavx2 -mfma -O3 -ggdb3"
export LDFLAGS="-rdynamic"
CC=clang-13 CXX=clang++-13 ./configure --enable-debug
make -j 128
sudo make install
cd /scratch/install/src/cadical
rm -rf build
CFLAGS="-mavx2 -mfma" \
CXXFLAGS="-mavx2 -mfma" \
CXX=clang++-13 CC=clang-13 ./configure --symbols --check
make -j 128
cd /scratch/install/src/cbmc
make -C src clean
export CFLAGS="-mavx2 -mfma -O3 -ggdb3"
export CXXFLAGS="-mavx2 -mfma -O3 -ggdb3"
make CADICAL=/scratch/install/src/cadical CC=clang-13 CXX=clang++-13 \
LINKFLAGS="-rdynamic" \
-j 128 -C src
sudo cp src/cbmc/cbmc /usr/local/bin/
All the tools were cloned in GIT from master/develop branches. Cadical version is 1.5.2 (commit ca9bff05c11bde5eae4912f9932871d1527e61d8). Jemalloc commit is b6a7a535b32a3298db5b3518bc1f52fccc1597a6.
GDB prints the following stack trace:
--- begin invariant violation report ---
Invariant check failed
File: ../util/irep.h:573 function: remove_ref
Condition: old_data->ref_count != 0
Reason: Precondition
Backtrace:
cbmc(print_backtrace(std::ostream&)+0xae) [0x6265fe]
cbmc(get_backtrace[abi:cxx11]()+0x24) [0x626db4]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x2d) [0x55c33d]
cbmc() [0x556c46]
cbmc(sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref(tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>*)+0x11f) [0x55b15f]
cbmc(sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref(tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>*)+0x48) [0x55b088]
cbmc(sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref(tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>*)+0x48) [0x55b088]
cbmc(sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref(tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>*)+0x48) [0x55b088]
cbmc(sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref(tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>*)+0x48) [0x55b088]
cbmc(goto_symex_statet::assignment(ssa_exprt, exprt const&, namespacet const&, bool, bool, bool)+0x495) [0x9293c5]
cbmc(symex_assignt::assign_non_struct_symbol(ssa_exprt const&, expr_skeletont const&, exprt const&, std::vector<exprt, std::allocator<exprt> > const&)+0x1d5) [0x958d65]
cbmc(symex_assignt::assign_byte_extract(byte_extract_exprt const&, expr_skeletont const&, exprt const&, std::vector<exprt, std::allocator<exprt> >&)+0xbc) [0x957cdc]
cbmc(goto_symext::symex_assign(goto_symex_statet&, exprt const&, exprt const&)+0x3d9) [0x91f7a9]
cbmc(goto_symext::execute_next_instruction(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&)+0x247) [0x97be67]
cbmc(goto_symext::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&)+0x27) [0x97bba7]
cbmc(symex_bmct::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&)+0x23b) [0x862cbb]
cbmc(goto_symext::symex_threaded_step(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&)+0x1c) [0x97a54c]
cbmc(goto_symext::symex_with_state(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&, symbol_tablet&)+0xcf) [0x97a85f]
cbmc(goto_symext::symex_from_entry_point_of(std::function<goto_functiont const& (dstringt const&)> const&, symbol_tablet&)+0x36) [0x97b366]
cbmc(multi_path_symex_only_checkert::generate_equation()+0x45) [0x84cf75]
cbmc(multi_path_symex_checkert::operator()(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x53) [0x84bae3]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x34) [0x6af444]
cbmc(cbmc_parse_optionst::doit()+0xc14) [0x6a7ec4]
cbmc(parse_options_baset::main()+0x83) [0xbf5443]
cbmc(main+0x22) [0x6a29d2]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7ffff77b10b3]
cbmc(_start+0x2e) [0x548d8e]
--- end invariant violation report ---
Program received signal SIGABRT, Aborted.
__GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:50
50 ../sysdeps/unix/sysv/linux/raise.c: No such file or directory.
(gdb) bt
#0 __GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:50
#1 0x00007ffff77af859 in __GI_abort () at abort.c:79
#2 0x000000000055c372 in invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&> (file=..., function=...,
line=<optimized out>, line@entry=573, condition=..., params="Precondition") at ../util/invariant.h:260
#3 0x0000000000556c46 in invariant_violated_string (file=<error reading variable: Cannot access memory at address 0xa>,
function=<error reading variable: Cannot create a lazy string with address 0x0, and a non-zero length.>, line=0, line@entry=573, condition=<error: Cannot access memory at address 0x10824848b48>,
reason=<error reading variable: Cannot access memory at address 0x8>) at ../util/invariant.h:282
#4 0x000000000055b15f in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref (old_data=0x7ffff6db6580) at ../util/irep.h:573
#5 0x000000000055b088 in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::~sharing_treet (this=0x7ffff5b55e30) at ../util/irep.h:247
#6 std::_Destroy<irept> (__pointer=0x7ffff5b55e30) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:140
#7 std::_Destroy_aux<false>::__destroy<irept*> (__first=0x7ffff5b55e30, __last=0x7ffff5b55f00) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:152
#8 std::_Destroy<irept*> (__first=<optimized out>, __last=0x7ffff5b55f00) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:184
#9 std::_Destroy<irept*, irept> (__first=<optimized out>, __last=0x7ffff5b55f00) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/alloc_traits.h:746
#10 std::vector<irept, std::allocator<irept> >::~vector (this=0x7ffff5b742e0) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_vector.h:680
#11 tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>::~tree_nodet (this=0x7ffff5b742d0) at ../util/irep.h:108
#12 sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref (old_data=0x7ffff5b742d0) at ../util/irep.h:590
#13 0x000000000055b088 in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::~sharing_treet (this=0x7ffff5b3a228) at ../util/irep.h:247
#14 std::_Destroy<irept> (__pointer=0x7ffff5b3a228) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:140
#15 std::_Destroy_aux<false>::__destroy<irept*> (__first=0x7ffff5b3a228, __last=0x7ffff5b3a400) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:152
#16 std::_Destroy<irept*> (__first=<optimized out>, __last=0x7ffff5b3a400) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:184
#17 std::_Destroy<irept*, irept> (__first=<optimized out>, __last=0x7ffff5b3a400) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/alloc_traits.h:746
#18 std::vector<irept, std::allocator<irept> >::~vector (this=0x7ffff5b741c0) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_vector.h:680
#19 tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>::~tree_nodet (this=0x7ffff5b741b0) at ../util/irep.h:108
#20 sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref (old_data=0x7ffff5b741b0) at ../util/irep.h:590
#21 0x000000000055b088 in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::~sharing_treet (this=0x7ffff5ad1450) at ../util/irep.h:247
#22 std::_Destroy<irept> (__pointer=0x7ffff5ad1450) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:140
#23 std::_Destroy_aux<false>::__destroy<irept*> (__first=0x7ffff5ad1450, __last=0x7ffff5ad1460) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:152
#24 std::_Destroy<irept*> (__first=<optimized out>, __last=0x7ffff5ad1460) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:184
#25 std::_Destroy<irept*, irept> (__first=<optimized out>, __last=0x7ffff5ad1460) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/alloc_traits.h:746
#26 std::vector<irept, std::allocator<irept> >::~vector (this=0x7ffff5b74190) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_vector.h:680
#27 tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>::~tree_nodet (this=0x7ffff5b74180) at ../util/irep.h:108
#28 sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref (old_data=0x7ffff5b74180) at ../util/irep.h:590
#29 0x000000000055b088 in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::~sharing_treet (this=0x7ffff5a3e828) at ../util/irep.h:247
#30 std::_Destroy<irept> (__pointer=0x7ffff5a3e828) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:140
#31 std::_Destroy_aux<false>::__destroy<irept*> (__first=0x7ffff5a3e828, __last=0x7ffff5a3e900) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:152
#32 std::_Destroy<irept*> (__first=<optimized out>, __last=0x7ffff5a3e900) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_construct.h:184
#33 std::_Destroy<irept*, irept> (__first=<optimized out>, __last=0x7ffff5a3e900) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/alloc_traits.h:746
#34 std::vector<irept, std::allocator<irept> >::~vector (this=0x7ffff5b256e0) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/stl_vector.h:680
#35 tree_nodet<irept, forward_list_as_mapt<dstringt, irept>, true>::~tree_nodet (this=0x7ffff5b256d0) at ../util/irep.h:108
#36 sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::remove_ref (old_data=0x7ffff5b256d0) at ../util/irep.h:590
#37 0x00000000009293c5 in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::~sharing_treet (this=<optimized out>) at ../util/irep.h:247
#38 goto_symex_statet::assignment (this=<optimized out>, lhs=..., rhs=..., ns=..., rhs_is_simplified=true, record_value=<optimized out>, allow_pointer_unsoundness=<optimized out>)
at goto_symex_state.cpp:137
#39 0x0000000000958d65 in symex_assignt::assign_non_struct_symbol (this=0x7fffffffc2c0, this@entry=0x7ffff6d62800, lhs=..., full_lhs=..., rhs=...,
guard=std::vector of length -518288384, capacity -634610 = {...}) at symex_assign.cpp:172
#40 0x0000000000957343 in symex_assignt::assign_symbol (this=<optimized out>, lhs=..., full_lhs=..., rhs=..., guard=...) at symex_assign.cpp:231
#41 symex_assignt::assign_rec (this=<optimized out>, this@entry=0x7fffffffc2c0, lhs=..., full_lhs=..., rhs=..., guard=std::vector of length 0, capacity 0) at symex_assign.cpp:44
#42 0x0000000000957cdc in symex_assignt::assign_byte_extract (this=0x7fffffffc2c0, lhs=..., full_lhs=..., rhs=..., guard=std::vector of length 0, capacity 0) at symex_assign.cpp:384
#43 0x000000000091f7a9 in goto_symext::symex_assign (this=0x7ffff6d62810, state=..., o_lhs=..., o_rhs=...) at goto_symex.cpp:119
#44 0x000000000097be67 in goto_symext::execute_next_instruction(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&) (this=this@entry=0x7ffff6d62810,
get_goto_function=..., state=...) at symex_main.cpp:670
#45 0x000000000097bba7 in goto_symext::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&) (this=0x7ffff6d62810, get_goto_function=..., state=...)
--Type <RET> for more, q to quit, c to continue without paging--c
at symex_main.cpp:598
#46 0x0000000000862cbb in symex_bmct::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&) (this=0x7ffff6d62810, get_goto_function=..., state=...) at symex_bmc.cpp:73
#47 0x000000000097a54c in goto_symext::symex_threaded_step(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&) (this=this@entry=0x7ffff6d62810, state=..., get_goto_function=...) at symex_main.cpp:304
#48 0x000000000097a85f in goto_symext::symex_with_state(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&, symbol_tablet&) (this=0x7ffff6d62810, state=..., get_goto_function=..., new_symbol_table=...) at symex_main.cpp:370
#49 0x000000000097b366 in goto_symext::symex_from_entry_point_of(std::function<goto_functiont const& (dstringt const&)> const&, symbol_tablet&) (this=0x7ffff6d62810, get_goto_function=..., new_symbol_table=...) at symex_main.cpp:476
#50 0x000000000084cf75 in multi_path_symex_only_checkert::generate_equation (this=0x7ffff6d621f0) at multi_path_symex_only_checker.cpp:77
#51 0x000000000084bae3 in multi_path_symex_checkert::operator() (this=0x7ffff6d621f0, properties=Python Exception <class 'AttributeError'> 'NoneType' object has no attribute 'pointer':
std::map with 1 element) at multi_path_symex_checker.cpp:49
#52 0x00000000006af444 in all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator() (this=0x7ffff6d62000) at ../goto-checker/all_properties_verifier_with_trace_storage.h:43
#53 0x00000000006a7ec4 in cbmc_parse_optionst::doit (this=0x7fffffffd928) at cbmc_parse_options.cpp:778
#54 0x0000000000bf5443 in parse_options_baset::main (this=0x7fffffffd928) at parse_options.cpp:100
#55 0x00000000006a29d2 in main (argc=<optimized out>, argv=<optimized out>) at cbmc_main.cpp:48
Unfortunately, I cannot share the Sample2.c program because it's proprietary.
The crash in CBMC doesn't happen always - I ran it a few tens of times (also with Address&Undefined sanitizers), and it's the first time I'm seeing the crash.