From 64e3fcfb54741f9b2bf2d6edf246dfa18c4c8bb4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 17 Oct 2019 11:22:50 +0200
Subject: [PATCH] formula: avoid id clash for atomic propositions

This corrects a bug that has never been observed yet, has it would
require more than UINT_MAX formulas allocations.

* spot/tl/formula.cc, spot/tl/formula.hh: Bump the formula ID in the
unlikely case a new atomic proposition would receive the same id as a
previous one.
---
 spot/tl/formula.cc | 33 +++++++++++++++++++++++----------
 spot/tl/formula.hh |  9 +++++----
 2 files changed, 28 insertions(+), 14 deletions(-)

diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc
index 9f06443f1..05b295708 100644
--- a/spot/tl/formula.cc
+++ b/spot/tl/formula.cc
@@ -1053,9 +1053,15 @@ namespace spot
     auto ires = m.name2ap.emplace(name, nullptr);
     if (!ires.second)
       return ires.first->second->clone();
-    // Name the formula before creating it, because
-    // the constructor will call ap_name().
-    m.ap2name.emplace(next_id_, name);
+    // Name the formula before creating it, because the constructor
+    // will call ap_name().
+    //
+    // We plan to use next_id_ for identifier, but it is possible that
+    // next_id_ has already wrapped around 0 and that next_id_ is
+    // already the name of another atomic proposition.  In that
+    // unlikely case, simply increment the id.
+    while (SPOT_UNLIKELY(!m.ap2name.emplace(next_id_, name).second))
+      bump_next_id();
     // next_id_ is incremented by setup_props(), called by the
     // constructor of fnode
     return ires.first->second = new fnode(op::ap, {});
@@ -1072,6 +1078,19 @@ namespace spot
   }
 
   size_t fnode::next_id_ = 0U;
+
+  size_t fnode::bump_next_id()
+  {
+    size_t id = next_id_++;
+    // If the counter of formulae ever loops, we want to skip the
+    // first three values, because they are permanently associated
+    // to constants, and it is convenient to have constants
+    // smaller than all other formulas.
+    if (SPOT_UNLIKELY(next_id_ == 0))
+      next_id_ = 3;
+    return id;
+  }
+
   const fnode* fnode::ff_ = new fnode(op::ff, {});
   const fnode* fnode::tt_ = new fnode(op::tt, {});
   const fnode* fnode::ew_ = new fnode(op::eword, {});
@@ -1079,13 +1098,7 @@ namespace spot
 
   void fnode::setup_props(op o)
   {
-    id_ = next_id_++;
-    // If the counter of formulae ever loops, we want to skip the
-    // first three values, because they are permanently associated
-    // to constants, and it is convenient to have constants
-    // smaller than all other formulas.
-    if (SPOT_UNLIKELY(next_id_ == 0))
-      next_id_ = 3;
+    id_ = bump_next_id();
 
     switch (o)
       {
diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh
index 882fa8c69..22f48edd4 100644
--- a/spot/tl/formula.hh
+++ b/spot/tl/formula.hh
@@ -504,6 +504,7 @@ namespace spot
       }
 
     private:
+      static size_t bump_next_id();
       void setup_props(op o);
       void destroy_aux() const;
 
@@ -790,9 +791,9 @@ namespace spot
       if (id() > other.id())
         return false;
       // The case where id()==other.id() but ptr_ != other.ptr_ is
-      // very unlikely (we would need to build more that UINT_MAX
-      // formulas), so let's just compare pointer, and ignore the fact
-      // that it may give some nondeterminism.
+      // very unlikely (we would need to build more than UINT_MAX
+      // formulas), so let's just compare pointers, and ignore the
+      // fact that it may introduce some nondeterminism.
       return ptr_ < other.ptr_;
     }
 
@@ -1402,7 +1403,7 @@ namespace spot
     /// Can be used as a hash number.
     ///
     /// The id is almost unique as it is an unsigned number
-    /// incremented at each formula construction, and the unsigned may
+    /// incremented for each formula construction, and the number may
     /// wrap around zero.  If this is used for ordering, make sure to
     /// deal with equality
     size_t id() const