Commit a9fc213a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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).
parent 4b70453d
......@@ -95,6 +95,7 @@ TESTS = \
isop.test \
syntimpl.test \
reduc.test \
reduc0.test \
reducpsl.test \
reduccmp.test \
uwrm.test
......
#! /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 <http://www.gnu.org/licenses/>.
. ./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'
......@@ -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)'
......
......@@ -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;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment