cex: fix stack overflow

* 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.
This commit is contained in:
Vincent Imbimbo
2020-05-16 14:51:44 -04:00
committed by Akim Demaille
parent 66283fb625
commit 482b370540
2 changed files with 106 additions and 26 deletions

View File

@@ -117,7 +117,7 @@ copy_parse_state (bool prepend, parse_state *parent)
ret->prepend = prepend; ret->prepend = prepend;
ret->reference_count = 0; ret->reference_count = 0;
ret->free_contents_early = false; ret->free_contents_early = false;
++parent->reference_count; parse_state_retain (parent);
++allocs; ++allocs;
return ret; return ret;
} }
@@ -177,26 +177,29 @@ parse_state_retain_deriv (parse_state *ps)
} }
void void
free_parse_state (parse_state *ps) free_parse_state (parse_state *original_ps)
{ {
if (ps == NULL) bool free_contents = true;
return; for (parse_state *ps = original_ps; ps && free_contents; ps = ps->parent)
{
--ps->reference_count; --ps->reference_count;
// need to keep the parse state around free_contents = (ps->reference_count == 1 && ps->free_contents_early)
// for visited, but its contents can be freed || (ps->reference_count == 0 && !ps->free_contents_early);
if ((ps->reference_count == 1 && ps->free_contents_early) || // need to keep the parse state around for visited hash set,
(ps->reference_count == 0 && !ps->free_contents_early)) // but its contents and parent can be freed
if (free_contents)
{ {
if (ps->state_items.contents) if (ps->state_items.contents)
gl_list_free (ps->state_items.contents); gl_list_free (ps->state_items.contents);
if (ps->derivs.contents) if (ps->derivs.contents)
gl_list_free (ps->derivs.contents); gl_list_free (ps->derivs.contents);
free_parse_state (ps->parent);
} }
if (ps->reference_count <= 0) if (ps->reference_count <= 0)
{ {
free (ps); free (ps);
++frees; ++frees;
break;
}
} }
} }
@@ -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); current_ps = copy_parse_state (false, current_ps);
ps_chunk_append (&current_ps->state_items, nsi); ps_chunk_append (&current_ps->state_items, nsi);
ps_chunk_append (&current_ps->derivs, derivation_new (sp, NULL)); 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); 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); 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->state_items, state_items + si_next);
ps_chunk_append (&next_ps->derivs, derivation_new (sym, NULL)); 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); gl_list_add_last (result, next_ps);
nullable_closure (next_ps, state_items + si_next, result); nullable_closure (next_ps, state_items + si_next, result);
@@ -444,7 +447,7 @@ simulate_production (parse_state *ps, symbol_number compat_sym)
continue; continue;
parse_state *next_ps = copy_parse_state (false, ps); parse_state *next_ps = copy_parse_state (false, ps);
ps_chunk_append (&next_ps->state_items, next); ps_chunk_append (&next_ps->state_items, next);
++next_ps->reference_count; parse_state_retain (next_ps);
gl_list_add_last (result, next_ps); gl_list_add_last (result, next_ps);
if (next_ps->depth >= 0) if (next_ps->depth >= 0)
++next_ps->depth; ++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; state_item *tail = (state_item *) new_root->state_items.tail_elt;
ps_chunk_append (&new_root->state_items, ps_chunk_append (&new_root->state_items,
state_items + si_trans[tail - 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); gl_list_add_last (result, new_root);
} }
else else
@@ -509,7 +512,7 @@ simulate_reduction (parse_state *ps, int rule_len, bitset symbol_set)
ps_chunk *sis = &copy->state_items; ps_chunk *sis = &copy->state_items;
const state_item *tail = sis->tail_elt; const state_item *tail = sis->tail_elt;
ps_chunk_append (sis, state_items + si_trans[tail - state_items]); ps_chunk_append (sis, state_items + si_trans[tail - state_items]);
++copy->reference_count; parse_state_retain (copy);
gl_list_add_last (result, copy); gl_list_add_last (result, copy);
nullable_closure (copy, (state_item *) sis->tail_elt, result); 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) BITSET_FOR_EACH (biter, prev, sin, 0)
{ {
parse_state *copy = copy_parse_state (true, ps); parse_state *copy = copy_parse_state (true, ps);
copy->reference_count++; parse_state_retain (copy);
ps_chunk_prepend (&copy->state_items, state_items + sin); ps_chunk_prepend (&copy->state_items, state_items + sin);
if (SI_TRANSITION (head)) if (SI_TRANSITION (head))
ps_chunk_prepend (&copy->derivs, derivation_new (prepend_sym, NULL)); ps_chunk_prepend (&copy->derivs, derivation_new (prepend_sym, NULL));

View File

@@ -419,7 +419,84 @@ d : a | c A | d;
]]) ]])
AT_BISON_CHECK([-Wcounterexample input.y], [], [], 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 AT_CLEANUP