[PATCH 3/5] Counterexample search
Vincent Imbimbo <[email protected]>
| Newsgroups | gmane.comp.parsers.bison.patches |
|---|---|
| Message-ID | <[email protected]> |
---
src/counterexample.c | 1194 ++++++++++++++++++++++++++++++++++++++++++
src/counterexample.h | 35 ++
2 files changed, 1229 insertions(+)
create mode 100644 src/counterexample.c
create mode 100644 src/counterexample.h
diff --git a/src/counterexample.c b/src/counterexample.c
new file mode 100644
index 00000000..aa4b96e5
--- /dev/null
+++ b/src/counterexample.c
@@ -0,0 +1,1194 @@
+/* Conflict counterexample generation
+
+ Copyright (C) 2019-2020 Free Software Foundation, Inc.
+
+ This file is part of Bison, the GNU Compiler Compiler.
+
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>. */
+
+#include <config.h>
+#include <time.h>
+#include <hash.h>
+#include <stdlib.h>
+#include <gl_linked_list.h>
+#include <gl_xlist.h>
+#include <gl_rbtreehash_list.h>
+#include "counterexample.h"
+#include "derivation.h"
+#include "gram.h"
+#include "complain.h"
+#include "closure.h"
+#include "nullable.h"
+#include "getargs.h"
+#include "lalr.h"
+#include "parse-simulation.h"
+#include "lssi.h"
+
+
+#define TIME_LIMIT_ENFORCED true
+/** If set to false, only consider the states on the shortest
+ * lookahead-sensitive path when constructing a unifying counterexample. */
+#define EXTENDED_SEARCH false
+
+/* costs for making various steps in a search */
+#define PRODUCTION_COST 50
+#define REDUCE_COST 1
+#define SHIFT_COST 1
+#define UNSHIFT_COST 1
+#define EXTENDED_COST 10000
+
+/** The time limit before printing an assurance message to the user to
+ * indicate that the search is still running. */
+#define ASSURANCE_LIMIT 2.0f
+
+/* The time limit before giving up looking for unifying counterexample. */
+#define TIME_LIMIT 5.0f
+
+#define CUMULATIVE_TIME_LIMIT 120.0f
+
+typedef struct
+{
+ const derivation *d1;
+ const derivation *d2;
+ bool unifying;
+ bool timeout;
+} counterexample;
+
+counterexample *
+new_counterexample (const derivation *d1, const derivation *d2,
+ bool u, bool t)
+{
+ counterexample *ret = xmalloc (sizeof (counterexample));
+ ret->d1 = d1;
+ ret->d2 = d2;
+ ret->unifying = u;
+ ret->timeout = t;
+ return ret;
+}
+
+void
+print_counterexample (counterexample *cex)
+{
+ if (cex->unifying)
+ printf ("Example ");
+ else
+ printf ("First Example");
+ derivation_print_leaves (cex->d1, stdout);
+ printf ("\nFirst derivation ");
+ derivation_print (cex->d1, stdout);
+ if (!cex->unifying)
+ {
+ printf ("\nSecond Example ");
+ derivation_print_leaves (cex->d2, stdout);
+ }
+ printf ("\nSecond derivation ");
+ derivation_print (cex->d2, stdout);
+ fputs ("\n\n", stdout);
+}
+
+/*
+ *
+ * NON UNIFYING COUNTER EXAMPLES
+ *
+ */
+
+// Search node for BFS on state items
+struct si_bfs_node;
+typedef struct si_bfs_node
+{
+ state_item_number si;
+ struct si_bfs_node *parent;
+ int reference_count;
+} si_bfs_node;
+
+si_bfs_node *
+si_bfs_new (state_item_number si, si_bfs_node *parent)
+{
+ si_bfs_node *ret = xcalloc (1, sizeof (si_bfs_node));
+ ret->si = si;
+ ret->parent = parent;
+ ret->reference_count = 1;
+ if (parent)
+ ++parent->reference_count;
+ return ret;
+}
+
+static bool
+si_bfs_contains (const si_bfs_node *n, state_item_number sin)
+{
+ for (const si_bfs_node *search = n; search != NULL; search = search->parent)
+ if (search->si == sin)
+ return true;
+ return false;
+}
+
+void
+si_bfs_free (si_bfs_node *n)
+{
+ if (n == NULL)
+ return;
+ if (n->reference_count == 0)
+ {
+ if (n->parent)
+ {
+ --n->parent->reference_count;
+ si_bfs_free (n->parent);
+ }
+ free (n);
+ }
+}
+
+/**
+ * start is a state_item such that conflict_sym is an element of FIRSTS of the
+ * non-terminal after the dot in start. Because of this, we should be able to
+ * find a production item starting with conflict_sym by only searching productions
+ * of the non-terminal and shifting over nullable non-terminals
+ *
+ * this returns the derivation of the productions that lead to conflict_sym
+ */
+static inline gl_list_t
+expand_to_conflict (state_item_number start, symbol_number conflict_sym)
+{
+ si_bfs_node *init = si_bfs_new (start, NULL);
+
+ gl_list_t queue = gl_list_create (GL_LINKED_LIST, NULL, NULL,
+ (gl_listelement_dispose_fn) si_bfs_free,
+ true, 1, (const void **) &init);
+ si_bfs_node *node;
+ // breadth-first search for a path of productions to the conflict symbol
+ while (gl_list_size (queue) > 0)
+ {
+ node = (si_bfs_node *) gl_list_get_at (queue, 0);
+ state_item *silast = state_items + node->si;
+ symbol_number sym = item_number_as_symbol_number (*(silast->item));
+ if (sym == conflict_sym)
+ break;
+ if (ISVAR (sym))
+ {
+ // add each production to the search
+ bitset_iterator biter;
+ state_item_number sin;
+ bitset sib = si_prods_lookup (node->si);
+ BITSET_FOR_EACH (biter, sib, sin, 0)
+ {
+ // ignore productions already in the path
+ if (si_bfs_contains (node, sin))
+ continue;
+ si_bfs_node *next = si_bfs_new (sin, node);
+ gl_list_add_last (queue, next);
+ }
+ // for nullable nonterminals, add its goto to the search
+ if (nullable[sym - ntokens])
+ {
+ si_bfs_node *next = si_bfs_new (si_trans[node->si], node);
+ gl_list_add_last (queue, next);
+ }
+ }
+ gl_list_remove_at (queue, 0);
+ }
+ if (gl_list_size (queue) == 0)
+ {
+ gl_list_free (queue);
+ fputs ("Error expanding derivation\n", stderr);
+ exit (1);
+ }
+
+ derivation *dinit = derivation_new (conflict_sym, NULL);
+ gl_list_t result =
+ gl_list_create (GL_LINKED_LIST, NULL, NULL,
+ (gl_listelement_dispose_fn) derivation_free,
+ true, 1, (const void **) &dinit);
+ // iterate backwards through the generated path to create a derivation
+ // of the conflict symbol containing derivations of each production step.
+
+ for (si_bfs_node *n = node; n != NULL; n = n->parent)
+ {
+ state_item *si = state_items + n->si;
+ item_number *pos = si->item;
+ if (SI_PRODUCTION (si))
+ {
+ item_number *i;
+ for (i = pos + 1; !item_number_is_rule_number (*i); ++i)
+ gl_list_add_last (result, derivation_new (*i, NULL));
+ symbol_number lhs =
+ rules[item_number_as_rule_number (*i)].lhs->number;
+ derivation *deriv = derivation_new (lhs, result);
+ result =
+ gl_list_create (GL_LINKED_LIST, NULL, NULL,
+ (gl_listelement_dispose_fn) derivation_free,
+ true, 1, (const void **) &deriv);
+ }
+ else
+ {
+ symbol_number sym = item_number_as_symbol_number (*(pos - 1));
+ derivation *deriv = derivation_new (sym, NULL);
+ gl_list_add_first (result, deriv);
+ }
+ }
+ gl_list_free (queue);
+ gl_list_remove_at (result, 0);
+ return result;
+}
+
+/**
+ * Complete derivations for any pending productions in the given
+ * sequence of state-items. For example, the input could be a path
+ * of states that would give us the following input:
+ * Stmt ::= [lval ::= [VAR] '=' e ::=[ e::=['0'] '+' •
+ * So to complete the derivation of Stmt, we need an output like:
+ * Stmt ::= [lval ::= [VAR] '=' e ::=[ e::=['0'] '+' • e ] ';' ]
+ */
+static derivation *
+complete_diverging_example (symbol_number conflict_sym,
+ gl_list_t states, gl_list_t derivs)
+{
+ // The idea is to transfer each pending symbol on the productions
+ // associated with the given StateItems to the resulting derivation.
+ gl_list_t result =
+ gl_list_create_empty (GL_LINKED_LIST, NULL, NULL, NULL, true);
+ bool lookahead_required = false;
+ if (!derivs)
+ {
+ derivs = gl_list_create_empty (GL_LINKED_LIST, NULL, NULL, NULL, true);
+ gl_list_add_last (result, derivation_dot ());
+ lookahead_required = true;
+ }
+ // This is the fastest way to get the tail node from the gl_list API
+ gl_list_node_t tmpd = gl_list_add_last (derivs, NULL);
+ gl_list_node_t tmps = gl_list_add_last (states, NULL);
+ gl_list_node_t deriv = gl_list_previous_node (derivs, tmpd);
+ gl_list_node_t state = gl_list_previous_node (states, tmps);
+ gl_list_remove_node (derivs, tmpd);
+ gl_list_remove_node (states, tmps);
+ // we go backwards through the path to create the derivation tree bottom-up.
+ // Effectively this loops through each production once, and generates a
+ // derivation of the left hand side by appending all of the rhs symbols.
+ // this becomes the derivation of the non-terminal after the dot in the
+ // next production, and all of the other symbols of the rule are added as normal.
+ for (; state != NULL; state = gl_list_previous_node (states, state))
+ {
+ state_item *si = (state_item *) gl_list_node_value (states, state);
+ item_number *item = si->item;
+ item_number pos = *item;
+ // symbols after dot
+ if (gl_list_size (result) == 1 && !item_number_is_rule_number (pos)
+ && gl_list_get_at (result, 0) == derivation_dot() )
+ {
+ gl_list_add_last (result,
+ derivation_new (item_number_as_symbol_number
+ (pos), NULL));
+ lookahead_required = false;
+ }
+ item_number *i = item;
+ // go through each symbol after the dot in the current rule, and
+ // add each symbol to its derivation.
+ for (state_item_number nsi = si - state_items;
+ !item_number_is_rule_number (*i); ++i, nsi = si_trans[nsi])
+ {
+ // if the item is a reduction, we could skip to the wrong rule
+ // by starting at i + 1, so this continue is necessary
+ if (i == item)
+ continue;
+ symbol_number sym = item_number_as_symbol_number (*i);
+ if (!lookahead_required || sym == conflict_sym)
+ {
+ gl_list_add_last (result, derivation_new (sym, NULL));
+ lookahead_required = false;
+ continue;
+ }
+ // Since states is a path to the conflict state-item,
+ // for a reduce conflict item, we will want to have a derivation
+ // that shows the conflict symbol from its lookahead set being used.
+ //
+ // Since reductions have the dot at the end of the item,
+ // this loop will be first executed on the last item in the path
+ // that's not a reduction. When that happens,
+ // the symbol after the dot should be a non-terminal,
+ // and we can look through successive nullable non-terminals
+ // for one with the conflict symbol in its first set.
+ if (bitset_test (FIRSTS (sym), conflict_sym))
+ {
+ lookahead_required = false;
+ gl_list_t next_derivs = expand_to_conflict (nsi,
+ conflict_sym);
+ gl_list_iterator_t it = gl_list_iterator (next_derivs);
+ derivation *d;
+ while (gl_list_iterator_next (&it, (const void **) &d, NULL))
+ gl_list_add_last (result, d);
+ i += gl_list_size (next_derivs) - 1;
+ // next_derivs is leaked to prevent the copied derivations from
+ // being freed. It is somewhat difficult to for expand_to_conflict
+ // to decide which derivation list will be the final one that is
+ // returned, so each list frees its derivations when freed.
+ }
+ else if (nullable[sym - ntokens])
+ {
+ derivation *d = derivation_new (sym,
+ gl_list_create_empty
+ (GL_LINKED_LIST, NULL,
+ NULL, NULL, 1));
+ gl_list_add_last (result, d);
+ }
+ else
+ {
+ // We found a path to the conflict item, and despite it
+ // having the conflict symbol in its lookahead, no example
+ // containing the symbol after the conflict item
+ // can be found.
+ gl_list_add_last (result, derivation_new (1, NULL));
+ lookahead_required = false;
+ }
+ }
+ rule_number r = item_number_as_rule_number (*i);
+ // add derivations for symbols before dot
+ for (i = item - 1; !item_number_is_rule_number (*i) && i >= ritem; i--)
+ {
+ gl_list_node_t p = gl_list_previous_node (states, state);
+ if (p)
+ state = p;
+ if (deriv)
+ {
+ const void *tmp_deriv = gl_list_node_value (derivs, deriv);
+ deriv = gl_list_previous_node (derivs, deriv);
+ gl_list_add_first (result, tmp_deriv);
+ }
+ else
+ gl_list_add_first (result, derivation_new (*i, NULL));
+ }
+ // completing the derivation
+ derivation *new_deriv = derivation_new (rules[r].lhs->number, result);
+ result =
+ gl_list_create (GL_LINKED_LIST, NULL, NULL, NULL, true, 1,
+ (const void **) &new_deriv);
+ }
+ derivation *ret = (derivation *) gl_list_get_at (result, 0);
+ gl_list_free (result);
+ return ret;
+}
+
+/* iterates backwards through the shifts of the path in the
+ reduce conflict, and finds a path of shifts from the shift
+ conflict that goes through the same states.
+ */
+gl_list_t
+nonunifying_shift_path (gl_list_t reduce_path, state_item *shift_conflict)
+{
+ gl_list_node_t tmp = gl_list_add_last (reduce_path, NULL);
+ gl_list_node_t next_node = gl_list_previous_node (reduce_path, tmp);
+ gl_list_node_t node = gl_list_previous_node (reduce_path, next_node);
+ gl_list_remove_node (reduce_path, tmp);
+ state_item *si = shift_conflict;
+ gl_list_t result =
+ gl_list_create_empty (GL_LINKED_LIST, NULL, NULL, NULL, true);
+ bool paths_merged;
+ for (; node != NULL; next_node = node,
+ node = gl_list_previous_node (reduce_path, node))
+ {
+ state_item *refsi =
+ (state_item *) gl_list_node_value (reduce_path, node);
+ state_item *nextrefsi =
+ (state_item *) gl_list_node_value (reduce_path, next_node);
+ if (nextrefsi == si)
+ {
+ gl_list_add_first (result, refsi);
+ si = refsi;
+ continue;
+ }
+ // skip reduction items
+ if (nextrefsi->item != refsi->item + 1 && refsi->item != ritem)
+ continue;
+
+ // bfs to find a shift to the right state
+ si_bfs_node *init = si_bfs_new (si - state_items, NULL);
+ gl_list_t queue =
+ gl_list_create (GL_LINKED_LIST, NULL, NULL,
+ (gl_listelement_dispose_fn) si_bfs_free,
+ true, 1, (const void **) &init);
+ si_bfs_node *sis = NULL;
+ state_item *prevsi = NULL;
+ while (gl_list_size (queue) > 0)
+ {
+ sis = (si_bfs_node *) gl_list_get_at (queue, 0);
+ // if we end up in the start state, the shift couldn't be found.
+ if (sis->si == 0)
+ break;
+
+ state_item *search_si = state_items + sis->si;
+ // if the current state-item is a production item,
+ // its reverse production items get added to the queue.
+ // Otherwise, look for a reverse transition to the target state.
+ bitset rsi = si_revs[sis->si];
+ bitset_iterator biter;
+ state_item_number sin;
+ BITSET_FOR_EACH (biter, rsi, sin, 0)
+ {
+ prevsi = state_items + sin;
+ if (SI_TRANSITION (search_si))
+ {
+ if (prevsi->state == refsi->state)
+ goto search_end;
+ }
+ else if (!si_bfs_contains (sis, sin))
+ {
+ si_bfs_node *prevsis = si_bfs_new (sin, sis);
+ gl_list_add_last (queue, prevsis);
+ }
+ }
+ gl_list_remove_at (queue, 0);
+ }
+ search_end:
+ // prepend path to shift we found
+ if (sis)
+ {
+ gl_list_node_t ln = gl_list_add_first (result, state_items + sis->si);
+ for (si_bfs_node *n = sis->parent; n; n = n->parent)
+ ln = gl_list_add_after (result, ln, state_items + n->si);
+
+ }
+ si = prevsi;
+ gl_list_free (queue);
+ }
+ if (trace_flag & trace_cex)
+ {
+ puts ("SHIFT ITEM PATH:");
+ gl_list_iterator_t it = gl_list_iterator (result);
+ state_item *sip;
+ while (gl_list_iterator_next (&it, (const void **) &sip, NULL))
+ print_state_item (sip, stdout);
+ }
+ return result;
+}
+
+
+/**
+ * Construct a nonunifying counterexample from the shortest
+ * lookahead-sensitive path.
+ */
+counterexample *
+example_from_path (bool shift_reduce,
+ state_item_number itm2,
+ gl_list_t shortest_path, symbol_number next_sym)
+{
+ derivation *deriv1 =
+ complete_diverging_example (next_sym, shortest_path, NULL);
+ gl_list_t path_2 = shift_reduce ? nonunifying_shift_path (shortest_path,
+ &state_items
+ [itm2]) :
+ shortest_path_from_start (itm2, next_sym);
+ derivation *deriv2 = complete_diverging_example (next_sym, path_2, NULL);
+ gl_list_free (path_2);
+ return new_counterexample (deriv1, deriv2, false, true);
+}
+
+/*
+ *
+ * UNIFYING COUNTER EXAMPLES
+ *
+ */
+
+/* A search state keeps track of two parser simulations,
+ * one starting at each conflict. Complexity is a metric
+ * which sums different parser actions with varying weights.
+ */
+typedef struct
+{
+ parse_state *states[2];
+ int complexity;
+} search_state;
+
+static search_state *
+initial_search_state (state_item *conflict1, state_item *conflict2)
+{
+ search_state *ret = xmalloc (sizeof (search_state));
+ ret->states[0] = new_parse_state (conflict1);
+ ret->states[1] = new_parse_state (conflict2);
+ parse_state_retain (ret->states[0]);
+ parse_state_retain (ret->states[1]);
+ ret->complexity = 0;
+ return ret;
+}
+
+static search_state *
+new_search_state (parse_state *ps1, parse_state *ps2, int complexity)
+{
+ search_state *ret = xmalloc (sizeof (search_state));
+ ret->states[0] = ps1;
+ ret->states[1] = ps2;
+ parse_state_retain (ret->states[0]);
+ parse_state_retain (ret->states[1]);
+ ret->complexity = complexity;
+ return ret;
+}
+
+static search_state *
+copy_search_state (search_state *parent)
+{
+ search_state *copy = xmalloc (sizeof (search_state));
+ memcpy (copy, parent, sizeof (search_state));
+ parse_state_retain (copy->states[0]);
+ parse_state_retain (copy->states[1]);
+ return copy;
+}
+
+static void
+search_state_free_children (search_state *ss)
+{
+ free_parse_state (ss->states[0]);
+ free_parse_state (ss->states[1]);
+}
+
+static void
+search_state_free (search_state *ss)
+{
+ if (ss == NULL)
+ return;
+ search_state_free_children (ss);
+ free (ss);
+}
+
+static void
+search_state_print (search_state *ss)
+{
+ fputs ("CONFLICT 1 ", stdout);
+ print_parse_state (ss->states[0]);
+ fputs ("CONFLICT 2 ", stdout);
+ print_parse_state (ss->states[1]);
+ putc ('\n', stdout);
+}
+
+/*
+ * When a search state is copied, this is used to
+ * directly set one of the parse states
+ */
+static inline void
+ss_set_parse_state (search_state *ss, int index, parse_state *ps)
+{
+ free_parse_state (ss->states[index]);
+ ss->states[index] = ps;
+ parse_state_retain (ps);
+}
+
+/*
+ * Construct a nonunifying example from a search state
+ * which has its parse states unified at the beginning
+ * but not the end of the example.
+ */
+counterexample *
+complete_diverging_examples(search_state *ss,
+ symbol_number next_sym)
+{
+ derivation *new_derivs[2];
+ for (int i = 0; i < 2; ++i)
+ {
+ gl_list_t state_items, derivs;
+ parse_state_lists (ss->states[i], &state_items, &derivs);
+ new_derivs[i] =
+ complete_diverging_example (next_sym, state_items, derivs);
+ }
+ return new_counterexample (new_derivs[0], new_derivs[1], false, true);
+}
+
+/*
+ * Search states are stored in bundles with those that
+ * share the same complexity. This is so the priority
+ * queue takes less overhead.
+ */
+typedef struct
+{
+ gl_list_t states;
+ int complexity;
+} search_state_bundle;
+void
+ssb_free (search_state_bundle *ssb)
+{
+ gl_list_free (ssb->states);
+ free(ssb);
+}
+
+static size_t
+ssb_hasher (search_state_bundle *ssb)
+{
+ return ssb->complexity;
+}
+
+static int
+ssb_comp (const search_state_bundle *s1, const search_state_bundle *s2)
+{
+ return s1->complexity - s2->complexity;
+}
+
+static bool
+ssb_equals (const search_state_bundle *s1, const search_state_bundle *s2)
+{
+ return s1->complexity == s2->complexity;
+}
+
+static size_t
+visited_hasher (const search_state *ss, size_t max)
+{
+ return (parse_state_hasher (ss->states[0], max)
+ + parse_state_hasher (ss->states[1], max)) % max;
+}
+
+static bool
+visited_comparator (const search_state *ss1, const search_state *ss2)
+{
+ return parse_state_comparator (ss1->states[0], ss2->states[0])
+ && parse_state_comparator (ss1->states[1], ss2->states[1]);
+}
+
+/* Priority queue for search states with minimal complexity. */
+static gl_list_t ssb_queue;
+static Hash_table *visited;
+/* The set of parser states on the shortest lookahead-sensitive path. */
+static bitset scp_set = NULL;
+/* The set of parser states used for the conflict reduction rule. */
+static bitset rpp_set = NULL;
+
+static void
+ssb_append (search_state *ss)
+{
+ if (hash_lookup (visited, ss))
+ {
+ search_state_free (ss);
+ return;
+ }
+ if (!hash_insert (visited, ss))
+ xalloc_die ();
+ // if states are only referenced by the visited set,
+ // their contents should be freed as we only need
+ // the metadata necessary to compute a hash.
+ parse_state_free_contents_early (ss->states[0]);
+ parse_state_free_contents_early (ss->states[1]);
+ parse_state_retain (ss->states[0]);
+ parse_state_retain (ss->states[1]);
+ search_state_bundle *ssb = xmalloc (sizeof (search_state_bundle));
+ ssb->complexity = ss->complexity;
+ gl_list_node_t n = gl_list_search (ssb_queue, ssb);
+ if (!n)
+ {
+ ssb->states =
+ gl_list_create_empty (GL_LINKED_LIST, NULL, NULL,
+ (gl_listelement_dispose_fn)search_state_free_children,
+ true);
+ gl_sortedlist_add (ssb_queue, (gl_listelement_compar_fn) ssb_comp, ssb);
+ }
+ else
+ {
+ free (ssb);
+ ssb = (search_state_bundle *) gl_list_node_value (ssb_queue, n);
+ }
+ gl_list_add_last (ssb->states, ss);
+}
+
+/*
+ * The following functions perform various actions on parse states
+ * and assign complexities to the newly generated search states.
+ */
+static void
+production_step (search_state *ss, int parser_state)
+{
+ const state_item *other_si = parse_state_tail (ss->states[1 - parser_state]);
+ symbol_number other_sym = item_number_as_symbol_number (*other_si->item);
+ gl_list_t prods = simulate_production (ss->states[parser_state], other_sym);
+ int complexity = ss->complexity + PRODUCTION_COST;
+
+ gl_list_iterator_t it = gl_list_iterator (prods);
+ parse_state *ps;
+ while (gl_list_iterator_next (&it, (const void **) &ps, NULL))
+ {
+ search_state *copy = copy_search_state (ss);
+ ss_set_parse_state (copy, parser_state, ps);
+ copy->complexity = complexity;
+ ssb_append (copy);
+ }
+}
+
+static inline int
+reduction_cost (const parse_state *ps)
+{
+ int shifts;
+ int productions;
+ parse_state_completed_steps (ps, &shifts, &productions);
+ return SHIFT_COST * shifts + PRODUCTION_COST * productions;
+}
+
+static gl_list_t
+reduction_step (search_state *ss, const item_number *conflict_item,
+ int parser_state, int rule_len)
+{
+ gl_list_t result =
+ gl_list_create_empty (GL_LINKED_LIST, NULL, NULL, NULL, 1);
+
+ parse_state *ps = ss->states[parser_state];
+ const state_item *si = parse_state_tail (ps);
+ bitset symbol_set = si->lookahead;
+ parse_state *other = ss->states[1 - parser_state];
+ const state_item *other_si = parse_state_tail (other);
+ // if the other state can transition on a symbol,
+ // the reduction needs to have that symbol in its lookahead
+ if (item_number_is_symbol_number (*other_si->item))
+ {
+ symbol_number other_sym =
+ item_number_as_symbol_number (*other_si->item);
+ if (!intersect_symbol (other_sym, symbol_set))
+ return result;
+ symbol_set = bitset_create (nsyms, BITSET_FIXED);
+ bitset_set (symbol_set, other_sym);
+ }
+
+ search_state *new_root = copy_search_state (ss);
+ gl_list_t reduced = simulate_reduction (ps, rule_len, symbol_set);
+ gl_list_iterator_t it = gl_list_iterator (reduced);
+ parse_state *reduced_ps;
+ while (gl_list_iterator_next (&it, (const void **) &reduced_ps, NULL))
+ {
+ search_state *copy = copy_search_state (ss);
+ ss_set_parse_state (copy, parser_state, reduced_ps);
+ int r_cost = reduction_cost (reduced_ps);
+ copy->complexity += r_cost + PRODUCTION_COST + 2 * SHIFT_COST;
+ gl_list_add_last (result, copy);
+ }
+ return result;
+}
+
+/**
+ * Attempt to prepend the given symbol to this search state, respecting
+ * the given subsequent next symbol on each path. If a reverse transition
+ * cannot be made on both states, possible reverse productions are prepended
+ */
+void
+search_state_prepend (search_state *ss, symbol_number sym, bitset guide)
+{
+ const state_item *si1src = parse_state_head (ss->states[0]);
+ const state_item *si2src = parse_state_head (ss->states[1]);
+
+ bool prod1 = SI_PRODUCTION (si1src);
+ // If one can make a reverse transition and the other can't, only apply
+ // the reverse productions that the other state can make in an attempt to
+ // make progress.
+ if (prod1 != SI_PRODUCTION (si2src))
+ {
+ int prod_state = prod1 ? 0 : 1;
+ gl_list_t prev = parser_prepend (ss->states[prod_state]);
+ gl_list_iterator_t iter = gl_list_iterator (prev);
+ parse_state *ps;
+ while (gl_list_iterator_next (&iter, (const void **)&ps, NULL))
+ {
+ const state_item *psi = parse_state_head (ps);
+ bool guided = bitset_test (guide, psi->state->number);
+ if (!guided && !EXTENDED_SEARCH)
+ continue;
+
+ search_state *copy = copy_search_state (ss);
+ ss_set_parse_state (copy, prod_state, ps);
+ copy->complexity += PRODUCTION_COST;
+ if (!guided)
+ copy->complexity += EXTENDED_COST;
+ ssb_append (copy);
+ }
+ gl_list_free (prev);
+ return;
+ }
+ // The parse state heads are either both production items or both
+ // transition items. So all prepend options will either be
+ // reverse transitions or reverse productions
+ int complexity_cost = prod1 ? PRODUCTION_COST : UNSHIFT_COST;
+ complexity_cost *= 2;
+
+ gl_list_t prev1 = parser_prepend (ss->states[0]);
+ gl_list_t prev2 = parser_prepend (ss->states[1]);
+
+ // loop through each pair of possible prepend states and append search
+ // states for each pair where the parser states correspond to the same
+ // parsed input.
+ gl_list_iterator_t iter1 = gl_list_iterator (prev1);
+ parse_state *ps1;
+ while (gl_list_iterator_next (&iter1, (const void **)&ps1, NULL))
+ {
+ const state_item *psi1 = parse_state_head (ps1);
+ bool guided1 = bitset_test (guide, psi1->state->number);
+ if (!guided1 && !EXTENDED_SEARCH)
+ continue;
+
+ gl_list_iterator_t iter2 = gl_list_iterator (prev2);
+ parse_state *ps2;
+ while (gl_list_iterator_next (&iter2, (const void **)&ps2, NULL))
+ {
+ const state_item *psi2 = parse_state_head (ps2);
+
+ bool guided2 = bitset_test (guide, psi2->state->number);
+ if (!guided2 && !EXTENDED_SEARCH)
+ continue;
+ // Only consider prepend state items that share the same state.
+ if (psi1->state != psi2->state)
+ continue;
+
+ int complexity = ss->complexity;
+ if (prod1)
+ complexity += PRODUCTION_COST * 2;
+ else
+ complexity += UNSHIFT_COST * 2;
+ // penalty for not being along the guide path
+ if (!guided1 || !guided2)
+ complexity += EXTENDED_COST;
+ ssb_append (new_search_state (ps1, ps2, complexity));
+ }
+ }
+ gl_list_free (prev1);
+ gl_list_free (prev2);
+}
+
+/**
+ * Determine if the productions associated with the given parser items have
+ * the same prefix up to the dot.
+ */
+static bool
+has_common_prefix (const item_number *itm1, const item_number *itm2)
+{
+ int i = 0;
+ for (; !item_number_is_rule_number (*(itm1 + i)); ++i)
+ if (*(itm1 + i) != *(itm2 + i))
+ return false;
+ return item_number_is_rule_number (*(itm2 + i));
+}
+
+/*
+ * Calculate the start and end locations of an item in ritem.
+ */
+static void
+item_rule_bounds (const item_number *item, const item_number **start,
+ const item_number **end)
+{
+ const item_number *s, *e;
+ for (s = item;
+ s > ritem && item_number_is_symbol_number (*(s - 1));
+ --s);
+ *start = s;
+
+ for (e = item; item_number_is_symbol_number (*e); ++e);
+ *end = e;
+}
+
+/*
+ * Perform the appropriate possible parser actions
+ * on a search state and add the results to the
+ * search state priority queue.
+ */
+static inline void
+generate_next_states (search_state *ss, state_item *conflict1,
+ state_item *conflict2)
+{
+ // Compute the successor configurations.
+ parse_state *ps1 = ss->states[0];
+ parse_state *ps2 = ss->states[1];
+ const state_item *si1 = parse_state_tail (ps1);
+ const state_item *si2 = parse_state_tail (ps2);
+ bool si1reduce = item_number_is_rule_number (*si1->item);
+ bool si2reduce = item_number_is_rule_number (*si2->item);
+ if (!si1reduce && !si2reduce)
+ {
+ // Transition if both paths end at the same symbol
+ if (*si1->item == *si2->item)
+ {
+ int complexity = ss->complexity + 2 * SHIFT_COST;
+ gl_list_t trans1 = simulate_transition (ps1);
+ gl_list_t trans2 = simulate_transition (ps2);
+ gl_list_iterator_t it1 = gl_list_iterator (trans1);
+ parse_state *tps1;
+ while (gl_list_iterator_next (&it1, (const void **) &tps1, NULL))
+ {
+ gl_list_iterator_t it2 = gl_list_iterator (trans2);
+ parse_state *tps2;
+ while (gl_list_iterator_next
+ (&it2, (const void **) &tps2, NULL))
+ ssb_append (new_search_state (tps1, tps2, complexity));
+ }
+ gl_list_free (trans1);
+ gl_list_free (trans2);
+ }
+
+ // Take production steps if possible.
+ production_step (ss, 0);
+ production_step (ss, 1);
+ }
+ // One of the states requires a reduction
+ else
+ {
+ const item_number *rhs1, *rhe1;
+ item_rule_bounds (si1->item, &rhs1, &rhe1);
+ int len1 = rhe1 - rhs1;
+ int size1 = parse_state_length (ps1);
+ bool ready1 = si1reduce && len1 < size1;
+
+ const item_number *rhs2, *rhe2;
+ item_rule_bounds (si2->item, &rhs2, &rhe2);
+ int len2 = rhe2 - rhs2;
+ int size2 = parse_state_length (ps2);
+ bool ready2 = si2reduce && len2 < size2;
+ // If there is a path ready for reduction
+ // without being prepended further, reduce.
+ if (ready1)
+ {
+ gl_list_t reduced1 = reduction_step (ss, conflict1->item, 0, len1);
+ gl_list_iterator_t iter = gl_list_iterator (reduced1);
+ search_state *red1;
+ if (ready2)
+ {
+ gl_list_add_last (reduced1, ss);
+ while (gl_list_iterator_next
+ (&iter, (const void **) &red1, NULL))
+ {
+ gl_list_t reduced2 =
+ reduction_step (red1, conflict2->item, 1, len2);
+ gl_list_iterator_t iter2 = gl_list_iterator (reduced2);
+ search_state *red2;
+ while (gl_list_iterator_next
+ (&iter2, (const void **) &red2, NULL))
+ ssb_append (red2);
+ // avoid duplicates
+ if (red1 != ss)
+ ssb_append (red1);
+ gl_list_free (reduced2);
+ }
+ }
+ else
+ while (gl_list_iterator_next (&iter, (const void **) &red1, NULL))
+ ssb_append (red1);
+ gl_list_free (reduced1);
+ }
+ else if (ready2)
+ {
+ gl_list_t reduced2 = reduction_step (ss, conflict2->item, 1, len2);
+ gl_list_iterator_t iter2 = gl_list_iterator (reduced2);
+ search_state *red2;
+ while (gl_list_iterator_next (&iter2, (const void **) &red2, NULL))
+ ssb_append (red2);
+ gl_list_free (reduced2);
+ }
+ /* Both states end with a reduction, yet they don't have enough symbols
+ * to reduce. This means symbols are missing from the beginning of the
+ * rule, so we must prepend */
+ else
+ {
+ symbol_number sym;
+ if (si1reduce && !ready1)
+ sym = *(rhe1 - size1);
+ else
+ sym = *(rhe2 - size2);
+ search_state_prepend (ss, sym,
+ parse_state_depth (ss->states[0]) >= 0
+ ? rpp_set : scp_set);
+ }
+ }
+}
+
+/*
+ * Perform the actual counter example search,
+ * keeps track of what stage of the search algorithm
+ * we are at and gives the appropriate counterexample
+ * type based off of time constraints.
+ */
+counterexample *
+unifying_example (state_item_number itm1,
+ state_item_number itm2,
+ bool shift_reduce,
+ gl_list_t reduce_path, symbol_number next_sym)
+{
+ state_item *conflict1 = state_items + itm1;
+ state_item *conflict2 = state_items + itm2;
+ search_state *initial = initial_search_state (conflict1, conflict2);
+ ssb_queue = gl_list_create_empty (GL_RBTREEHASH_LIST,
+ (gl_listelement_equals_fn) ssb_equals,
+ (gl_listelement_hashcode_fn) ssb_hasher,
+ (gl_listelement_dispose_fn) ssb_free,
+ false);
+ visited =
+ hash_initialize (32, NULL, (Hash_hasher) visited_hasher,
+ (Hash_comparator) visited_comparator,
+ (Hash_data_freer) search_state_free);
+ ssb_append (initial);
+ time_t start = time (NULL);
+ bool assurance_printed = false;
+ search_state *stage3result = NULL;
+ counterexample *cex = NULL;
+ while (gl_list_size (ssb_queue) > 0)
+ {
+ const search_state_bundle *ssb = gl_list_get_at (ssb_queue, 0);
+ gl_list_iterator_t it = gl_list_iterator (ssb->states);
+ search_state *ss;
+ while (gl_list_iterator_next (&it, (const void **) &ss, NULL))
+ {
+ if (trace_flag & trace_cex)
+ search_state_print (ss);
+ // Stage 1/2 completing the rules containing the conflicts
+ parse_state *ps1 = ss->states[0];
+ parse_state *ps2 = ss->states[1];
+ if (parse_state_depth (ps1) < 0 && parse_state_depth (ps2) < 0)
+ {
+ // Stage 3: reduce and shift conflict items completed.
+ const state_item *si1src = parse_state_head (ps1);
+ const state_item *si2src = parse_state_head (ps2);
+ if (item_rule (si1src->item)->lhs == item_rule (si2src->item)->lhs
+ && has_common_prefix (si1src->item, si2src->item))
+ {
+ // Stage 4: both paths share a prefix
+ const derivation *d1 = parse_state_derivation (ps1);
+ const derivation *d2 = parse_state_derivation (ps2);
+ if (parse_state_derivation_completed (ps1)
+ && parse_state_derivation_completed (ps2)
+ && d1->sym == d2->sym)
+ {
+ // Once we have two derivations for the same symbol,
+ // 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);
+ goto cex_search_end;
+ }
+ if (!stage3result)
+ stage3result = ss;
+ }
+ }
+ if (TIME_LIMIT_ENFORCED)
+ {
+ float time_passed = difftime (time (NULL), start);
+ if (!assurance_printed && time_passed > ASSURANCE_LIMIT
+ && stage3result)
+ {
+ puts
+ ("Productions leading up to the conflict state found. Still finding a possible unifying counterexample...");
+ assurance_printed = true;
+ }
+ if (time_passed > TIME_LIMIT)
+ {
+ printf ("time limit exceeded: %f\n", time_passed);
+ goto cex_search_end;
+ }
+ }
+ generate_next_states (ss, conflict1, conflict2);
+ }
+ gl_sortedlist_remove (ssb_queue,
+ (gl_listelement_compar_fn) ssb_comp, ssb);
+ }
+cex_search_end:;
+ if (!cex)
+ {
+ // No unifying counterexamples
+ // 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);
+ // Otherwise, construct a nonunifying counterexample that
+ // begins from the start state using the shortest
+ // lookahead-sensitive path to the reduce item.
+ else
+ cex = example_from_path (shift_reduce, itm2, reduce_path, next_sym);
+ }
+ gl_list_free (ssb_queue);
+ hash_free (visited);
+ return cex;
+}
+
+static time_t cumulative_time;
+
+void
+counterexample_init (void)
+{
+ time (&cumulative_time);
+ scp_set = bitset_create (nstates, BITSET_FIXED);
+ rpp_set = bitset_create (nstates, BITSET_FIXED);
+ state_items_init ();
+}
+
+
+void
+counterexample_free (void)
+{
+ if (scp_set)
+ {
+ bitset_free (scp_set);
+ bitset_free (rpp_set);
+ state_items_free ();
+ }
+}
+
+/**
+ * Report a counterexample for conflict on symbol next_sym
+ * between the given state-items
+ */
+static void
+counterexample_report (state_item_number itm1, state_item_number itm2,
+ symbol_number next_sym, bool shift_reduce)
+{
+ // Compute the shortest lookahead-sensitive path and associated sets of
+ // parser states.
+ gl_list_t shortest_path = shortest_path_from_start (itm1, next_sym);
+ bool reduceProdReached = false;
+ const rule *reduce_rule = item_rule (state_items[itm1].item);
+
+ bitset_zero (scp_set);
+ bitset_zero (rpp_set);
+ gl_list_iterator_t it = gl_list_iterator (shortest_path);
+ state_item *si;
+ while (gl_list_iterator_next (&it, (const void **) &si, NULL))
+ {
+ bitset_set (scp_set, si->state->number);
+ reduceProdReached = reduceProdReached
+ || item_rule (si->item) == reduce_rule;
+ if (reduceProdReached)
+ bitset_set (rpp_set, si->state->number);
+ }
+ time_t t = time (NULL);
+ counterexample *cex = difftime (t,
+ cumulative_time) <
+ CUMULATIVE_TIME_LIMIT ? unifying_example (itm1, itm2, shift_reduce,
+ shortest_path,
+ next_sym) :
+ example_from_path (shift_reduce, itm2, shortest_path, next_sym);
+
+ gl_list_free (shortest_path);
+ print_counterexample (cex);
+
+}
+
+void
+counterexample_report_shift_reduce (state_item_number itm1, state_item_number itm2,
+ symbol_number next_sym)
+{
+ puts ("Shift-Reduce Conflict:");
+ print_state_item (&state_items[itm1], stdout);
+ print_state_item (&state_items[itm2], stdout);
+ printf ("On Symbol: %s\n", symbols[next_sym]->tag);
+ counterexample_report (itm1, itm2, next_sym, true);
+}
+
+void
+counterexample_report_reduce_reduce (state_item_number itm1, state_item_number itm2,
+ bitset conflict_syms)
+{
+ puts ("Reduce-Reduce Conflict:");
+ print_state_item (&state_items[itm1], stdout);
+ print_state_item (&state_items[itm2], stdout);
+ fputs ("On Symbols: {", stdout);
+ bitset_iterator biter;
+ state_item_number sym;
+ BITSET_FOR_EACH (biter, conflict_syms, sym, 0)
+ {
+ printf ("%s,", symbols[sym]->tag);
+ }
+ fputs ("}\n", stdout);
+ counterexample_report (itm1, itm2, bitset_first (conflict_syms), false);
+}
\ No newline at end of file
diff --git a/src/counterexample.h b/src/counterexample.h
new file mode 100644
index 00000000..8f37db5b
--- /dev/null
+++ b/src/counterexample.h
@@ -0,0 +1,35 @@
+/* Conflict counterexample generation
+
+ Copyright (C) 2019-2020 Free Software Foundation, Inc.
+
+ This file is part of Bison, the GNU Compiler Compiler.
+
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>. */
+
+#ifndef COUNTEREXAMPLE_H
+#define COUNTEREXAMPLE_H
+
+#include "state-item.h"
+
+void counterexample_init (void);
+void counterexample_free (void);
+
+void counterexample_report_shift_reduce (state_item_number itm1,
+ state_item_number itm2,
+ symbol_number next_sym);
+
+void counterexample_report_reduce_reduce (state_item_number itm1,
+ state_item_number itm2,
+ bitset conflict_syms);
+#endif /* COUNTEREXAMPLE_H */
--
2.20.1 (Apple Git-117)