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

formula: catch min/max overflows at construction

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2021-11-18 11:18:06 +01:00
parent 59b361babd
commit afdd38277d
5 changed files with 127 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

8
python/spot/impl.i
View file

@ -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());
}
}
%}

68
spot/tl/formula.cc
View file

@ -21,6 +21,7 @@
#include <spot/misc/common.hh>
#include <spot/tl/formula.hh>
#include <iostream>
#include <sstream>
#include <map>
#include <set>
#include <tuple>
@ -40,6 +41,23 @@ namespace spot
{
typedef std::vector<const fnode*> 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();
}
else if (min != unbounded())
{
min += min2;
if (SPOT_UNLIKELY(min >= unbounded()))
break;
}
if (max2 == unbounded())
{
max = unbounded();
}
else if (max != unbounded())
{
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)
@ -700,6 +738,9 @@ namespace spot
const fnode* exp = child->nth(0);
if (j == unbounded())
{
// cannot simplify if the bound overflows
if ((min * i) < unbounded())
{
min *= i;
max = unbounded();
@ -709,9 +750,15 @@ namespace spot
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

28
spot/tl/formula.hh
View file

@ -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<const fnode*> 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
///

3
tests/core/equals.test
View file

@ -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[*]}

35
tests/python/except.py
View file

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