Comments (5)
works on master
but not on backport
from hw-cbmc.
Do these work with 4.2?
from hw-cbmc.
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
.
from hw-cbmc.
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
from hw-cbmc.
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)
from hw-cbmc.
Related Issues (20)
- segmentation fault on regression test HOT 1
- Setup CBMC as git submodule for HW-CBMC HOT 1
- Parser exhausts memory on large SMV files (converted from AIG) HOT 1
- EBMC/ic3 fails to analyze SMV converted from AIG HOT 1
- EBMC/ic3 fails to verify property of `ring_buffer` example HOT 3
- EBMC fails to read SMV files with `.` in name
- Memory Exhaustion in SMV parser
- EBMC 4.4 fails to analyze VHDL regression tests
- Assertion violation `Assertion `!isEliminated(v)' failed.` in 4.4 HOT 1
- issue in implication operator HOT 16
- Implement circuit reduction HOT 2
- Invariant Violation Report HOT 2
- Solving time problem
- Verilog Parser 4.4 has problems with file HOT 3
- PARSING ERROR syntax error before '__value' when verifying hardware of DUAL_PATH_ADDER of the FM16 paper's benchmark. HOT 2
- Problems compiling current EBMC HOT 3
- questions about co-verification tool HW-CBMC supporting for concurrency scenarios
- mv: cannot stat 'y.tab.cpp.h': No such file or directory HOT 1
- Could not parse macro in verilog file HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from hw-cbmc.