From 3c3b23bfa46cc46dd3b1585f1a44958312c47a3c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Mar 2004 15:02:57 +0000 Subject: [PATCH] * src/misc/freelist.cc (free_list::remove): Work around invalidated iterators. * tgba/bdddict.cc (unregister_variable): New methods, extracted from ... (bdd_dict::unregister_all_my_variables): ... here. * tgba/bdddict.hh (unregister_variable): Declare them. --- ChangeLog | 9 +++ src/misc/freelist.cc | 8 ++- src/tgba/bdddict.cc | 127 ++++++++++++++++++++++++------------------- src/tgba/bdddict.hh | 6 +- 4 files changed, 90 insertions(+), 60 deletions(-) diff --git a/ChangeLog b/ChangeLog index d408324a5..5e9bc4896 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-03-25 Alexandre Duret-Lutz + + * src/misc/freelist.cc (free_list::remove): Work around + invalidated iterators. + * tgba/bdddict.cc (unregister_variable): New methods, + extracted from ... + (bdd_dict::unregister_all_my_variables): ... here. + * tgba/bdddict.hh (unregister_variable): Declare them. + 2004-03-23 Alexandre DURET-LUTZ * src/misc/freelist.hh (free_list::remove, free_list::insert): New diff --git a/src/misc/freelist.cc b/src/misc/freelist.cc index 52c5a8638..ef82984bc 100644 --- a/src/misc/freelist.cc +++ b/src/misc/freelist.cc @@ -131,13 +131,15 @@ namespace spot void free_list::remove(int base, int n) { - free_list_type::iterator cur; + free_list_type::iterator cur = fl.begin(); int end = base + n; - for (cur = fl.begin(); cur != fl.end() && cur->first <= end; ++cur) + while (cur != fl.end() && cur->first <= end) { int cend = cur->first + cur->second; + // Remove may invalidate the current iterator, so advance it first. + free_list_type::iterator old = cur++; if (cend >= end) - remove(cur, base, std::max(n, cend - base)); + remove(old, base, std::max(n, cend - base)); } } diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 8ac4f44ab..554dbec53 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -172,6 +172,76 @@ namespace spot free_annonymous_list_of[for_me] = free_annonymous_list_of[from_other]; } + void + bdd_dict::unregister_variable(int var, const void* me) + { + vr_map::iterator i = var_refs.find(var); + assert(i != var_refs.end()); + unregister_variable(i, me); + } + + void + bdd_dict::unregister_variable(vr_map::iterator& cur, const void* me) + { + ref_set& s = cur->second; + ref_set::iterator si = s.find(me); + if (si == s.end()) + return; + s.erase(si); + if (! s.empty()) + return; + + // ME was the last user of this variable. + // Let's free it. First, we need to find + // if this is a Now, a Var, or an Acc variable. + int var = cur->first; + int n = 1; + const ltl::formula* f = 0; + vf_map::iterator vi = var_formula_map.find(var); + if (vi != var_formula_map.end()) + { + f = vi->second; + var_map.erase(f); + var_formula_map.erase(vi); + } + else + { + vi = now_formula_map.find(var); + if (vi != now_formula_map.end()) + { + f = vi->second; + now_map.erase(f); + now_formula_map.erase(vi); + n = 2; + bdd_setpair(next_to_now, var + 1, var + 1); + bdd_setpair(now_to_next, var, var); + } + else + { + vi = acc_formula_map.find(var); + if (vi != acc_formula_map.end()) + { + f = vi->second; + acc_map.erase(f); + acc_formula_map.erase(vi); + } + else + { + free_annonymous_list_of_type::iterator i; + for (i = free_annonymous_list_of.begin(); + i != free_annonymous_list_of.end(); ++i) + i->second.remove(var, n); + } + } + } + // Actually release the associated BDD variables, and the + // formula itself. + release_variables(var, n); + if (f) + ltl::destroy(f); + var_refs.erase(cur); + } + void bdd_dict::unregister_all_my_variables(const void* me) { @@ -181,62 +251,7 @@ namespace spot // Increment i++ now, we will possibly erase // the current node (which would invalidate the iterator). vr_map::iterator cur = i++; - - ref_set& s = cur->second; - ref_set::iterator si = s.find(me); - if (si == s.end()) - continue; - s.erase(si); - if (! s.empty()) - continue; - // ME was the last user of this variable. - // Let's free it. First, we need to find - // if this is a Now, a Var, or an Acc variable. - int var = cur->first; - int n = 1; - const ltl::formula* f; - vf_map::iterator vi = var_formula_map.find(var); - if (vi != var_formula_map.end()) - { - f = vi->second; - var_map.erase(f); - var_formula_map.erase(vi); - } - else - { - vi = now_formula_map.find(var); - if (vi != now_formula_map.end()) - { - f = vi->second; - now_map.erase(f); - now_formula_map.erase(vi); - n = 2; - bdd_setpair(next_to_now, var + 1, var + 1); - bdd_setpair(now_to_next, var, var); - } - else - { - vi = acc_formula_map.find(var); - if (vi != acc_formula_map.end()) - { - f = vi->second; - acc_map.erase(f); - acc_formula_map.erase(vi); - } - else - { - free_annonymous_list_of_type::iterator i; - for (i = free_annonymous_list_of.begin(); - i != free_annonymous_list_of.end(); ++i) - i->second.remove(var, n); - } - } - } - // Actually release the associated BDD variables, and the - // formula itself. - release_variables(var, n); - ltl::destroy(f); - var_refs.erase(cur); + unregister_variable(cur, me); } free_annonymous_list_of.erase(me); } diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 2b3236f85..0591ebcd8 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -135,11 +135,14 @@ namespace spot /// is deleted if \a from_other is still alive. void register_all_variables_of(const void* from_other, const void* for_me); - /// \brief Release the variables used by object. + /// \brief Release all variables used by an object. /// /// Usually called in the destructor if \a me. void unregister_all_my_variables(const void* me); + /// \brief Release a variable used by \a me. + void unregister_variable(int var, const void* me); + /// @{ /// Check whether formula \a f has already been registered by \a by_me. bool is_registered_proposition(const ltl::formula* f, const void* by_me); @@ -164,6 +167,7 @@ namespace spot typedef Sgi::hash_map vr_map; vr_map var_refs; + void unregister_variable(vr_map::iterator& cur, const void* me); class annon_free_list : public spot::free_list {