Skip to content

Possible bug in ila.so when using the setVar call #1

@deepaksirone

Description

@deepaksirone

The setVar call crashes when setting register values. The exact register which causes the crash seems to differ in differing environments.

Stack trace:

#0  0x00007fffec99a3c6 in __dynamic_cast () from /lib64/libstdc++.so.6
#1  0x00007fffee7e6680 in ila::BitvectorConst::equal (this=0x555555d14c80, that_=0x555557973290) at src/ast/bitvec.cpp:107
#2  0x00007fffee80184d in ila::nodeEqual (left=0x555555d14c80, right=0x555557973290) at src/ast/node.cpp:198
#3  0x00007fffee8d48af in std::__detail::_Equal_helper<ila::Node const*, std::pair<ila::Node const* const, z3::expr>, std::__detail::_Select1st, bool (*)(ila::Node const*, ila::Node const*), unsigned long, true>::_S_equals (
    __eq=@0x7fffe769b850: 0x7fffee80181f <ila::nodeEqual(ila::Node const*, ila::Node const*)>, __extract=..., 
    __k=@0x7fffffffcc30: 0x555555d14c80, __c=0x6b730f308e64012a, __n=0x555557c796d0)
    at /usr/include/c++/7/bits/hashtable_policy.h:1433
#4  0x00007fffee8d453a in std::__detail::_Hashtable_base<ila::Node const*, std::pair<ila::Node const* const, z3::expr>, std::__detail::_Select1st, bool (*)(ila::Node const*, ila::Node const*), unsigned long (*)(ila::Node const*), std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Hashtable_traits<true, false, true> >::_M_equals (this=0x7fffe769b848, 
    __k=@0x7fffffffcc30: 0x555555d14c80, __c=0x6b730f308e64012a, __n=0x555557c796d0)
    at /usr/include/c++/7/bits/hashtable_policy.h:1815
#5  0x00007fffee8d3f5a in std::_Hashtable<ila::Node const*, std::pair<ila::Node const* const, z3::expr>, std::allocator<std::pair<ila::Node const* const, z3::expr> >, std::__detail::_Select1st, bool (*)(ila::Node const*, ila::Node const*), unsigned long (*)(ila::Node const*), std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true> >::_M_find_before_node (this=0x7fffe769b848, __n=0x10b, __k=@0x7fffffffcc30: 0x555555d14c80, 
    __code=0x6b730f308e64012a) at /usr/include/c++/7/bits/hashtable.h:1548
#6  0x00007fffee8d3ac8 in std::_Hashtable<ila::Node const*, std::pair<ila::Node const* const, z3::expr>, std::allocator<std::pair<ila::Node const* const, z3::expr> >, std::__detail::_Select1st, bool (*)(ila::Node const*, ila::Node const*), unsigned long (*)(ila::Node const*), std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true> >::_M_find_node (this=0x7fffe769b848, __bkt=0x10b, __key=@0x7fffffffcc30: 0x555555d14c80, 
    __c=0x6b730f308e64012a) at /usr/include/c++/7/bits/hashtable.h:642
#7  0x00007fffee8d36f4 in std::_Hashtable<ila::Node const*, std::pair<ila::Node const* const, z3::expr>, std::allocator<std::pair<ila::Node const* const, z3::expr> >, std::__detail::_Select1st, bool (*)(ila::Node const*, ila::Node const*), unsigned long (*)(ila::Node const*), std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true> >::find (this=0x7fffe769b848, __k=@0x7fffffffcc30: 0x555555d14c80)
    at /usr/include/c++/7/bits/hashtable.h:1422
#8  0x00007fffee8d2cf7 in std::unordered_map<ila::Node const*, z3::expr, unsigned long (*)(ila::Node const*), bool (*)(ila::Node const*, ila::Node const*), std::allocator<std::pair<ila::Node const* const, z3::expr> > >::find (this=0x7fffe769b848, 
    __x=@0x7fffffffcc30: 0x555555d14c80) at /usr/include/c++/7/bits/unordered_map.h:923
#9  0x00007fffee8cb4af in ila::Z3ExprAdapter::operator() (this=0x7fffe769b838, n=0x555555d14c80) at src/smt.cpp:40
#10 0x00007fffee8d2e96 in ila::Node::depthFirstVisit<ila::Z3ExprAdapter> (this=0x555555d14c80, func=...) at include/ast/node.hpp:168
#11 0x00007fffee8cd1a9 in ila::Z3ExprAdapter::getExpr (this=0x7fffe769b838, n=0x555555d14c80) at src/smt.cpp:183
#12 0x00007fffee8055c4 in ila::LiftingZ3Adapter::addConstant (this=0x7fffe769b838, name="XRAM_ADDR", init=0x555555d14c80)
    at src/uclid5.cpp:8
#13 0x00007fffee806261 in ila::Uclid5Translator::setVar (this=0x7fffe769b7f0, name="XRAM_ADDR", value_=...) at src/uclid5.cpp:118
#14 0x00007fffee8800aa in boost::python::detail::invoke<int, void (ila::Uclid5Translator::*)(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, boost::python::api::object&), boost::python::arg_from_python<ila::Uclid5Translator&>, boost::python::arg_from_python<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>, boost::python::arg_from_python<boost::python::api::object&> > (f=
    @0x55555593f668: (void (ila::Uclid5Translator::*)(ila::Uclid5Translator * const, const std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > &, boost::python::api::object &)) 0x7fffee8060e0 <ila::Uclid5Translator::setVar(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, boost::python::api::object&)>, tc=..., ac0=..., ac1=...)
    at /usr/local/include/boost/python/detail/invoke.hpp:92
#15 0x00007fffee872530 in boost::python::detail::caller_arity<3u>::impl<void (ila::Uclid5Translator::*)(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, boost::python::api::object&), boost::python::default_call_policies, boost::mpl::vector4<void, ila::Uclid5Translator&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, boost::python::api::object&> >::operator() (this=0x55555593f668, args_=0x7fffe7900230)
    at /usr/local/include/boost/python/detail/caller.hpp:216
#16 0x00007fffee865989 in boost::python::objects::caller_py_function_impl<boost::python::detail::caller<void (ila::Uclid5Translator::*)(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, boost::python::api::object&), boost::python::default_call_policies, boost::mpl::vector4<void, ila::Uclid5Translator&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, boost::python::api::object&> > >::operator() (this=0x55555593f660, args=0x7fffe7900230, kw=0x0)
    at /usr/local/include/boost/python/object/py_function.hpp:38
#17 0x00007fffee269855 in boost::python::objects::function::call(_object*, _object*) const ()
   from /usr/local/lib/libboost_python27.so.1.67.0
#18 0x00007fffee269a08 in boost::detail::function::void_function_ref_invoker0<boost::python::objects::(anonymous namespace)::bind_return, void>::invoke(boost::detail::function::function_buffer&) () from /usr/local/lib/libboost_python27.so.1.67.0
#19 0x00007fffee27034b in boost::python::detail::exception_handler::operator()(boost::function0<void> const&) const ()
   from /usr/local/lib/libboost_python27.so.1.67.0
#20 0x00007fffee85284e in boost::python::detail::translate_exception<ila::PyILAException, void (*)(ila::PyILAException const&)>::operator() (this=0x55555592e328, handler=..., f=..., translate=0x7fffee82f862 <ila::translateILAException(ila::PyILAException const&)>)
    at /usr/local/include/boost/python/detail/translate_exception.hpp:46
#21 0x00007fffee84db8d in boost::_bi::list3<boost::arg<1>, boost::arg<2>, boost::_bi::value<void (*)(ila::PyILAException const&)> >::operator()<bool, boost::python::detail::translate_exception<ila::PyILAException, void (*)(ila::PyILAException const&)>, boost::_bi::rrlist2<boost::python::detail::exception_handler const&, boost::function0<void> const&> > (this=0x55555592e330, f=..., a=...)
    at /usr/local/include/boost/bind/bind.hpp:388
#22 0x00007fffee84950c in boost::_bi::bind_t<bool, boost::python::detail::translate_exception<ila::PyILAException, void (*)(ila::PyILAException const&)>, boost::_bi::list3<boost::arg<1>, boost::arg<2>, boost::_bi::value<void (*)(ila::PyILAException const&)> > >::operator()<boost::python::detail::exception_handler const&, boost::function0<void> const&> (this=0x55555592e328, a1=..., a2=...)
    at /usr/local/include/boost/bind/bind.hpp:1318
#23 0x00007fffee844e46 in boost::detail::function::function_obj_invoker2<boost::_bi::bind_t<bool, boost::python::detail::translate_exception<ila::PyILAException, void (*)(ila::PyILAException const&)>, boost::_bi::list3<boost::arg<1>, boost::arg<2>, boost::_bi::value<void (*)(ila::PyILAException const&)> > >, bool, boost::python::detail::exception_handler const&, boost::function0<void> const&>::invoke
    (function_obj_ptr=..., a0=..., a1=...) at /usr/local/include/boost/function/function_template.hpp:138
#24 0x00007fffee27011f in boost::python::handle_exception_impl(boost::function0<void>) ()
   from /usr/local/lib/libboost_python27.so.1.67.0
#25 0x00007fffee267209 in function_call () from /usr/local/lib/libboost_python27.so.1.67.0
#26 0x00007ffff7a3bbe3 in PyObject_Call () from /lib64/libpython2.7.so.1.0
#27 0x00007ffff7afd992 in PyEval_EvalFrameEx () from /lib64/libpython2.7.so.1.0
#28 0x00007ffff7b002f9 in PyEval_EvalFrameEx () from /lib64/libpython2.7.so.1.0
#29 0x00007ffff7b002f9 in PyEval_EvalFrameEx () from /lib64/libpython2.7.so.1.0
#30 0x00007ffff7b002f9 in PyEval_EvalFrameEx () from /lib64/libpython2.7.so.1.0
#31 0x00007ffff7b02988 in PyEval_EvalCodeEx () from /lib64/libpython2.7.so.1.0
#32 0x00007ffff7b02b99 in PyEval_EvalCode () from /lib64/libpython2.7.so.1.0
#33 0x00007ffff7b08e2f in run_mod () from /lib64/libpython2.7.so.1.0
#34 0x00007ffff7b08dda in PyRun_FileExFlags () from /lib64/libpython2.7.so.1.0
#35 0x00007ffff7b08cce in PyRun_SimpleFileExFlags () from /lib64/libpython2.7.so.1.0
#36 0x00007ffff7b0ef8e in Py_Main () from /lib64/libpython2.7.so.1.0
#37 0x00007ffff6c93f2a in __libc_start_main () from /lib64/libc.so.6
#38 0x000055555555478a in _start ()

The environment used can be found here:
https://github.com/deepaksirone/mtech-thesis/tree/master/uclid_programs/gen_uclid5

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions