stack overflow

[adl]

While testing the Chomp specification at SYNTCOMP/benchmarks#42 for N=3, M=4, I could reliably trigger a SegFault from LydiaSyft.

I ran it through gdb to find that the issue was a stack overflow in MONA.

(abbreviated) stack trace

#0  0x00007ffff7aad3bb in _int_free (av=0x7ffff7bf1ac0 <main_arena>, p=0x555609c45e80,
    have_lock=0) at ./malloc/malloc.c:4699
#1  __GI___libc_free (mem=mem@entry=0x555609c45e90) at ./malloc/malloc.c:3476
#2  0x00005555558e0d15 in mem_free (x=x@entry=0x555609c45e90) at mem.c:70
#3  0x00005555558dfa17 in kill_trace (t=0x555609c45e90) at bdd_trace.c:109
#4  kill_trace (t=0x555609c45e90) at bdd_trace.c:105
#5  kill_trace (t=0x555609c45eb0) at bdd_trace.c:108
#6  kill_trace (t=0x555609c45eb0) at bdd_trace.c:105
#7  kill_trace (t=0x555609c45ed0) at bdd_trace.c:108
#8  kill_trace (t=0x555609c45ed0) at bdd_trace.c:105
#9  0x00005555558dfa07 in kill_trace (t=0x555609c45ef0) at bdd_trace.c:108
[...]
#55 kill_trace (t=0x555609c461d0) at bdd_trace.c:108
#56 kill_trace (t=0x555609c461d0) at bdd_trace.c:105
#57 kill_paths (p=0x555609c45e70) at bdd_trace.c:116
#58 0x00005555558e0437 in kill_paths (p=0x555609c45ad0) at bdd_trace.c:117
#59 kill_paths (p=<optimized out>) at bdd_trace.c:117
#60 kill_paths (p=0x555609c466f0) at bdd_trace.c:117
[...]
#407344 kill_paths (p=0x55561d212330) at bdd_trace.c:117
#407345 kill_paths (p=0x55561d212030) at bdd_trace.c:117
#407346 0x00005555557f19f7 in whitemech::lydia::dfa_concatenate(DFA*, DFA*, int, int*) ()
#407347 0x00005555557fef4c in whitemech::lydia::ComposeDFARegexVisitor::test_free_star_(whitemewhitemech::lydia::StarRegExp const&) ()
#407348 0x00005555557ff200 in whitemech::lydia::ComposeDFAVisitor::visit(whitemech::lydia::LDLfBox const&) ()
#407349 0x00005555557feb18 in whitemech::lydia::ComposeDFAVisitor::apply(whitemech::lydia::LDLfFormula const&) ()
#407350 0x00005555558033cc in DFA* whitemech::lydia::dfa_and_or<whitemech::lydia::LDLfFormula const, &whitemech::lydia::dfaLDLfTrue, (dfaProductType)8, false>(std::set<std::shared_ptr<whitemech::lydia::LDLfFormula const>, whitemech::lydia::SharedComparator, std::allocator<std::shared_ptr<whitemech::lydia::LDLfFormula const> > >, whitemech::lydia::AComposeDFAVisitor&) ()
#407351 0x000055555580120a in whitemech::lydia::ComposeDFAVisitor::visit(whitemech::lydia::LDLfAnd const&) ()
#407352 0x00005555557feb18 in whitemech::lydia::ComposeDFAVisitor::apply(whitemech::lydia::LDLfFormula const&) ()
#407353 0x000055555580394c in DFA* whitemech::lydia::dfa_and_or<whitemech::lydia::LDLfFormula const, &whitemech::lydia::dfaLDLfFalse, (dfaProductType)14, true>(std::set<std::shared_ptr<whitemech::lydia::LDLfFormula const>, whitemech::lydia::SharedComparator, std::allocator<std::shared_ptr<whitemech::lydia::LDLfFormula const> > >, whitemech::lydia::AComposeDFAVisitor&) ()
#407354 0x000055555580137a in whitemech::lydia::ComposeDFAVisitor::visit(whitemech::lydia::LDLfOr const&) ()
#407355 0x00005555557feb18 in whitemech::lydia::ComposeDFAVisitor::apply(whitemech::lydia::LDLfFormula const&) ()
#407356 0x00005555558033cc in DFA* whitemech::lydia::dfa_and_or<whitemech::lydia::LDLfFormula const, &whitemech::lydia::dfaLDLfTrue, (dfaProductType)8, false>(std::set<std::shared_ptr<whitemech::lydia::LDLfFormula const>, whitemech::lydia::SharedComparator, std::allocator<std::shared_ptr<whitemech::lydia::LDLfFormula const> > >, whitemech::lydia::AComposeDFAVisitor&) ()
#407357 0x000055555580120a in whitemech::lydia::ComposeDFAVisitor::visit(whitemech::lydia::LDLfAnd const&) ()
#407358 0x0000555555801926 in whitemech::lydia::CompositionalStrategy::to_dfa_internal(whitemech::lydia::LDLfFormula const&, std::set<std::shared_ptr<whitemech::lydia::PropositionalAtom const>, whitemech::lydia::SharedComparator, std::allocator<std::shared_ptr<whitemech::lydia::PropositionalAtom const> > >) ()
#407359 0x0000555555801e4d in whitemech::lydia::CompositionalStrategy::to_dfa(whitemech::lydia::LDLfFormula const&) ()
#407360 0x0000555555792d89 in Syft::ExplicitStateDfa::dfa_of_formula(whitemech::lydia::LTLfFormula const&) ()
#407361 0x0000555555787fa0 in Syft::do_dfa_construction(whitemech::lydia::LTLfFormula const&, std::shared_ptr<Syft::VarMgr> const&) ()
#407362 0x0000555555778e8a in Syft::BaseRunner::do_dfa_construction_() const ()
#407363 0x00005555557862d6 in Syft::SynthesisRunner::run() ()
#407364 0x000055555572812f in main ()

The culprit is the following code in MONA:

void kill_trace(trace_descr t)
{
  if (t) {
    kill_trace (t->next);
    mem_free(t);
  }
}

void kill_paths(paths p)
{
  if (p) {
    kill_trace (p->trace);
    kill_paths (p->next);
    mem_free(p);
  }
}

It seems to me that these two functions would be best written as while loops, especially as this example seems to be dealing with a list of over 400k paths...