alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

work around gcc 8.2.1+ bug #89303

Browse source 
Do not call std::make_shared on classes inheriting from
std::enable_shared_from_this when compiling with g++ 8.2.

* NEWS: Mention the bug.
* spot/misc/common.hh (SPOT_make_shared_enabled__): New macro.
* spot/twa/twagraph.cc, spot/twa/twagraph.hh, spot/twa/twaproduct.hh,
spot/twa/taatgba.hh, spot/twaalgos/couvreurnew.cc,
spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc,
spot/twaalgos/tau03opt.cc, spot/twaalgos/gv04.cc,
spot/ltsmin/ltsmin.cc, spot/twaalgos/gtec/gtec.cc: Use it.
This commit is contained in:
Alexandre Duret-Lutz 2019-02-12 17:58:38 +01:00
parent d0b9806500
commit a86925e20e
14 changed files with 105 additions and 58 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -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

5
spot/ltsmin/ltsmin.cc
View file

@ -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<spins_kripke>(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.

25
spot/misc/common.hh
View file

@ -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<TYPE>(new TYPE(__VA_ARGS__))
#else
# define SPOT_make_shared_enabled__(TYPE, ...) \
std::make_shared<TYPE>(__VA_ARGS__)
#endif

6
spot/twa/taatgba.hh
View file

@ -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<taa_tgba_string>(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<taa_tgba_formula>(dict);
return SPOT_make_shared_enabled__(taa_tgba_formula, dict);
}
}

4
spot/twa/twagraph.cc
View file

@ -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<const twa_graph>(aut))
return std::make_shared<twa_graph>(a, p);
return SPOT_make_shared_enabled__(twa_graph, a, p);
return copy(aut, p, preserve_names, max_states);
}
}

17
spot/twa/twagraph.hh
View file

@ -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<twa_graph>(new twa_graph(__VA_ARGS__))
#else
# define SPOT_make_twa_graph__(...) \
std::make_shared<twa_graph>(__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<twa_graph>(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<twa_graph>(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<twa_graph>(aut, p);
return SPOT_make_shared_enabled__(twa_graph, aut, p);
}
/// \ingroup twa_representation

8
spot/twa/twaproduct.hh
View file

@ -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<twa_product>(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<twa_product_init>(left, right,
left_init, right_init);
return SPOT_make_shared_enabled__(twa_product_init,
left, right, left_init, right_init);
}
}

47
spot/twaalgos/couvreurnew.cc
View file

@ -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<twa_strength strength>
using cna = couvreur99_new<false, strength>;
template<twa_strength strength>
using cne = couvreur99_new<true, strength>;
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<TERMINAL>, a, o);
if (a->prop_weak())
return SPOT_make_shared_enabled__(cna<WEAK>, a, o);
return SPOT_make_shared_enabled__(cna<STRONG>, 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<const twa_graph>(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<couvreur99_new<true, TERMINAL>>(ag, o);
return SPOT_make_shared_enabled__(cne<TERMINAL>, ag, o);
if (a->prop_weak())
return std::make_shared<couvreur99_new<true, WEAK>>(ag, o);
return std::make_shared<couvreur99_new<true, STRONG>>(ag, o);
return SPOT_make_shared_enabled__(cne<WEAK>, ag, o);
return SPOT_make_shared_enabled__(cne<STRONG>, 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<couvreur99_new<false, TERMINAL>>(a, o);
if (a->prop_weak())
return std::make_shared<couvreur99_new<false, WEAK>>(a, o);
return std::make_shared<couvreur99_new<false, STRONG>>(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<couvreur99_new<false, TERMINAL>>(a, o);
if (a->prop_weak())
return std::make_shared<couvreur99_new<false, WEAK>>(a, o);
return std::make_shared<couvreur99_new<false, STRONG>>(a, o);
}
} // namespace spot

8
spot/twaalgos/gtec/gtec.cc
View file

@ -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<couvreur99_check_shy>(a, o);
return std::make_shared<couvreur99_check>(a, o);
return SPOT_make_shared_enabled__(couvreur99_check_shy, a, o);
return SPOT_make_shared_enabled__(couvreur99_check, a, o);
}
}

4
spot/twaalgos/gv04.cc
View file

@ -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<gv04>(a, o);
return SPOT_make_shared_enabled__(gv04, a, o);
}
}

10
spot/twaalgos/magic.cc
View file

@ -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<magic_search_<explicit_magic_search_heap>>(a, 0, o);
return
SPOT_make_shared_enabled__(magic_search_<explicit_magic_search_heap>,
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<magic_search_<bsh_magic_search_heap>>(a, size, o);
return
SPOT_make_shared_enabled__(magic_search_<bsh_magic_search_heap>,
a, size, o);
}
emptiness_check_ptr

10
spot/twaalgos/se05.cc
View file

@ -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<se05_search<explicit_se05_search_heap>>(a, 0, o);
return
SPOT_make_shared_enabled__(se05_search<explicit_se05_search_heap>,
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<se05_search<bsh_se05_search_heap>>(a, size, o);
return
SPOT_make_shared_enabled__(se05_search<bsh_se05_search_heap>,
a, size, o);
}
emptiness_check_ptr

6
spot/twaalgos/tau03.cc
View file

@ -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<tau03_search<explicit_tau03_search_heap>>(a, 0, o);
return
SPOT_make_shared_enabled__(tau03_search<explicit_tau03_search_heap>,
a, 0, o);
}
}

7
spot/twaalgos/tau03opt.cc
View file

@ -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<tau03_opt_search<explicit_tau03_opt_search_heap>>(a,
0, o);
return SPOT_make_shared_enabled__
(tau03_opt_search<explicit_tau03_opt_search_heap>, a, 0, o);
}
}