Re: [PATCH] cex: fix crash from zombie result

[Akim Demaille]

Brilliant!

I confirm that it does fix the failure of test 247 on my side!

Please, from now on provide more details in the commit messages.
Describing the changes is not really useful.  What is super important
is to describe the motivation for changes.  In particular, when you
fix a bug, please explain what the bug was, and how your changes
fix it.  Also don't forget to update the expectated test results.

I'm pushing this in the cex branch.  If you have a better commit
message than this one, I'd be happy to fix it.

I would like to merge this branch into master asap.  We have the
problem of the test 253 which crashes too.  Do you think you
will find a fix soon too?

Thanks Vincent!

PS/ I have rebased and pushed -f the cex branch, beware of accidents
with rebase.


commit 7827460bec746beacf04deee2f0432e5c86a918d
Author: Vincent Imbimbo <address@hidden>
Date:   Sat May 16 11:32:29 2020 -0400

    cex: fix crash from zombie result
    
    Fixes the SEGV in test 247 (counterexample.at:195): "S/R after first
    token".
    
    * src/counterexample.c: here.
    * tests/counterexample.at: Fix expectations.

diff --git a/src/counterexample.c b/src/counterexample.c
index bcfc6fa6..dffca1f8 100644
--- a/src/counterexample.c
+++ b/src/counterexample.c
@@ -567,6 +567,13 @@ search_state_free (search_state *ss)
   free (ss);
 }
 
+static inline void
+search_state_retain_derivs (search_state *ss)
+{
+  parse_state_retain_deriv (ss->states[0]);
+  parse_state_retain_deriv (ss->states[1]);
+}
+
 static void
 search_state_print (search_state *ss)
 {
@@ -1070,12 +1077,11 @@ unifying_example (state_item_number itm1,
                       // we've found a unifying counterexample.
                       cex = new_counterexample (d1, d2, true, false);
                       // prevent d1/d2 from being freed.
-                      parse_state_retain_deriv (ps1);
-                      parse_state_retain_deriv (ps2);
+                      search_state_retain_derivs (ss);
                       goto cex_search_end;
                     }
                   if (!stage3result)
-                    stage3result = ss;
+                    stage3result = copy_search_state (ss);
                 }
             }
           if (TIME_LIMIT_ENFORCED)
@@ -1107,7 +1113,11 @@ cex_search_end:;
       // If a search state from Stage 3 is available, use it
       // to construct a more compact nonunifying counterexample.
       if (stage3result)
-        cex = complete_diverging_examples (stage3result, next_sym);
+        {
+          cex = complete_diverging_examples (stage3result, next_sym);
+          search_state_retain_derivs (stage3result);
+          search_state_free (stage3result);
+        }
       // Otherwise, construct a nonunifying counterexample that
       // begins from the start state using the shortest
       // lookahead-sensitive path to the reduce item.
diff --git a/tests/counterexample.at b/tests/counterexample.at
index 9bc16005..03c0a9a6 100644
--- a/tests/counterexample.at
+++ b/tests/counterexample.at
@@ -222,8 +222,8 @@ Shift-Reduce Conflict:
 10:    8 x: X .
 10:    9 xx: X . X
 On Symbol: X
-First  Example X  •  X
-First  derivation  t ::=[ x ::=[ X  • ]  X ]
+First  Example X  •  X  xy
+First  derivation  a ::=[ x ::=[ X  • ]  t ::=[ X  xy ] ]
 Second Example A  X  •  X
 Second derivation  a ::=[ t ::=[ A  xx ::=[ X  •  X ] ] ]