From afdd38277df311b7dfb47ff2d025a084adba8bc8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 18 Nov 2021 11:18:06 +0100 Subject: [PATCH] formula: catch min/max overflows at construction For issue #485. * spot/tl/formula.cc, spot/tl/formula.hh: Catch min/max overflow when the operators are constructed. Also disable travial simplification rules that would create such overflow. For instance x[*200][*2] will not become x[*400] anymore. * python/spot/impl.i: Catch std::overflow_error. * tests/core/equals.test, tests/python/except.py: Add test cases. --- python/spot/impl.i | 8 +++- spot/tl/formula.cc | 88 ++++++++++++++++++++++++++++++++++-------- spot/tl/formula.hh | 28 +++++++------- tests/core/equals.test | 3 +- tests/python/except.py | 35 ++++++++++++++++- 5 files changed, 127 insertions(+), 35 deletions(-) diff --git a/python/spot/impl.i b/python/spot/impl.i index afbda909e..67d29ea09 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -460,14 +460,18 @@ static void handle_any_exception() { SWIG_Error(SWIG_ValueError, e.what()); } - catch (const std::runtime_error& e) + catch (const std::overflow_error& e) { - SWIG_Error(SWIG_RuntimeError, e.what()); + SWIG_Error(SWIG_OverflowError, e.what()); } catch (const std::out_of_range& e) { SWIG_Error(SWIG_IndexError, e.what()); } + catch (const std::runtime_error& e) + { + SWIG_Error(SWIG_RuntimeError, e.what()); + } } %} diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 346d77fce..8fe91bf70 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -21,6 +21,7 @@ #include #include #include +#include #include #include #include @@ -40,6 +41,23 @@ namespace spot { typedef std::vector vec; + [[noreturn]] static void + report_repetition_overflow(unsigned val) + { + std::ostringstream s; + s << val << " exceeds maximum supported repetition (" + << (fnode::unbounded()-1) << ')'; + throw std::overflow_error(s.str()); + } + + [[noreturn]] static void + report_swapped_minmax(unsigned min, unsigned max) + { + std::ostringstream s; + s << "range " << min << ".." << max << " looks reversed (min>max)"; + throw std::overflow_error(s.str()); + } + // Compare two formulas, by looking at their operators and // children. This does not use id for the top-level operator, // because it is used to decide whether to reuse an equal existing @@ -565,13 +583,25 @@ namespace spot min2 = max2 = 1; } if (min2 == unbounded()) - min = unbounded(); + { + min = unbounded(); + } else if (min != unbounded()) - min += min2; + { + min += min2; + if (SPOT_UNLIKELY(min >= unbounded())) + break; + } if (max2 == unbounded()) - max = unbounded(); + { + max = unbounded(); + } else if (max != unbounded()) - max += max2; + { + max += max2; + if (SPOT_UNLIKELY(max >= unbounded())) + break; + } (*i)->destroy(); i = v.erase(i); changed = true; @@ -614,9 +644,17 @@ namespace spot } const fnode* - fnode::bunop(op o, const fnode* child, uint8_t min, uint8_t max) + fnode::bunop(op o, const fnode* child, unsigned min, unsigned max) { - assert(min <= max); + if (SPOT_UNLIKELY(min >= unbounded())) + report_repetition_overflow(min); + // We are testing strict ">", because unbounded() is a legitimate + // input for max. We just cannot tell if it was really intented + // as "unbounded". + if (SPOT_UNLIKELY(max > unbounded())) + report_repetition_overflow(max); + if (SPOT_UNLIKELY(min > max)) + report_swapped_minmax(min, max); const fnode* neutral = nullptr; switch (o) @@ -701,17 +739,26 @@ namespace spot const fnode* exp = child->nth(0); if (j == unbounded()) { - min *= i; - max = unbounded(); + // cannot simplify if the bound overflows + if ((min * i) < unbounded()) + { + min *= i; + max = unbounded(); - // Exp[*min..max] - exp->clone(); - child->destroy(); - child = exp; + // Exp[*min..max] + exp->clone(); + child->destroy(); + child = exp; + } } else { - if (i * (min + 1) <= (j * min) + 1) + if ((i * (min + 1) <= (j * min) + 1) + // cannot simplify if the bound overflows + && (min < unbounded() + && (max == unbounded() + || j == unbounded() + || max * j < unbounded()))) { min *= i; if (max != unbounded()) @@ -1576,7 +1623,7 @@ namespace spot is_.syntactic_si = syntactic_si; if (op_ == op::Fusion) is_.accepting_eword = false; - // A concatenation is an siSERE if looks like + // A concatenation is an siSERE if it looks like // r;b* or b*;r // where b is Boolean and r is siSERE. generalized to n-ary // concatenation, it means all arguments should be of the @@ -1674,9 +1721,16 @@ namespace spot fnode::nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode* f) { - const fnode* res = f; if (max < min) std::swap(min, max); + if (SPOT_UNLIKELY(min >= unbounded())) + report_repetition_overflow(min); + // We are testing strict ">", because unbounded() is a legitimate + // input for max. We just cannot tell if it was really intented + // as "unbounded". + if (SPOT_UNLIKELY(max > unbounded())) + report_repetition_overflow(max); + const fnode* res = f; if (max != unbounded()) for (unsigned i = min; i < max; ++i) { @@ -1772,7 +1826,7 @@ namespace spot return cnt == 0; } - formula formula::sugar_goto(const formula& b, uint8_t min, uint8_t max) + formula formula::sugar_goto(const formula& b, unsigned min, unsigned max) { if (!b.is_boolean()) throw @@ -1781,7 +1835,7 @@ namespace spot return Star(Concat({Star(Not(b)), b}), min, max); } - formula formula::sugar_equal(const formula& b, uint8_t min, uint8_t max) + formula formula::sugar_equal(const formula& b, unsigned min, unsigned max) { if (!b.is_boolean()) throw diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index f355a4d23..a323dcdaf 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -170,7 +170,7 @@ namespace spot static const fnode* multop(op o, std::vector l); /// \see formula::bunop static const fnode* bunop(op o, const fnode* f, - uint8_t min, uint8_t max = unbounded()); + unsigned min, unsigned max = unbounded()); /// \see formula::nested_unop_range static const fnode* nested_unop_range(op uo, op bo, unsigned min, @@ -1188,16 +1188,16 @@ namespace spot /// \pre \a o should be op::Star or op::FStar. /// @{ static formula bunop(op o, const formula& f, - uint8_t min = 0U, - uint8_t max = unbounded()) + unsigned min = 0U, + unsigned max = unbounded()) { return formula(fnode::bunop(o, f.ptr_->clone(), min, max)); } #ifndef SWIG static formula bunop(op o, formula&& f, - uint8_t min = 0U, - uint8_t max = unbounded()) + unsigned min = 0U, + unsigned max = unbounded()) { return formula(fnode::bunop(o, f.to_node_(), min, max)); } @@ -1207,22 +1207,22 @@ namespace spot #if SWIG #define SPOT_DEF_BUNOP(Name) \ static formula Name(const formula& f, \ - uint8_t min = 0U, \ - uint8_t max = unbounded()) \ + unsigned min = 0U, \ + unsigned max = unbounded()) \ { \ return bunop(op::Name, f, min, max); \ } #else // !SWIG #define SPOT_DEF_BUNOP(Name) \ static formula Name(const formula& f, \ - uint8_t min = 0U, \ - uint8_t max = unbounded()) \ + unsigned min = 0U, \ + unsigned max = unbounded()) \ { \ return bunop(op::Name, f, min, max); \ } \ static formula Name(formula&& f, \ - uint8_t min = 0U, \ - uint8_t max = unbounded()) \ + unsigned min = 0U, \ + unsigned max = unbounded()) \ { \ return bunop(op::Name, std::move(f), min, max); \ } @@ -1264,14 +1264,14 @@ namespace spot /// The operator does not exist: it is handled as syntactic sugar /// by the parser and the printer. This function is used by the /// parser to create the equivalent SERE. - static formula sugar_goto(const formula& b, uint8_t min, uint8_t max); + static formula sugar_goto(const formula& b, unsigned min, unsigned max); /// Create the SERE b[=min..max] /// /// The operator does not exist: it is handled as syntactic sugar /// by the parser and the printer. This function is used by the /// parser to create the equivalent SERE. - static formula sugar_equal(const formula& b, uint8_t min, uint8_t max); + static formula sugar_equal(const formula& b, unsigned min, unsigned max); /// Create the SERE a ##[n:m] b /// diff --git a/tests/core/equals.test b/tests/core/equals.test index 4a8834d0a..f00216347 100755 --- a/tests/core/equals.test +++ b/tests/core/equals.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de Recherche et +# Copyright (C) 2009-2012, 2014-2015, 2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -142,6 +142,7 @@ G({1}<>->1), 1 {z;a*;b*;*;c;d;*;b*;e;a*;*;b*}, {z;[*];c;d;[*];e;[*]} {((a;b)|[*0]);[*];c}!, {[*];c}! {a;a;a*;a;b;b[*];c[*2:3];c[*4:5]}, {a[*3..];b[+];c[*6..8]} +{a;a[*200];a[*..60];a;b[*..100][*..2]}, {a[*201];a[*1..61];b[*..200]} {a[*0]}, {[*0]} {a[*..]}, {a[*]} diff --git a/tests/python/except.py b/tests/python/except.py index 0cf6ad1fe..ef6ec3cc5 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -245,3 +245,36 @@ except RuntimeError as e: in str(e) else: report_missing_exception() + + +try: + spot.formula_Star(spot.formula("a"), 10, 333) +except OverflowError as e: + assert "333" in str(e) + assert "254" in str(e) +else: + report_missing_exception() + +try: + spot.formula_FStar(spot.formula("a"), 333, 400) +except OverflowError as e: + assert "333" in str(e) + assert "254" in str(e) +else: + report_missing_exception() + +try: + spot.formula_nested_unop_range(spot.op_F, spot.op_Or, 333, 400, + spot.formula("a")) +except OverflowError as e: + assert "333" in str(e) + assert "254" in str(e) +else: + report_missing_exception() + +try: + spot.formula_FStar(spot.formula("a"), 50, 40) +except OverflowError as e: + assert "reversed" in str(e) +else: + report_missing_exception()