segfault on typecheck

[mgudemann]

For some of the SMV models converted from Aiger format, EBMC fails with sefgault which typechecking.
The example is from http://www.cprover.org/ebmc/download/AIG_SMV_08.tar.gz

aig.zip

[mgudemann]

works on master but not on backport

[kroening]

Do these work with 4.2?

[mgudemann]

it does not occur with the 4.2 binaries
But I can reproduce on master and backport now. It appears on debug builds with -O0 -g.

My guess is that with these SMV files converted from aiger, there is a stack overflow problem. Every state-bit and every node has it own identifier and convert_define calls itself recursively if a used identifier is not yet converted. As its an unordered_map we use to iterate through, then although this is topologically sorted in AIG, it is not in EBMC.

This seems to be what gdb says:

#0  0x0000000000627d46 in std::__detail::_Equal_helper<dstringt, std::pair<dstringt const, smv_typecheckt::definet>, std::__detail::_Select1st, std::equal_to<dstringt>, unsigned long, true>::_S_equals (__eq=..., __extract=..., __k=..., __c=178846, __n=0xeebb510) at /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/hashtable_policy.h:1322
#1  0x0000000000627cb0 in std::__detail::_Hashtable_base<dstringt, std::pair<dstringt const, smv_typecheckt::definet>, std::__detail::_Select1st, std::equal_to<dstringt>, dstring_hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Hashtable_traits<true, false, true> >::_M_equals (this=0x7fffffffc9b0, __k=..., __c=178846, 
    __n=0xeebb510) at /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/hashtable_policy.h:1703
#2  0x0000000000627bda in std::_Hashtable<dstringt, std::pair<dstringt const, smv_typecheckt::definet>, std::allocator<std::pair<dstringt const, smv_typecheckt::definet> >, std::__detail::_Select1st, std::equal_to<dstringt>, dstring_hash, 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=0x7fffffffc9b0, __n=54380, __k=..., __code=178846)
    at /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/hashtable.h:1433
#3  0x0000000000627a5d in std::_Hashtable<dstringt, std::pair<dstringt const, smv_typecheckt::definet>, std::allocator<std::pair<dstringt const, smv_typecheckt::definet> >, std::__detail::_Select1st, std::equal_to<dstringt>, dstring_hash, 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=0x7fffffffc9b0, __bkt=54380, __key=..., __c=178846)
    at /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/hashtable.h:632
#4  0x0000000000627985 in std::_Hashtable<dstringt, std::pair<dstringt const, smv_typecheckt::definet>, std::allocator<std::pair<dstringt const, smv_typecheckt::definet> >, std::__detail::_Select1st, std::equal_to<dstringt>, dstring_hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true> >::find (this=0x7fffffffc9b0, __k=...) at /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/hashtable.h:1307
#5  0x00000000006256bd in std::unordered_map<dstringt, smv_typecheckt::definet, dstring_hash, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, smv_typecheckt::definet> > >::find (this=0x7fffffffc9b0, __x=...) at /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/unordered_map.h:615
#6  0x000000000061ef8b in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:632
#7  0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#8  0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#9  0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#10 0x000000000061efe0 in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:633
#11 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#12 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#13 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#14 0x000000000061efe0 in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:633
#15 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#16 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#17 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#18 0x000000000061efe0 in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:633
#19 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#20 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#21 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
----8<-----
---->8-----
#5145 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#5146 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#5147 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#5148 0x000000000061efe0 in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:633
#5149 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#5150 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#5151 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#5152 0x000000000061efe0 in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:633
#5153 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#5154 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#5155 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#5156 0x000000000061efe0 in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:633
#5157 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#5158 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#5159 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#5160 0x000000000061efe0 in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:633
#5161 0x000000000061e4bc in smv_typecheckt::typecheck_op (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:490
#5162 0x000000000061f2bc in smv_typecheckt::typecheck (this=0x7fffffffc7e0, expr=..., type=..., mode=smv_typecheckt::OTHER) at smv_typecheck.cpp:663
#5163 0x00000000006227e4 in smv_typecheckt::convert_define (this=0x7fffffffc7e0, identifier=...) at smv_typecheck.cpp:1320
#5164 0x0000000000623eef in smv_typecheckt::convert_defines (this=0x7fffffffc7e0, invar=std::vector of length 0, capacity 0) at smv_typecheck.cpp:1347
#5165 0x000000000062440c in smv_typecheckt::convert (this=0x7fffffffc7e0, smv_module=...) at smv_typecheck.cpp:1407
#5166 0x0000000000624d54 in smv_typecheckt::typecheck (this=0x7fffffffc7e0) at smv_typecheck.cpp:1479
#5167 0x0000000000706231 in typecheckt::typecheck_main (this=0x7fffffffc7e0) at typecheck.cpp:21

valgrind seems to have this opinion, too

Converting
Type-checking smv::main
==25482== Stack overflow in thread #1: can't grow stack to 0xffe801000
==25482== 
==25482== Process terminating with default action of signal 11 (SIGSEGV)
==25482==  Access not within mapped region at address 0xFFE801DC8
==25482== Stack overflow in thread #1: can't grow stack to 0xffe801000
==25482==    at 0x61EEDC: smv_typecheckt::typecheck(exprt&, typet const&, smv_typecheckt::modet) (smv_typecheck.cpp:626)
==25482==  If you believe this happened as a result of a stack
==25482==  overflow in your program's main thread (unlikely but
==25482==  possible), you can try to increase the size of the
==25482==  main thread stack using the --main-stacksize= flag.
==25482==  The main thread stack size used in this run was 8388608.
==25482== Stack overflow in thread #1: can't grow stack to 0xffe801000

I re-tested all AIG_SMV_08 files (with --bound 1), and with optimization settings it works on both master and the 4.4 binaries, with the exception of

Parsing intel048.aig.smv
file intel048.aig.smv line 271364: memory exhausted before `a471304'
PARSING ERROR

which also fails for 4.2

So the problem seems to be optimized away or at least much less problematic with optimization. I'd say we do the top-sort eventually in master but this is no blocker for 4.4.

[mgudemann]

I added a topological sort in diffblue/cbmc#1089, when adding a depth counter to convert_define and typecheck, we got initially the maxima of call depth for typecheck at 6399 for intel014.aig.smv, with the preceding topsort the call depth is 3. This also passes the smv models that failed before, like the attached one.
depth.zip

[mgudemann]

I retested this on current EBMC with an increased value for YYMAXDEPTH (cf. #233)

this leads to the following error

$ ebmc --k-induction AIG_SMV/dintel048.aig/intel048.aig.smv
using default bound 1
Parsing AIG_SMV/dintel048.aig/intel048.aig.smv
Converting
Type-checking smv::main
fish: Job 2, “ebmc --k-induction AIG_SMV/dint…” terminated by signal SIGSEGV (Address boundary error)