From ba86dc6b180b1876b6decd5f5fd0c1c2b46e2fe9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 4 Dec 2023 17:59:09 +0100
Subject: [PATCH] twa: guard against highlighting of non-existing edges and
 states
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For issue #556, reported by Dávid Smolka.  Not sure if this is a
complete fix yet, but that's at least part of the issue.

* spot/twa/twagraph.cc (defrag_states): Skip those unexisting edges
and states while remaping highlight-states and highlight-edges.
* spot/parseaut/parseaut.yy: Likewise for dropped edges.
* tests/python/parsetgba.py: Augment test case.
---
 spot/parseaut/parseaut.yy |  5 ++++-
 spot/twa/twagraph.cc      | 12 +++++++++++-
 tests/python/parsetgba.py | 12 +++++++-----
 3 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy
index 865bf6afd..6410d00de 100644
--- a/spot/parseaut/parseaut.yy
+++ b/spot/parseaut/parseaut.yy
@@ -2943,9 +2943,12 @@ namespace spot
       {
         // Update the highlight_edges map to deal with removed/added
         // edges.
+        unsigned ems = r.edge_map.size();
         std::map<unsigned, unsigned> remap;
         for (auto [edgnum, color]: *r.highlight_edges)
-          if (edgnum > 0) /* not expected, but can't trust input data */
+          /* edge numbers outside of the actual number of edges read are
+             not expected, but we can't trust input data */
+          if (SPOT_LIKELY(edgnum > 0 && edgnum <= ems))
             if (unsigned newnum = r.edge_map[edgnum - 1]; newnum > 0)
               remap[newnum] = color;
         std::swap(remap, *r.highlight_edges);
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index b83263931..eb74dd496 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -1274,9 +1274,15 @@ namespace spot
     if (auto hs = get_named_prop<std::map<unsigned, unsigned>>
         ("highlight-states"))
       {
+        unsigned ns = newst.size();
         std::map<unsigned, unsigned> hs2;
         for (auto p: *hs)
           {
+            // Let's just ignore unexisting states.  Raising an
+            // exception here would leave the automaton in a strange
+            // state.
+            if (SPOT_UNLIKELY(p.first >= ns))
+              continue;
             unsigned dst = newst[p.first];
             if (dst != -1U)
               hs2[dst] = p.second;
@@ -1306,7 +1312,11 @@ namespace spot
           }
         std::map<unsigned, unsigned> he2;
         for (auto [e, c]: *he)
-          if (newedges[e] != -1U)
+          // Let's just ignore unexisting edges.  Raising an exception
+          // here would leave the automaton in a strange state.
+          if (SPOT_UNLIKELY(e > es))
+            continue;
+          else if (newedges[e] != -1U)
             he2.emplace(newedges[e], c);
         std::swap(*he, he2);
       }
diff --git a/tests/python/parsetgba.py b/tests/python/parsetgba.py
index feeaad0dd..493d2341f 100755
--- a/tests/python/parsetgba.py
+++ b/tests/python/parsetgba.py
@@ -147,15 +147,17 @@ State: 4 {0}
 [2] 4
 --END--""")
 
-# Issue #555 again.
+# Issue #555 again.   The pairs 30 1 for states and edges are for issue #556
 a4 = spot.automaton("""HOA: v1.1 States: 5 Start: 2 AP: 3 "p36" "p38"
 "p37" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels
 explicit-labels state-acc !complete properties: !deterministic
-exist-branch spot.highlight.edges: 1 1 3 1 8 1 12 1 --BODY-- State: 0
-[t] 1 State: 1 {0} [!0] 1 State: 2 [!0 | !1 | 2] 0 [t] 3 State: 3 [2]
-1 [!2] 4 [2] 1 [!2] 4 State: 4 [!0&2] 1 [!0&!2] 4 [!0&2] 1 [!0&!2] 4
---END--""")
+exist-branch spot.highlight.edges: 1 1 3 1 8 1 12 1 30 1
+spot.highlight.states: 30 1 --BODY-- State: 0 [t] 1 State: 1 {0} [!0]
+1 State: 2 [!0 | !1 | 2] 0 [t] 3 State: 3 [2] 1 [!2] 4 [2] 1 [!2] 4
+State: 4 [!0&2] 1 [!0&!2] 4 [!0&2] 1 [!0&!2] 4 --END--""")
 oi = a4.out_iteraser(2)
+a4.highlight_edge(40, 10);
+a4.highlight_state(40, 10);
 while oi:
     n = a4.edge_number(oi.current())
     if n == 3: