[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PATCH] cex: fix pruning crash
From: |
Vincent Imbimbo |
Subject: |
[PATCH] cex: fix pruning crash |
Date: |
Sat, 23 May 2020 11:20:46 -0400 |
* src/state-item.c (prune_disabled_paths): Prune forward and backwards paths in
seperate passes.
(prune_forward): New.
(prune_backward): New.
(disable_state_item): Change function argument from state_item_number to
state_item.
(state_items_report): Add disabling to graph print-out.
* src/conflicts.c (find_state_item_number, report_state_counterexamples): Add
SI_DISABLED checks.
---
src/conflicts.c | 5 +-
src/state-item.c | 117 ++++++++++++++++++++++++++++++++---------------
2 files changed, 85 insertions(+), 37 deletions(-)
diff --git a/src/conflicts.c b/src/conflicts.c
index 63b07d47..054e5147 100644
--- a/src/conflicts.c
+++ b/src/conflicts.c
@@ -629,7 +629,8 @@ static state_item_number
find_state_item_number (const rule *r, state_number sn)
{
for (int i = state_item_map[sn]; i < state_item_map[sn + 1]; ++i)
- if (item_number_as_rule_number (*state_items[i].item) == r->number)
+ if (!SI_DISABLED (i) &&
+ item_number_as_rule_number (*state_items[i].item) == r->number)
return i;
abort ();
}
@@ -668,6 +669,8 @@ report_state_counterexamples (const state *s)
for (int k = state_item_map[sn];
k < state_item_map[sn + 1]; ++k)
{
+ if (SI_DISABLED (k))
+ continue;
state_item *si = state_items + k;
const rule *r = item_rule (si->item);
if (r == r2)
diff --git a/src/state-item.c b/src/state-item.c
index 90e473a5..a457bb34 100644
--- a/src/state-item.c
+++ b/src/state-item.c
@@ -378,15 +378,85 @@ init_firsts (void)
}
static inline void
-disable_state_item (state_item_number sin)
+disable_state_item (state_item *si)
{
- state_item *si = state_items + sin;
si->trans = -2;
bitset_free (si->revs);
if (si->prods)
bitset_free (si->prods);
}
+/* disable all transitions and productions that can only be
+ * reached through this state_item.
+ */
+static void
+prune_forward (const state_item *si)
+{
+ gl_list_t queue =
+ gl_list_create (GL_LINKED_LIST, NULL, NULL, NULL, true, 1,
+ (const void **) &si);
+
+ while (gl_list_size (queue) > 0)
+ {
+ state_item *dsi = (state_item *) gl_list_get_at (queue, 0);
+ gl_list_remove_at (queue, 0);
+ if (dsi->trans >= 0)
+ gl_list_add_last (queue, state_items + dsi->trans);
+
+ if (dsi->prods)
+ {
+ bitset_iterator biter;
+ state_item_number sin;
+ BITSET_FOR_EACH (biter, dsi->prods, sin, 0)
+ {
+ const state_item *prod = state_items + sin;
+ bitset_reset (prod->revs, dsi - state_items);
+ if (bitset_empty_p (prod->revs))
+ gl_list_add_last (queue, prod);
+ }
+ }
+ if (dsi != si)
+ disable_state_item (dsi);
+ }
+ gl_list_free (queue);
+}
+
+/* disable all state_item paths that lead to
+ * si and nowhere else.
+ */
+static void
+prune_backward (const state_item *si)
+{
+ gl_list_t queue =
+ gl_list_create (GL_LINKED_LIST, NULL, NULL, NULL, true, 1,
+ (const void **) &si);
+
+ while (gl_list_size (queue) > 0)
+ {
+ state_item *dsi = (state_item *) gl_list_get_at (queue, 0);
+ gl_list_remove_at (queue, 0);
+ bitset_iterator biter;
+ state_item_number sin;
+ BITSET_FOR_EACH (biter, dsi->revs, sin, 0)
+ {
+ if (SI_DISABLED (sin))
+ continue;
+ state_item *rev = state_items + sin;
+ if (rev->prods)
+ {
+ bitset_reset (rev->prods, dsi - state_items);
+ if (bitset_empty_p (rev->prods))
+ gl_list_add_last (queue, rev);
+ }
+ else
+ gl_list_add_last (queue, rev);
+ }
+ if (dsi != si)
+ disable_state_item (dsi);
+ }
+ gl_list_free (queue);
+}
+
/*
To make searches more efficient, we can prune away paths that are
caused by disabled transitions.
@@ -399,40 +469,9 @@ prune_disabled_paths (void)
state_item *si = state_items + i;
if (si->trans == -1 && item_number_is_symbol_number (*si->item))
{
- // disable the transitions out of i
- for (state_item_number j = si->trans; j != -1; j =
state_items[j].trans)
- disable_state_item (j);
-
- gl_list_t queue =
- gl_list_create (GL_LINKED_LIST, NULL, NULL, NULL, true, 1,
- (const void **) &si);
-
- // For each disabled transition, traverse through all state_items
- // accessible through reverse transition steps, and set their
- // lookaheads to the reduction items lookahead
- while (gl_list_size (queue) > 0)
- {
- const state_item *prev = gl_list_get_at (queue, 0);
- gl_list_remove_at (queue, 0);
- state_item_number prev_num = prev - state_items;
-
- bitset rsi = prev->revs;
- bitset_iterator biter;
- state_item_number sin;
- BITSET_FOR_EACH (biter, rsi, sin, 0)
- {
- if (SI_TRANSITION (prev))
- gl_list_add_first (queue, &state_items[sin]);
- else
- {
- bitset p = state_items[sin].prods;
- if (p)
- bitset_reset (p, prev_num);
- }
- }
- disable_state_item (prev_num);
- }
- gl_list_free (queue);
+ prune_forward (si);
+ prune_backward (si);
+ disable_state_item (si);
}
}
}
@@ -459,6 +498,12 @@ state_items_report (void)
{
state_item *si = state_items + j;
item_print (si->item, NULL, stdout);
+ if (SI_DISABLED (j))
+ {
+ item_print (si->item, NULL, stdout);
+ puts (" DISABLED");
+ continue;
+ }
puts ("");
if (si->trans >= 0)
{
--
2.20.1 (Apple Git-117)
- [PATCH] cex: fix pruning crash,
Vincent Imbimbo <=