[PATCH] cex: fix a crash

* src/parse-simulation.c: Replace reference counting with parse_state_retain everywhere.
(free_parse_state): Make this function iterative instead of recursive. Long parse_state chains were causing stack exhaustion.

* tests/counterexample.at: fix expectations

It's possible for the search to do a rapid infinite descent through productions, which is one of the reasons there's a timeout. I had never thought of the chance a path would be deep enough to cause stack exhaustion.

I'll be taking a deeper look into the actual results of these tests soon. I'm curious as to what causes the unifying search to fail on the first example from this test.

~Vincent 
---
 src/parse-simulation.c  | 53 ++++++++++++++-------------
 tests/counterexample.at | 79 ++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 106 insertions(+), 26 deletions(-)

diff --git a/src/parse-simulation.c b/src/parse-simulation.c
index 0744b118..c53ea913 100644
--- a/src/parse-simulation.c
+++ b/src/parse-simulation.c
@@ -117,7 +117,7 @@ copy_parse_state (bool prepend, parse_state *parent)
   ret->prepend = prepend;
   ret->reference_count = 0;
   ret->free_contents_early = false;
-  ++parent->reference_count;
+  parse_state_retain (parent);
   ++allocs;
   return ret;
 }
@@ -177,26 +177,29 @@ parse_state_retain_deriv (parse_state *ps)
 }
 
 void
-free_parse_state (parse_state *ps)
+free_parse_state (parse_state *original_ps)
 {
-  if (ps == NULL)
-    return;
-  --ps->reference_count;
-  // need to keep the parse state around
-  // for visited, but its contents can be freed
-  if ((ps->reference_count == 1 && ps->free_contents_early) ||
-      (ps->reference_count == 0 && !ps->free_contents_early))
+  bool free_contents = true;
+  for (parse_state *ps = original_ps; ps && free_contents; ps = ps->parent)
     {
-      if (ps->state_items.contents)
-        gl_list_free (ps->state_items.contents);
-      if (ps->derivs.contents)
-        gl_list_free (ps->derivs.contents);
-      free_parse_state (ps->parent);
-    }
-  if (ps->reference_count <= 0)
-    {
-      free (ps);
-      ++frees;
+      --ps->reference_count;
+      free_contents =
+        (ps->reference_count == 1 && ps->free_contents_early) ||
+        (ps->reference_count == 0 && !ps->free_contents_early);
+      // need to keep the parse state around for visited hash set,
+      // but its contents and parent can be freed
+      if (free_contents)
+        {
+          if (ps->state_items.contents)
+            gl_list_free (ps->state_items.contents);
+          if (ps->derivs.contents)
+            gl_list_free (ps->derivs.contents);
+        }
+      if (ps->reference_count <= 0)
+        {
+          free (ps);
+          ++frees;
+        }
     }
 }
 
@@ -370,7 +373,7 @@ nullable_closure (parse_state *ps, state_item *si, gl_list_t state_list)
       current_ps = copy_parse_state (false, current_ps);
       ps_chunk_append (&current_ps->state_items, nsi);
       ps_chunk_append (&current_ps->derivs, derivation_new (sp, NULL));
-      ++current_ps->reference_count;
+      parse_state_retain (current_ps);
       gl_list_add_last (state_list, current_ps);
     }
 }
@@ -395,7 +398,7 @@ simulate_transition (parse_state *ps)
   parse_state *next_ps = copy_parse_state (false, ps);
   ps_chunk_append (&next_ps->state_items, state_items + si_next);
   ps_chunk_append (&next_ps->derivs, derivation_new (sym, NULL));
-  ++next_ps->reference_count;
+  parse_state_retain (next_ps);
   gl_list_add_last (result, next_ps);
 
   nullable_closure (next_ps, state_items + si_next, result);
@@ -444,7 +447,7 @@ simulate_production (parse_state *ps, symbol_number compat_sym)
             continue;
           parse_state *next_ps = copy_parse_state (false, ps);
           ps_chunk_append (&next_ps->state_items, next);
-          ++next_ps->reference_count;
+          parse_state_retain (next_ps);
           gl_list_add_last (result, next_ps);
           if (next_ps->depth >= 0)
             ++next_ps->depth;
@@ -487,7 +490,7 @@ simulate_reduction (parse_state *ps, int rule_len, bitset symbol_set)
       state_item *tail = (state_item *) new_root->state_items.tail_elt;
       ps_chunk_append (&new_root->state_items,
                        state_items + si_trans[tail - state_items]);
-      ++new_root->reference_count;
+      parse_state_retain (new_root);
       gl_list_add_last (result, new_root);
     }
   else
@@ -509,7 +512,7 @@ simulate_reduction (parse_state *ps, int rule_len, bitset symbol_set)
           ps_chunk *sis = &copy->state_items;
           const state_item *tail = sis->tail_elt;
           ps_chunk_append (sis, state_items + si_trans[tail - state_items]);
-          ++copy->reference_count;
+          parse_state_retain (copy);
           gl_list_add_last (result, copy);
           nullable_closure (copy, (state_item *) sis->tail_elt, result);
         }
@@ -534,7 +537,7 @@ parser_prepend (parse_state *ps)
   BITSET_FOR_EACH (biter, prev, sin, 0)
   {
     parse_state *copy = copy_parse_state (true, ps);
-    copy->reference_count++;
+    parse_state_retain (copy);
     ps_chunk_prepend (&copy->state_items, state_items + sin);
     if (SI_TRANSITION (head))
       ps_chunk_prepend (&copy->derivs, derivation_new (prepend_sym, NULL));
diff --git a/tests/counterexample.at b/tests/counterexample.at
index 9bc16005..73198b0a 100644
--- a/tests/counterexample.at
+++ b/tests/counterexample.at
@@ -419,7 +419,84 @@ d : a | c A | d;
 ]])
 
 AT_BISON_CHECK([-Wcounterexample input.y], [], [],
-[[]])
+[[Reduce-Reduce Conflict:
+0:    3 b: . %empty
+0:    4 c: . %empty
+On Symbols: {A,}
+First  Example •  c  A  A  $end
+First  derivation  $accept ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ]  $end ]
+Second Example •  c  A  A  $end
+Second derivation  $accept ::=[ a ::=[ c ::=[ • ]  d ::=[ c  A  A ] ]  $end ]
+
+Reduce-Reduce Conflict:
+2:    3 b: . %empty
+2:    4 c: . %empty
+On Symbols: {A,}
+time limit exceeded: 6.000000
+First  Example b  •  c  A  A  $end
+First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ]  $end ]
+Second Example b  •  A  $end
+Second derivation  $accept ::=[ a ::=[ b  d ::=[ c ::=[ • ]  A ] ]  $end ]
+
+Reduce-Reduce Conflict:
+3:    3 b: . %empty
+3:    4 c: . %empty
+On Symbols: {A,}
+time limit exceeded: 6.000000
+First  Example c  •  c  A  A  $end
+First  derivation  $accept ::=[ a ::=[ c  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ]  $end ]
+Second Example c  •  A  $end
+Second derivation  $accept ::=[ a ::=[ c  d ::=[ c ::=[ • ]  A ] ]  $end ]
+
+Shift-Reduce Conflict:
+6:    3 b: . %empty
+6:    6 d: c . A
+On Symbol: A
+time limit exceeded: 6.000000
+First  Example b  c  •  c  A  A  $end
+First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ] ] ]  $end ]
+Second Example b  c  •  A
+Second derivation  a ::=[ b  d ::=[ c  •  A ] ]
+
+Reduce-Reduce Conflict:
+6:    3 b: . %empty
+6:    4 c: . %empty
+On Symbols: {A,}
+First  Example b  c  •  c  A  A  $end
+First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ a ::=[ b ::=[ • ]  d ::=[ c  A  A ] ] ] ] ] ]  $end ]
+Second Example b  c  •  A  $end
+Second derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ c ::=[ • ]  A ] ] ] ]  $end ]
+
+Shift-Reduce Conflict:
+6:    4 c: . %empty
+6:    6 d: c . A
+On Symbol: A
+First  Example b  c  •  A  $end
+First  derivation  $accept ::=[ a ::=[ b  d ::=[ a ::=[ c  d ::=[ c ::=[ • ]  A ] ] ] ]  $end ]
+Second Example b  c  •  A
+Second derivation  a ::=[ b  d ::=[ c  •  A ] ]
+
+Reduce-Reduce Conflict:
+7:    1 a: b d .
+7:    7 d: d .
+On Symbols: {$end,}
+Example  b  d  •
+First  derivation  a ::=[ b  d  • ]
+Second derivation  a ::=[ b  d ::=[ d  • ] ]
+
+Reduce-Reduce Conflict:
+8:    2 a: c d .
+8:    7 d: d .
+On Symbols: {$end,}
+Example  c  d  •
+First  derivation  a ::=[ c  d  • ]
+Second derivation  a ::=[ c  d ::=[ d  • ] ]
+
+input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
+input.y: warning: 6 reduce/reduce conflicts [-Wconflicts-rr]
+input.y:5.4: warning: rule useless in parser due to conflicts [-Wother]
+input.y:6.15: warning: rule useless in parser due to conflicts [-Wother]
+]])
 
 AT_CLEANUP
 
-- 
2.20.1 (Apple Git-117)