search

seahorn / crab

A library for building abstract interpretation-based analyses
Apache License 2.0
233 stars 32 forks source link

none-optional dereference on array-expansion domain with elina-pk #26

Closed elazarg closed 5 years ago

elazarg commented 5 years ago

The issue seem to come from array_expansion.hpp:1287 - missing if (!ignore_array_store) in the condition.

Valgrind traceback:

ebpf-verifier (post-submission)$ valgrind ./check ebpf-samples/cilium/bpf_lxc.o 2/7 --domain=polyElina
==31540== Memcheck, a memory error detector
==31540== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==31540== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==31540== Command: ./check ebpf-samples/cilium/bpf_lxc.o 2/7 --domain=polyElina
==31540== 
exception vector product
exception vector product
exception vector product
exception vector product
check: /usr/include/boost/optional/optional.hpp:1205: boost::optional<T>::reference_type boost::optional<T>::get() [with T = ikos::z_number; boost::optional<T>::reference_type = ikos::z_number&]: Assertion `this->is_initialized()' failed.
==31540== 
==31540== Process terminating with default action of signal 6 (SIGABRT)
==31540==    at 0x5967077: raise (raise.c:51)
==31540==    by 0x5948534: abort (abort.c:79)
==31540==    by 0x594840E: __assert_fail_base.cold.0 (assert.c:92)
==31540==    by 0x5958141: __assert_fail (assert.c:101)
==31540==    by 0x31666E: get (optional.hpp:1205)
==31540==    by 0x31666E: operator* (optional.hpp:1222)
==31540==    by 0x31666E: 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_range(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>, 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>) (array_expansion.hpp:1287)
==31540==    by 0x317107: 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:518)
==31540==    by 0x2ACA8E: 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)
==31540==    by 0x2B4E71: 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)
==31540==    by 0x201409: 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)
==31540==    by 0x1D2C79: run (fwd_fixpoint_iterators.hpp:261)
==31540==    by 0x1D2C79: Run (fwd_analyzer.hpp:138)
==31540==    by 0x1D2C79: run (fwd_analyzer.hpp:285)
==31540==    by 0x1D2C79: crab::checker::checks_db analyze<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> > >(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>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&) (crab_verifier.cpp:156)
==31540==    by 0x1DA725: std::_Function_handler<crab::checker::checks_db (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>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&), crab::checker::checks_db (*)(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>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&)>::_M_invoke(std::_Any_data const&, 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>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&, boost::signals2::signal<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&), boost::signals2::optional_last_value<void>, int, std::less<int>, boost::function<void (std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::function<void (boost::signals2::connection const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)>, boost::signals2::mutex>&) (std_function.h:283)
==31540==    by 0x1D14F5: operator() (std_function.h:687)
==31540==    by 0x1D14F5: analyze (crab_verifier.cpp:232)
==31540==    by 0x1D14F5: abs_validate(Cfg const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, program_info) (crab_verifier.cpp:72)
==31540== 
==31540== HEAP SUMMARY:
==31540==     in use at exit: 463,322,523 bytes in 4,653,262 blocks
==31540==   total heap usage: 48,232,624 allocs, 43,579,362 frees, 4,789,812,024 bytes allocated
==31540== 
==31540== LEAK SUMMARY:
==31540==    definitely lost: 2,784,843 bytes in 142,118 blocks
==31540==    indirectly lost: 326,439 bytes in 16,535 blocks
==31540==      possibly lost: 155,348,967 bytes in 1,107,462 blocks
==31540==    still reachable: 304,862,274 bytes in 3,387,147 blocks
==31540==         suppressed: 0 bytes in 0 blocks
==31540== Rerun with --leak-check=full to see details of leaked memory
==31540== 
==31540== For counts of detected and suppressed errors, rerun with: -v
==31540== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
Aborted (core dumped)
elazarg commented 5 years ago

(also in the next condition. maybe if (ignore_array_store) return; is better)

caballa commented 5 years ago

Thanks for debugging that. I've committed a fix. Let me know how it goes

elazarg commented 5 years ago

Fixed