Segfault in opt_pk_matrix.c

[elazarg]

Segfault encountered using ebpf-verifier. Valgrind trace:

$ valgrind ./check ebpf-samples/cilium/bpf_lxc.o 2/7 --domain=polyElina
==6092== Memcheck, a memory error detector
==6092== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==6092== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==6092== Command: ./check ebpf-samples/cilium/bpf_lxc.o 2/7 --domain=polyElina
==6092== 
==6092== Invalid write of size 8
==6092==    at 0x48A56C3: opt_matrix_alloc (opt_pk_matrix.c:71)
==6092==    by 0x48AA8E9: opt_poly_asssub_linexpr_det (opt_pk_assign.c:285)
==6092==    by 0x48AD6A9: opt_poly_asssub_texpr_array (opt_pk_assign.c:1198)
==6092==    by 0x48AD9B8: opt_pk_assign_texpr_array (opt_pk_assign.c:1327)
==6092==    by 0x4867B81: elina_abstract0_asssub_texpr_array (elina_abstract0.c:1106)
==6092==    by 0x48688CF: elina_abstract0_assign_texpr (elina_abstract0.c:1446)
==6092==    by 0x2A605B: assign_texpr (elina_domains.hpp:743)
==6092==    by 0x2A605B: crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2>::assign(ikos::variable<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>) (elina_domains.hpp:1517)
==6092==    by 0x311BD5: crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> >::array_store(ikos::variable<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, bool) (array_expansion.hpp:1224)
==6092==    by 0x3137DA: crab::analyzer::intra_abs_transformer<crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > >::exec(crab::cfg::array_store_stmt<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>&) (abs_transformer.hpp:515)
==6092==    by 0x2A9DA3: crab::analyzer::fwd_analyzer<crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> >, crab::analyzer::intra_abs_transformer<crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > > >::analyze(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> >&) (fwd_analyzer.hpp:80)
==6092==    by 0x2AB911: ikos::interleaved_fwd_fixpoint_iterator_impl::wto_iterator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> >, crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > >::visit(ikos::wto_vertex<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >&) (fwd_fixpoint_iterators.hpp:419)
==6092==    by 0x201009: ikos::wto<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >::accept(ikos::wto_component_visitor<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >*) (wto.hpp:743)
==6092==  Address 0x0 is not stack'd, malloc'd or (recently) free'd
==6092== 
==6092== 
==6092== Process terminating with default action of signal 11 (SIGSEGV)
==6092==  Access not within mapped region at address 0x0
==6092==    at 0x48A56C3: opt_matrix_alloc (opt_pk_matrix.c:71)
==6092==    by 0x48AA8E9: opt_poly_asssub_linexpr_det (opt_pk_assign.c:285)
==6092==    by 0x48AD6A9: opt_poly_asssub_texpr_array (opt_pk_assign.c:1198)
==6092==    by 0x48AD9B8: opt_pk_assign_texpr_array (opt_pk_assign.c:1327)
==6092==    by 0x4867B81: elina_abstract0_asssub_texpr_array (elina_abstract0.c:1106)
==6092==    by 0x48688CF: elina_abstract0_assign_texpr (elina_abstract0.c:1446)
==6092==    by 0x2A605B: assign_texpr (elina_domains.hpp:743)
==6092==    by 0x2A605B: crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2>::assign(ikos::variable<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>) (elina_domains.hpp:1517)
==6092==    by 0x311BD5: crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> >::array_store(ikos::variable<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, ikos::linear_expression<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>, bool) (array_expansion.hpp:1224)
==6092==    by 0x3137DA: crab::analyzer::intra_abs_transformer<crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > >::exec(crab::cfg::array_store_stmt<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string>&) (abs_transformer.hpp:515)
==6092==    by 0x2A9DA3: crab::analyzer::fwd_analyzer<crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> >, crab::analyzer::intra_abs_transformer<crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > > >::analyze(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> >&) (fwd_analyzer.hpp:80)
==6092==    by 0x2AB911: ikos::interleaved_fwd_fixpoint_iterator_impl::wto_iterator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> >, crab::domains::array_expansion_domain<crab::domains::elina_domain_<ikos::z_number, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, (crab::domains::elina_domain_id_t)2> > >::visit(ikos::wto_vertex<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >&) (fwd_fixpoint_iterators.hpp:419)
==6092==    by 0x201009: ikos::wto<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >::accept(ikos::wto_component_visitor<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::cfg_ref<crab::cfg::cfg<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, crab::cfg::var_factory_impl::variable_factory<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >::indexed_string, ikos::z_number> > >*) (wto.hpp:743)
==6092==  If you believe this happened as a result of a stack
==6092==  overflow in your program's main thread (unlikely but
==6092==  possible), you can try to increase the size of the
==6092==  main thread stack using the --main-stacksize= flag.
==6092==  The main thread stack size used in this run was 8388608.
==6092== 
==6092== HEAP SUMMARY:
==6092==     in use at exit: 216,665,945 bytes in 3,566,557 blocks
==6092==   total heap usage: 42,448,431 allocs, 38,881,874 frees, 3,415,306,951 bytes allocated
==6092== 
==6092== LEAK SUMMARY:
==6092==    definitely lost: 2,543,067 bytes in 137,568 blocks
==6092==    indirectly lost: 237,196 bytes in 11,956 blocks
==6092==      possibly lost: 92,732,261 bytes in 661,108 blocks
==6092==    still reachable: 121,153,421 bytes in 2,755,925 blocks
==6092==         suppressed: 0 bytes in 0 blocks
==6092== Rerun with --leak-check=full to see details of leaked memory
==6092== 
==6092== For counts of detected and suppressed errors, rerun with: -v
==6092== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0)

cc @caballa

[GgnDpSngh]

Hi,

Thanks for reporting this bug. I wanted to know if you are using the latest version of ELINA?

Cheers, Gagandeep Singh

[elazarg]

I believe it is the latest. I'm using it through Crab. (@caballa, does Crab fetch the latest version?)

[GgnDpSngh]

I also tried building ebpf tool on my machine in order to reproduce the bug but I get the following error while compiling:

src/asm_marshal.cpp:77:40: sorry, unimplemented: non-trivial designated initializers not supported compilation terminated due to -Wfatal-errors

any idea how to fix it?

[caballa]

@GgnDpSngh : I'm trying to reproduce the problem on my side as well. Not familiar with the error but I think he is using the post-submission branch. Let me try first before you spend more time on this.

[elazarg]

Hi, sorry for the misunderstanding, I have linked to the assert-bits branch. Only there does it reproduce. (I will not be able to respond in the next 24 hours. My sincere apologies)

[elazarg]

@GgnDpSngh the tool requires gcc 8.2+.

[caballa]

I was able to run the example and I can confirm it works fine.

[elazarg]

Just cloned from scratch and reproduced the error (with -O0 FWIW).

[GgnDpSngh]

Can you pull ELINA again and check if the bug disappears? I made a fix which might help.

[elazarg]

Seems to be fixed. Thanks! I will run regression to make sure (will take a while).

[elazarg]

Fixed. Thanks for the quick response!