segfault in do_g_f_terminal_inplace
There is a quite serious issue in do_g_f_terminal_inplace which iterates over an automaton that is being modified. When if the edge vector is reallocated during that process, it can lead to a segfault.
This is currently visible on the alpine builds, where ltl2tgba2.test fails. I'm not sure why this was not visible before.
/build/spot/bin # ../libtool e valgrind ./ltl2tgba 'GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3))'
==50824== Memcheck, a memory error detector
==50824== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==50824== Using Valgrind-3.16.1 and LibVEX; rerun with -h for copyright info
==50824== Command: /build/spot/bin/.libs/lt-ltl2tgba GF(!(p1\ \<-\>\ Xp1)\ |\ !(p0\ \<-\>\ Xp0)\ |\ !(p2\ \<-\>\ Xp2)\ |\ !(p3\ \<-\>\ Xp3))
==50824==
==50824== Invalid read of size 4
==50824== at 0x4A2C7AA: spot::(anonymous namespace)::do_g_f_terminal_inplace(spot::scc_info&, bool) (gfguarantee.cc:361)
==50824== by 0x4A2E3CD: spot::gf_guarantee_to_ba_maybe(spot::formula, std::shared_ptr<spot::bdd_dict> const&, bool, bool) (gfguarantee.cc:465)
==50824== by 0x4B32ADB: spot::translator::run_aux(spot::formula) (translate.cc:385)
==50824== by 0x4B34385: spot::translator::run(spot::formula*) (translate.cc:523)
==50824== by 0x1110D4: (anonymous namespace)::trans_processor::process_formula(spot::formula, char const*, int) (ltl2tgba.cc:156)
==50824== by 0x119596: job_processor::process_string(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, char const*, int) (common_finput.cc:130)
==50824== by 0x11A4D4: job_processor::run() (common_finput.cc:362)
==50824== by 0x111733: main::{lambda()#1}::operator()() const (ltl2tgba.cc:193)
==50824== by 0x1117E4: __invoke_impl<int, main(int, char**)::<lambda()>&> (invoke.h:60)
==50824== by 0x1117E4: __invoke_r<int, main(int, char**)::<lambda()>&> (invoke.h:113)
==50824== by 0x1117E4: std::_Function_handler<int (), main::{lambda()#1}>::_M_invoke(std::_Any_data const&) (std_function.h:291)
==50824== by 0x11AD62: operator() (std_function.h:622)
==50824== by 0x11AD62: protected_main(char**, std::function<int ()>) (common_setup.cc:205)
==50824== by 0x110D65: main (ltl2tgba.cc:173)
==50824== Address 0x5bb27d8 is 456 bytes inside a block of size 1,680 free'd
==50824== at 0x48A2DDA: operator delete(void*, unsigned long) (vg_replace_malloc.c:593)
==50824== by 0x4927AE3: deallocate (new_allocator.h:133)
==50824== by 0x4927AE3: deallocate (alloc_traits.h:492)
==50824== by 0x4927AE3: _M_deallocate (stl_vector.h:354)
==50824== by 0x4927AE3: void std::vector<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >, std::allocator<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> > > >::_M_realloc_insert<unsigned int&, int, unsigned int&, bdd&, spot::acc_cond::mark_t&>(__gnu_cxx::__normal_iterator<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >*, std::vector<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >, std::allocator<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> > > > >, unsigned int&, int&&, unsigned int&, bdd&, spot::acc_cond::mark_t&) (vector.tcc:500)
==50824== by 0x4927BB5: spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >& std::vector<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >, std::allocator<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> > > >::emplace_back<unsigned int&, int, unsigned int&, bdd&, spot::acc_cond::mark_t&>(unsigned int&, int&&, unsigned int&, bdd&, spot::acc_cond::mark_t&) (vector.tcc:121)
==50824== by 0x4A2C830: new_edge<bdd&, spot::acc_cond::mark_t&> (graph.hh:775)
==50824== by 0x4A2C830: new_edge (twagraph.hh:449)
==50824== by 0x4A2C830: spot::(anonymous namespace)::do_g_f_terminal_inplace(spot::scc_info&, bool) (gfguarantee.cc:361)
==50824== by 0x4A2E3CD: spot::gf_guarantee_to_ba_maybe(spot::formula, std::shared_ptr<spot::bdd_dict> const&, bool, bool) (gfguarantee.cc:465)
==50824== by 0x4B32ADB: spot::translator::run_aux(spot::formula) (translate.cc:385)
==50824== by 0x4B34385: spot::translator::run(spot::formula*) (translate.cc:523)
==50824== by 0x1110D4: (anonymous namespace)::trans_processor::process_formula(spot::formula, char const*, int) (ltl2tgba.cc:156)
==50824== by 0x119596: job_processor::process_string(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, char const*, int) (common_finput.cc:130)
==50824== by 0x11A4D4: job_processor::run() (common_finput.cc:362)
==50824== by 0x111733: main::{lambda()#1}::operator()() const (ltl2tgba.cc:193)
==50824== by 0x1117E4: __invoke_impl<int, main(int, char**)::<lambda()>&> (invoke.h:60)
==50824== by 0x1117E4: __invoke_r<int, main(int, char**)::<lambda()>&> (invoke.h:113)
==50824== by 0x1117E4: std::_Function_handler<int (), main::{lambda()#1}>::_M_invoke(std::_Any_data const&) (std_function.h:291)
==50824== Block was alloc'd at
==50824== at 0x48A1D3A: operator new(unsigned long) (vg_replace_malloc.c:342)
==50824== by 0x4927F15: allocate (new_allocator.h:115)
==50824== by 0x4927F15: allocate (alloc_traits.h:460)
==50824== by 0x4927F15: _M_allocate (stl_vector.h:346)
==50824== by 0x4927F15: void std::vector<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >, std::allocator<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> > > >::_M_realloc_insert<unsigned int&, int, unsigned int&, bdd&>(__gnu_cxx::__normal_iterator<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >*, std::vector<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >, std::allocator<spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> > > > >, unsigned int&, int&&, unsigned int&, bdd&) (vector.tcc:440)
==50824== by 0x4A7742C: emplace_back<unsigned int&, int, unsigned int&, bdd&> (vector.tcc:121)
==50824== by 0x4A7742C: new_edge<bdd&> (graph.hh:775)
==50824== by 0x4A7742C: new_acc_edge (twagraph.hh:458)
==50824== by 0x4A7742C: build_result (minimize.cc:143)
==50824== by 0x4A7742C: spot::(anonymous namespace)::minimize_dfa(std::shared_ptr<spot::twa_graph const> const&, std::set<unsigned int, std::less<unsigned int>, std::allocator<unsigned int> >*, std::set<unsigned int, std::less<unsigned int>, std::allocator<unsigned int> >*) (minimize.cc:336)
==50824== by 0x4A79206: spot::minimize_wdba(std::shared_ptr<spot::twa_graph const> const&, spot::output_aborter const*) (minimize.cc:545)
==50824== by 0x4A7A1F4: spot::minimize_obligation(std::shared_ptr<spot::twa_graph const> const&, spot::formula, std::shared_ptr<spot::twa_graph const>, bool, spot::output_aborter const*) (minimize.cc:643)
==50824== by 0x4A2E0B9: spot::gf_guarantee_to_ba_maybe(spot::formula, std::shared_ptr<spot::bdd_dict> const&, bool, bool) (gfguarantee.cc:459)
==50824== by 0x4B32ADB: spot::translator::run_aux(spot::formula) (translate.cc:385)
==50824== by 0x4B34385: spot::translator::run(spot::formula*) (translate.cc:523)
==50824== by 0x1110D4: (anonymous namespace)::trans_processor::process_formula(spot::formula, char const*, int) (ltl2tgba.cc:156)
==50824== by 0x119596: job_processor::process_string(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, char const*, int) (common_finput.cc:130)
==50824== by 0x11A4D4: job_processor::run() (common_finput.cc:362)
==50824== by 0x111733: main::{lambda()#1}::operator()() const (ltl2tgba.cc:193)
==50824==