From 9e7d0677e7190d2761f3ec34ed4d4803f9c1bd37 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 15 Oct 2015 18:26:26 +0200
Subject: [PATCH] parseaut: better diagnostic of unsupported versions

* src/parseaut/parseaut.yy: Add and the a check_version() function.
* src/tests/parseaut.test: Test it.
* NEWS: Mention it.
---
 NEWS                     |  3 +++
 src/parseaut/parseaut.yy | 49 ++++++++++++++++++++++++++++++++++++----
 src/tests/parseaut.test  | 15 ++++++++++--
 3 files changed, 61 insertions(+), 6 deletions(-)

diff --git a/NEWS b/NEWS
index 6072b1f93..be10784b7 100644
--- a/NEWS
+++ b/NEWS
@@ -36,6 +36,9 @@ New in spot 1.99.4a (not yet released)
     the language, but it speedup some algorithms like NDFS-based
     emptiness checks, as discussed in our Spin'15 paper.)
 
+  * The HOA parser will diagnose any version that is not v1, unless it
+    looks like a subversion of v1 and no parse error was detected.
+
   Python:
 
   * Add bindings for complete() and dtwa_complement()
diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy
index f8627301f..408f829e5 100644
--- a/src/parseaut/parseaut.yy
+++ b/src/parseaut/parseaut.yy
@@ -29,6 +29,8 @@
 
 %code requires
 {
+#include "config.h"
+#include "misc/common.hh"
 #include <string>
 #include <cstring>
 #include <sstream>
@@ -39,6 +41,11 @@
 #include "priv/accmap.hh"
 #include "tl/parse.hh"
 
+#ifndef HAVE_STRVERSCMP
+// If the libc does not have this, a version is compiled in lib/.
+extern "C" int strverscmp(const char *s1, const char *s2);
+#endif
+
   inline namespace hoayy_support
   {
     typedef std::map<int, bdd> map_t;
@@ -71,6 +78,8 @@
 	spot::location used_loc;
       };
       spot::parsed_aut_ptr h;
+      std::string format_version;
+      spot::location format_version_loc;
       spot::environment* env;
       formula_cache fcache;
       named_tgba_t* namer = nullptr;
@@ -418,8 +427,8 @@ header: format-version header-items
 
 version: IDENTIFIER
          {
-	   if (*$1 != "v1")
-	     error(@$, "unsupported version of the HOA format");
+	   res.format_version = *$1;
+	   res.format_version_loc = @1;
 	   delete $1;
 	 }
 
@@ -1435,7 +1444,7 @@ nc-formula: nc-formula-or-ident
 nc-opt-dest:
   /* empty */
     {
-      $$ = 0;
+      $$ = nullptr;
     }
   | "->" "goto" IDENTIFIER
     {
@@ -1457,7 +1466,7 @@ nc-src-dest: nc-formula nc-opt-dest
       //   fi
       if (!$2)
 	{
-	  $$ = 0;
+	  $$ = nullptr;
 	}
       else
 	{
@@ -1847,6 +1856,37 @@ static void fix_properties(result_& r)
     r.h->aut->prop_state_based_acc();
 }
 
+static void check_version(const result_& r,
+			  spot::parse_aut_error_list& error_list)
+{
+  if (r.h->type != spot::parsed_aut_type::HOA)
+    return;
+  auto& v = r.format_version;
+  if (v.size() < 2 || v[0] != 'v' || v[1] < '1' || v[1] > '9')
+    {
+      error_list.emplace_front(r.format_version_loc, "unknown HOA version");
+      return;
+    }
+  const char* beg = &v[1];
+  char* end = nullptr;
+  long int vers = strtol(beg, &end, 10);
+  if (vers != 1)
+    {
+      error_list.emplace_front(r.format_version_loc, "unsupported HOA version");
+      return;
+    }
+  constexpr const char supported[] = "1";
+  if (strverscmp(supported, beg) < 0 && !error_list.empty())
+    {
+      std::ostringstream s;
+      s << "we can read HOA v" << supported
+	<< " but this file uses " << v << "; this might "
+	<< "cause the following errors";
+      error_list.emplace_front(r.format_version_loc, s.str());
+      return;
+    }
+}
+
 namespace spot
 {
   automaton_stream_parser::automaton_stream_parser(const std::string& name,
@@ -1906,6 +1946,7 @@ namespace spot
 	// Bison 3.0.2 lacks a += operator for locations.
 	r.h->loc = r.h->loc + e.pos;
       }
+    check_version(r, error_list);
     last_loc = r.h->loc;
     last_loc.step();
     if (r.h->aborted)
diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test
index 09bfad85e..b4a94800c 100755
--- a/src/tests/parseaut.test
+++ b/src/tests/parseaut.test
@@ -250,17 +250,28 @@ State: 1 {0}
 HOA: v2
 --BODY--
 --END--
+HOA: w1
+--BODY--
+--END--
+HOA: v1_1
+--BODY--
+--END--
 EOF
 
+t='this might cause the following errors'
 expecterr input <<EOF
 input:5.19: number is larger than the count of acceptance sets...
 input:5.1-13: ... declared here.
-input:12.6-7: unsupported version of the HOA format
+input:12.6-7: unsupported HOA version
 input:12.1-7: missing 'Acceptance:' header
+input:15.6-7: unknown HOA version
+input:15.1-7: missing 'Acceptance:' header
+input:18.6-9: we can read HOA v1 but this file uses v1_1; $t
+input:18.1-9: missing 'Acceptance:' header
 EOF
 
 cat >input<<EOF
-    HOA: v1
+    HOA: v1a  /* version greater than 1, but assumed to be compatible */
     States: 3
     Start: 0
     acc-name: generalized-Buchi 2