From a9fc213a442fe8d135171d0b4a164c5597be0539 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 Mar 2013 17:24:20 +0100 Subject: [PATCH] fix a memory leak in basic LTL simplifications When something like XFa & FXa is reduced, the subformulae XFa and FXa are both rewritten separately to XFa, and then the vector of arguments of the And operators, [XFa,XFa], is passed through a specialized loop that searches of the form X(...) that can potentially be simplified with some other terms. This loop converts the vector [XFa,XFa] into the set {XFa,XFa}={XFa} and forgot to deal with the case where the insertion would actually not add an existing subformula. * src/ltlvisit/simplify.cc: Fix the code for Or, and And. * src/ltltest/reduc0.test: New file, to test it. * src/ltltest/Makefile.am (TESTS): Add it. * src/ltltest/reduccmp.test: Add an extra test that does not trigger the bug (because reduccmp.test uses more than basic optimizations, and the implication-based simplifications are already able to detect that XFa and FXa are equivalent). --- src/ltltest/Makefile.am | 1 + src/ltltest/reduc0.test | 26 ++++++++++++++++++ src/ltltest/reduccmp.test | 3 +++ src/ltlvisit/simplify.cc | 57 ++++++++++++++++++++++++++++----------- 4 files changed, 72 insertions(+), 15 deletions(-) create mode 100755 src/ltltest/reduc0.test diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 5dc76cd75..18ebe32de 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -95,6 +95,7 @@ TESTS = \ isop.test \ syntimpl.test \ reduc.test \ + reduc0.test \ reducpsl.test \ reduccmp.test \ uwrm.test diff --git a/src/ltltest/reduc0.test b/src/ltltest/reduc0.test new file mode 100755 index 000000000..744f654c2 --- /dev/null +++ b/src/ltltest/reduc0.test @@ -0,0 +1,26 @@ +#! /bin/sh +# Copyright (C) 2013 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs || exit 1 +set -e + +# These two reductions used to cause a memory leak. +run 0 ../reduc 0 'XFa & FXa' 'XFa' +run 0 ../reduc 0 '(Xf W 0) | X(f W 0)' 'XGf' + diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index ef5117699..514074b02 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -99,6 +99,9 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'FX(a)' 'XF(a)' run 0 $x 'GX(a)' 'XG(a)' + run 0 $x '(Xf W 0) | X(f W 0)' 'XGf' + run 0 $x 'XFa & FXa' 'XFa' + run 0 $x 'GF(a | Xb)' 'GF(a | b)' run 0 $x 'GF(a | Fb)' 'GF(a | b)' run 0 $x 'GF(Xa | Fb)' 'GF(a | b)' diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 041f2e87a..873db091a 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -2600,6 +2600,8 @@ namespace spot { if (!(*res)[n]) continue; + if ((*res)[n]->is_X_free()) + continue; const formula* xarg = is_XWU((*res)[n]); if (xarg) @@ -2612,8 +2614,6 @@ namespace spot // - X(...) // - b | X(b R ...) // - b | X(b M ...) - if ((*res)[n]->is_X_free()) - continue; const binop* barg = is_bXbRM((*res)[n]); if (barg) @@ -2636,12 +2636,17 @@ namespace spot { \ unsigned y = a2->size(); \ for (unsigned n = 0; n < y; ++n) \ - xgset. \ - insert(a2->nth(n)->clone()); \ + { \ + const formula* sub = a2->nth(n); \ + if (xgset.insert(sub).second) \ + sub->clone(); \ + } \ } \ else \ { \ - xgset.insert(g->child()->clone()); \ + const formula* sub = g->child(); \ + if (xgset.insert(sub).second) \ + sub->clone(); \ } HANDLE_G; } @@ -2657,13 +2662,15 @@ namespace spot } else { - xset.insert(x->clone()); + if (xset.insert(x).second) + x->clone(); } } } else { - xset.insert(c->clone()); + if (xset.insert(c).second) + c->clone(); } (*res)[n]->destroy(); (*res)[n] = 0; @@ -3307,6 +3314,8 @@ namespace spot { if (!(*res)[n]) continue; + if ((*res)[n]->is_X_free()) + continue; const formula* xarg = is_XRM((*res)[n]); if (xarg) @@ -3319,8 +3328,6 @@ namespace spot // - X(...) // - b & X(b W ...) // - b & X(b U ...) - if ((*res)[n]->is_X_free()) - continue; const binop* barg = is_bXbWU((*res)[n]); if (barg) @@ -3329,7 +3336,6 @@ namespace spot continue; } - const unop* uo = is_X((*res)[n]); if (!uo) continue; @@ -3344,12 +3350,17 @@ namespace spot { \ unsigned y = o2->size(); \ for (unsigned n = 0; n < y; ++n) \ - xfset. \ - insert(o2->nth(n)->clone()); \ + { \ + const formula* sub = o2->nth(n); \ + if (xfset.insert(sub).second) \ + sub->clone(); \ + } \ } \ else \ { \ - xfset.insert(f->child()->clone()); \ + const formula* sub = f->child(); \ + if (xfset.insert(sub).second) \ + sub->clone(); \ } HANDLE_F; } @@ -3365,13 +3376,15 @@ namespace spot } else { - xset.insert(x->clone()); + if (xset.insert(x).second) + x->clone(); } } } else { - xset.insert(c->clone()); + if (xset.insert(c).second) + c->clone(); } (*res)[n]->destroy(); (*res)[n] = 0; @@ -3989,7 +4002,12 @@ namespace spot simplify_recursively(const formula* f, ltl_simplifier_cache* c) { +#ifdef TRACE + static int srec = 0; + for (int i = srec; i; --i) + trace << ' '; trace << "** simplify_recursively(" << to_string(f) << ")"; +#endif const formula* result = c->lookup_simplified(f); if (result) @@ -4002,6 +4020,10 @@ namespace spot trace << " miss" << std::endl; } +#ifdef TRACE + ++srec; +#endif + if (f->is_boolean() && c->options.boolean_to_isop) { result = c->boolean_to_isop(f); @@ -4013,8 +4035,13 @@ namespace spot result = v.result(); } +#ifdef TRACE + --srec; + for (int i = srec; i; --i) + trace << ' '; trace << "** simplify_recursively(" << to_string(f) << ") result: " << to_string(result) << std::endl; +#endif c->cache_simplified(f, result); return result;