diff --git a/NEWS b/NEWS index ad362d97d..1a93911d9 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,11 @@ New in spot 2.7.0.dev (not yet release) + Build + + - Work around GCC bug #89303, that causes memory leaks and std::weak_bad_ptr + exceptions when Spot is compiled with the version of g++ 8.2 currently + distributed with Debian (starting with 8.2.0-15). + Python: - The following methods of spot::bdd_dict are now usable in Python when diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index a6cebb285..96b946f4c 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014-2018 Laboratoire de +// Copyright (C) 2011, 2012, 2014-2019 Laboratoire de // Recherche et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -1106,7 +1106,8 @@ namespace spot dict->unregister_all_my_variables(iface.get()); throw; } - auto res = std::make_shared(iface, dict, ps, dead, compress); + auto res = SPOT_make_shared_enabled__(spins_kripke, + iface, dict, ps, dead, compress); // All atomic propositions have been registered to the bdd_dict // for iface, but we also need to add them to the automaton so // twa::ap() works. diff --git a/spot/misc/common.hh b/spot/misc/common.hh index ef090e749..0fcf9a346 100644 --- a/spot/misc/common.hh +++ b/spot/misc/common.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -176,3 +176,26 @@ namespace spot } }; } + +// This is a workaround for the issue described in GNU GCC bug 89303. +// https://gcc.gnu.org/bugzilla/show_bug.cgi?id=89303 +// +// In brief: with some version of gcc distributed by Debian unstable +// and that correspond to something a bit newer than 8.2.1 (Debian is +// tracking the gcc-8-branch instead of following releases), mixing +// make_shared with enable_shared_from_this produces memory leaks or +// bad_weak_ptr exceptions. +// +// Our workaround is simply to avoid calling make_shared in those +// cases. +// +// The use of "enabled" in the macro name is just here to remember +// that we only need this macro for classes that inherit from +// enable_shared_from_this. +#if __GNUC__ == 8 && __GNUC_MINOR__ == 2 +# define SPOT_make_shared_enabled__(TYPE, ...) \ + std::shared_ptr(new TYPE(__VA_ARGS__)) +#else +# define SPOT_make_shared_enabled__(TYPE, ...) \ + std::make_shared(__VA_ARGS__) +#endif diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh index 3d020af4f..9daa4975d 100644 --- a/spot/twa/taatgba.hh +++ b/spot/twa/taatgba.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011-2018 Laboratoire de Recherche et Développement de +// Copyright (C) 2009, 2011-2019 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -319,7 +319,7 @@ namespace spot inline taa_tgba_string_ptr make_taa_tgba_string(const bdd_dict_ptr& dict) { - return std::make_shared(dict); + return SPOT_make_shared_enabled__(taa_tgba_string, dict); } class SPOT_API taa_tgba_formula final: @@ -344,6 +344,6 @@ namespace spot inline taa_tgba_formula_ptr make_taa_tgba_formula(const bdd_dict_ptr& dict) { - return std::make_shared(dict); + return SPOT_make_shared_enabled__(taa_tgba_formula, dict); } } diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 97a9908ec..4c5218306 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -1031,7 +1031,7 @@ namespace spot { if (max_states == -1U && !preserve_names) if (auto a = std::dynamic_pointer_cast(aut)) - return std::make_shared(a, p); + return SPOT_make_shared_enabled__(twa_graph, a, p); return copy(aut, p, preserve_names, max_states); } } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 215f9d522..fcbdb97d8 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de l'Epita. +// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -714,11 +714,20 @@ namespace spot const char* opt = nullptr) const; }; + // This is a workaround for +#if __GNUC__ == 8 && __GNUC_MINOR__ == 2 +# define SPOT_make_twa_graph__(...) \ + std::shared_ptr(new twa_graph(__VA_ARGS__)) +#else +# define SPOT_make_twa_graph__(...) \ + std::make_shared(__VA_ARGS__) +#endif + /// \ingroup twa_representation /// \brief Build an explicit automaton from all states of \a aut, inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict) { - return std::make_shared(dict); + return SPOT_make_shared_enabled__(twa_graph, dict); } /// \ingroup twa_representation @@ -726,7 +735,7 @@ namespace spot inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut, twa::prop_set p) { - return std::make_shared(aut, p); + return SPOT_make_shared_enabled__(twa_graph, aut, p); } /// \ingroup twa_representation @@ -734,7 +743,7 @@ namespace spot inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut, twa::prop_set p) { - return std::make_shared(aut, p); + return SPOT_make_shared_enabled__(twa_graph, aut, p); } /// \ingroup twa_representation diff --git a/spot/twa/twaproduct.hh b/spot/twa/twaproduct.hh index 24cec7034..e16cc9cab 100644 --- a/spot/twa/twaproduct.hh +++ b/spot/twa/twaproduct.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -131,7 +131,7 @@ namespace spot inline twa_product_ptr otf_product(const const_twa_ptr& left, const const_twa_ptr& right) { - return std::make_shared(left, right); + return SPOT_make_shared_enabled__(twa_product, left, right); } /// \brief on-the-fly TGBA product with forced initial states @@ -140,7 +140,7 @@ namespace spot const state* left_init, const state* right_init) { - return std::make_shared(left, right, - left_init, right_init); + return SPOT_make_shared_enabled__(twa_product_init, + left, right, left_init, right_init); } } diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index cf907779f..1f0d3c495 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2016-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -850,29 +850,38 @@ namespace spot } // anonymous namespace + template + using cna = couvreur99_new; + template + using cne = couvreur99_new; + + emptiness_check_ptr + get_couvreur99_new_abstract(const const_twa_ptr& a, option_map o) + { + // NB: The order of the if's matter. + if (a->prop_terminal()) + return SPOT_make_shared_enabled__(cna, a, o); + if (a->prop_weak()) + return SPOT_make_shared_enabled__(cna, a, o); + return SPOT_make_shared_enabled__(cna, a, o); + } + emptiness_check_ptr get_couvreur99_new(const const_twa_ptr& a, spot::option_map o) { const_twa_graph_ptr ag = std::dynamic_pointer_cast(a); - if (ag) - // the automaton is explicit + if (ag) // the automaton is explicit { // NB: The order of the if's matter. if (a->prop_terminal()) - return std::make_shared>(ag, o); + return SPOT_make_shared_enabled__(cne, ag, o); if (a->prop_weak()) - return std::make_shared>(ag, o); - return std::make_shared>(ag, o); + return SPOT_make_shared_enabled__(cne, ag, o); + return SPOT_make_shared_enabled__(cne, ag, o); } - else - // the automaton is abstract + else // the automaton is abstract { - // NB: The order of the if's matter. - if (a->prop_terminal()) - return std::make_shared>(a, o); - if (a->prop_weak()) - return std::make_shared>(a, o); - return std::make_shared>(a, o); + return get_couvreur99_new_abstract(a, o); } } @@ -882,14 +891,4 @@ namespace spot return get_couvreur99_new(a, spot::option_map())->check(); } - emptiness_check_ptr - get_couvreur99_new_abstract(const const_twa_ptr& a, option_map o) - { - if (a->prop_terminal()) - return std::make_shared>(a, o); - if (a->prop_weak()) - return std::make_shared>(a, o); - return std::make_shared>(a, o); - } - } // namespace spot diff --git a/spot/twaalgos/gtec/gtec.cc b/spot/twaalgos/gtec/gtec.cc index 83d5c6326..4b4a827de 100644 --- a/spot/twaalgos/gtec/gtec.cc +++ b/spot/twaalgos/gtec/gtec.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2014-2016, 2018 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011, 2014-2016, 2018-2019 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -613,8 +613,8 @@ namespace spot couvreur99(const const_twa_ptr& a, option_map o) { if (o.get("shy")) - return std::make_shared(a, o); - return std::make_shared(a, o); + return SPOT_make_shared_enabled__(couvreur99_check_shy, a, o); + return SPOT_make_shared_enabled__(couvreur99_check, a, o); } } diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc index 2ad80e796..d756a1bc4 100644 --- a/spot/twaalgos/gv04.cc +++ b/spot/twaalgos/gv04.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2011, 2013-2018 Laboratoire de +// Copyright (C) 2008, 2010, 2011, 2013-2019 Laboratoire de // recherche et développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -411,6 +411,6 @@ namespace spot emptiness_check_ptr explicit_gv04_check(const const_twa_ptr& a, option_map o) { - return std::make_shared(a, o); + return SPOT_make_shared_enabled__(gv04, a, o); } } diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index 1a86a154a..50be6086b 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2018 Laboratoire de recherche et +// Copyright (C) 2011, 2013-2019 Laboratoire de recherche et // développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -588,14 +588,18 @@ namespace spot emptiness_check_ptr explicit_magic_search(const const_twa_ptr& a, option_map o) { - return std::make_shared>(a, 0, o); + return + SPOT_make_shared_enabled__(magic_search_, + a, 0, o); } emptiness_check_ptr bit_state_hashing_magic_search(const const_twa_ptr& a, size_t size, option_map o) { - return std::make_shared>(a, size, o); + return + SPOT_make_shared_enabled__(magic_search_, + a, size, o); } emptiness_check_ptr diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index 3c2d8dc00..fbea7dfae 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2018 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -680,14 +680,18 @@ namespace spot emptiness_check_ptr explicit_se05_search(const const_twa_ptr& a, option_map o) { - return std::make_shared>(a, 0, o); + return + SPOT_make_shared_enabled__(se05_search, + a, 0, o); } emptiness_check_ptr bit_state_hashing_se05_search(const const_twa_ptr& a, size_t size, option_map o) { - return std::make_shared>(a, size, o); + return + SPOT_make_shared_enabled__(se05_search, + a, size, o); } emptiness_check_ptr diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index 61e041776..4ea8ab0bb 100644 --- a/spot/twaalgos/tau03.cc +++ b/spot/twaalgos/tau03.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2018 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2019 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -376,7 +376,9 @@ namespace spot emptiness_check_ptr explicit_tau03_search(const const_twa_ptr& a, option_map o) { - return std::make_shared>(a, 0, o); + return + SPOT_make_shared_enabled__(tau03_search, + a, 0, o); } } diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index 038ebabe4..e1c4e5885 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2018 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -563,9 +563,8 @@ namespace spot emptiness_check_ptr explicit_tau03_opt_search(const const_twa_ptr& a, option_map o) { - return - std::make_shared>(a, - 0, o); + return SPOT_make_shared_enabled__ + (tau03_opt_search, a, 0, o); } }