From 8ffd06e9a6aa4acd59e54c1b921dfe47dbe8d7f8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 2 Dec 2021 09:25:59 +0100
Subject: [PATCH] catch overflow in SVA delays during parsing

* spot/parsetl/scantl.ll: Diagnose delays (##n) larger than
unbounded().  Remove all checks for delays with 1 or 2 characters.
* tests/core/parseerr.test: Add a test case.
* NEWS: Mention this fix.
---
 NEWS                     |  3 +++
 spot/parsetl/scantl.ll   | 22 +++++++++++++++++++---
 tests/core/parseerr.test |  6 ++++++
 3 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 747f78d64..be5760f51 100644
--- a/NEWS
+++ b/NEWS
@@ -8,6 +8,9 @@ New in spot 2.10.1.dev  (not yet released)
   - only use sched_getcpu() and pthread_setaffinity_np() when they are
     available.
 
+  - Using ##300 in a SERE will report that the repeatition exceeds the
+    allowed value using a parse error, not as an exception.
+
 New in spot 2.10.1  (2021-11-19)
 
   Build:
diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll
index a105de21c..ff15685f8 100644
--- a/spot/parsetl/scantl.ll
+++ b/spot/parsetl/scantl.ll
@@ -1,6 +1,6 @@
 /* -*- coding: utf-8 -*-
-** Copyright (C) 2010-2015, 2017-2019, Laboratoire de Recherche et
-** Développement de l'Epita (LRDE).
+** Copyright (C) 2010-2015, 2017-2019, 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 et Marie Curie.
@@ -35,6 +35,7 @@
 
 #include <spot/parsetl/parsedecl.hh>
 #include "spot/priv/trim.hh"
+#include "spot/tl/formula.hh"
 
 #define YY_USER_ACTION \
   yylloc->columns(yyleng);
@@ -221,7 +222,11 @@ eol2        (\n\r)+|(\r\n)+
 "first_match"                   BEGIN(0); return token::OP_FIRST_MATCH;
 
   /* SVA operators */
-"##"[0-9]+                      {
+"##"[0-9]{1,2}                  {
+                                  yylval->num = strtoul(yytext + 2, 0, 10);
+                                  return token::OP_DELAY_N;
+                                }
+"##"[0-9]{3,}                   {
 				  errno = 0;
 				  unsigned long n = strtoul(yytext + 2, 0, 10);
                                   yylval->num = n;
@@ -232,6 +237,17 @@ eol2        (\n\r)+|(\r\n)+
 					  "value too large ignored"));
                                       yylval->num = 1;
                                     }
+                                  if (yylval->num >= spot::fnode::unbounded())
+                                    {
+                                      auto max = spot::fnode::unbounded() - 1;
+                                      std::ostringstream s;
+                                      s << yylval->num
+                                        << (" exceeds maximum supported "
+                                            "repetition (")
+                                        << max << ")";
+                                      error_list.emplace_back(*yylloc, s.str());
+                                      yylval->num = max;
+                                    }
                                   return token::OP_DELAY_N;
                                 }
 "##[+]"                         BEGIN(0); return token::OP_DELAY_PLUS;
diff --git a/tests/core/parseerr.test b/tests/core/parseerr.test
index 479397b44..f9e1b79b7 100755
--- a/tests/core/parseerr.test
+++ b/tests/core/parseerr.test
@@ -35,6 +35,7 @@ cat >input <<EOF
 a - b
 {a[*9999999999]}
 {a ##[1:255] b}
+{a ##255 b}
 EOF
 
 run 1 ../ltl2text input |
@@ -80,6 +81,11 @@ Closure(@6 #0 [Star(@5 #0 0.. ["a"])])
 255 exceeds maximum supported repetition (254)
 
 Closure(@12 #0 [Concat(@11 #0 ["a", Star(@9 #0 0..253 [tt(@1 #0)]), "b"])])
+>>> {a ##255 b}
+       ^^^^^
+255 exceeds maximum supported repetition (254)
+
+Closure(@17 #0 [Concat(@16 #0 ["a", Star(@15 #0 253..253 [tt(@1 #0)]), "b"])])
 EOF
 
 diff output expected