[PATCH 4/5] counterexample generation integration
Vincent Imbimbo <[email protected]>
| Newsgroups | gmane.comp.parsers.bison.patches |
|---|---|
| Message-ID | <[email protected]> |
---
src/complain.c | 2 ++
src/complain.h | 2 ++
src/conflicts.c | 67 +++++++++++++++++++++++++++++++++++++++++++++++++
src/getargs.c | 2 ++
src/getargs.h | 1 +
src/local.mk | 10 ++++++++
src/main.c | 3 +++
7 files changed, 87 insertions(+)
diff --git a/src/complain.c b/src/complain.c
index 87563d59..e4037c5e 100644
--- a/src/complain.c
+++ b/src/complain.c
@@ -113,6 +113,7 @@ static const argmatch_warning_doc argmatch_warning_docs[] =
{
{ "conflicts-sr", N_("S/R conflicts (enabled by default)") },
{ "conflicts-rr", N_("R/R conflicts (enabled by default)") },
+ { "counterexample", N_("Conflict counter examples") },
{ "deprecated", N_("obsolete constructs") },
{ "empty-rule", N_("empty rules without %empty") },
{ "midrule-values", N_("unset or unused midrule values") },
@@ -133,6 +134,7 @@ static const argmatch_warning_arg argmatch_warning_args[] =
{ "yacc", Wyacc },
{ "conflicts-sr", Wconflicts_sr },
{ "conflicts-rr", Wconflicts_rr },
+ { "counterexample", Wcounterexample },
{ "deprecated", Wdeprecated },
{ "empty-rule", Wempty_rule },
{ "precedence", Wprecedence },
diff --git a/src/complain.h b/src/complain.h
index 4b73d08d..dfe7bcc4 100644
--- a/src/complain.h
+++ b/src/complain.h
@@ -47,6 +47,7 @@ typedef enum
{
warning_conflicts_rr,
warning_conflicts_sr,
+ warning_counterexample,
warning_deprecated,
warning_empty_rule,
warning_midrule_values,
@@ -104,6 +105,7 @@ typedef enum
Wconflicts_rr = 1 << warning_conflicts_rr,
Wconflicts_sr = 1 << warning_conflicts_sr,
+ Wcounterexample = 1 << warning_counterexample,
Wdeprecated = 1 << warning_deprecated,
Wempty_rule = 1 << warning_empty_rule,
Wmidrule_values = 1 << warning_midrule_values,
diff --git a/src/conflicts.c b/src/conflicts.c
index cfc729aa..01598049 100644
--- a/src/conflicts.c
+++ b/src/conflicts.c
@@ -34,6 +34,7 @@
#include "reader.h"
#include "state.h"
#include "symtab.h"
+#include "counterexample.h"
/* -1 stands for not specified. */
int expected_sr_conflicts = -1;
@@ -628,6 +629,70 @@ conflicts_total_count (void)
| Reporting per-rule conflicts. |
`------------------------------*/
+static void
+report_counterexamples ()
+{
+ for (state_number sn = 0; sn < nstates; ++sn)
+ {
+ if (conflicts[sn])
+ {
+ state *s = states[sn];
+ reductions *reds = s->reductions;
+ for (int i = 0; i < reds->num; ++i)
+ {
+ rule *r1 = reds->rules[i];
+ state_item_number c1;
+ for (int j = state_item_map[sn];
+ j < state_item_map[sn + 1]; ++j)
+ {
+ if (item_number_as_rule_number (*state_items[j].item) == r1->number)
+ {
+ c1 = j;
+ break;
+ }
+ }
+
+ for (int j = state_item_map[sn];
+ j < state_item_map[sn + 1]; ++j)
+ {
+ if (SI_DISABLED (j))
+ continue;
+ state_item *si = state_items + j;
+ item_number conf = *si->item;
+ if (item_number_is_symbol_number (conf) &&
+ bitset_test (reds->lookahead_tokens[i], conf))
+ {
+ counterexample_report_shift_reduce (c1, j, conf);
+ break;
+ }
+ }
+ for (int j = i+1; j < reds->num; ++j)
+ {
+ bitset conf = bitset_create (ntokens, BITSET_FIXED);
+ bitset_intersection (conf,
+ reds->lookahead_tokens[i],
+ reds->lookahead_tokens[j]);
+ if (!bitset_empty_p (conf))
+ {
+ rule *r2 = reds->rules[j];
+ for (int k = state_item_map[sn];
+ k < state_item_map[sn + 1]; ++k)
+ {
+ state_item *si = state_items + k;
+ const rule *r = item_rule (si->item);
+ if (r == r2)
+ {
+ counterexample_report_reduce_reduce (c1, k, conf);
+ break;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
static void
rule_conflicts_print (void)
{
@@ -653,6 +718,8 @@ rule_conflicts_print (void)
r->user_number, rr, expected_rr);
}
}
+ if (warning_is_enabled (Wcounterexample))
+ report_counterexamples ();
}
/*---------------------------------.
diff --git a/src/getargs.c b/src/getargs.c
index bf4a938f..7544ec22 100644
--- a/src/getargs.c
+++ b/src/getargs.c
@@ -261,6 +261,7 @@ static const argmatch_trace_doc argmatch_trace_docs[] =
{ "skeleton", "skeleton postprocessing" },
{ "time", "time consumption" },
{ "ielr", "IELR conversion" },
+ { "cex", "counterexample generation"},
{ "all", "all of the above" },
{ NULL, NULL},
};
@@ -283,6 +284,7 @@ static const argmatch_trace_arg argmatch_trace_args[] =
{ "skeleton", trace_skeleton },
{ "time", trace_time },
{ "ielr", trace_ielr },
+ { "cex", trace_cex },
{ "all", trace_all },
{ NULL, trace_none},
};
diff --git a/src/getargs.h b/src/getargs.h
index ab6af6c3..598fce4f 100644
--- a/src/getargs.h
+++ b/src/getargs.h
@@ -105,6 +105,7 @@ enum trace
trace_ielr = 1 << 12, /**< IELR conversion. */
trace_closure = 1 << 13, /**< Input/output of closure(). */
trace_locations = 1 << 14, /**< Full display of locations. */
+ trace_cex = 1 << 15, /**< Counterexample generation */
trace_all = ~0 /**< All of the above. */
};
/** What debug items bison displays during its run. */
diff --git a/src/local.mk b/src/local.mk
index ee8ec03b..8b28800f 100644
--- a/src/local.mk
+++ b/src/local.mk
@@ -40,6 +40,10 @@ src_bison_SOURCES = \
src/complain.h \
src/conflicts.c \
src/conflicts.h \
+ src/counterexample.c \
+ src/counterexample.h \
+ src/derivation.c \
+ src/derivation.h \
src/derives.c \
src/derives.h \
src/files.c \
@@ -61,6 +65,8 @@ src_bison_SOURCES = \
src/location.h \
src/lr0.c \
src/lr0.h \
+ src/lssi.c \
+ src/lssi.h \
src/main.c \
src/muscle-tab.c \
src/muscle-tab.h \
@@ -71,6 +77,8 @@ src_bison_SOURCES = \
src/output.c \
src/output.h \
src/parse-gram.y \
+ src/parse-simulation.c \
+ src/parse-simulation.h \
src/print-graph.c \
src/print-graph.h \
src/print-xml.c \
@@ -91,6 +99,8 @@ src_bison_SOURCES = \
src/scan-skel.h \
src/state.c \
src/state.h \
+ src/state-item.c \
+ src/state-item.h \
src/symlist.c \
src/symlist.h \
src/symtab.c \
diff --git a/src/main.c b/src/main.c
index 258a6d1e..cbae8fbc 100644
--- a/src/main.c
+++ b/src/main.c
@@ -55,6 +55,7 @@
#include "symtab.h"
#include "tables.h"
#include "uniqstr.h"
+#include "counterexample.h"
int
@@ -144,6 +145,7 @@ main (int argc, char *argv[])
conflicts_update_state_numbers (old_to_new, nstates_old);
free (old_to_new);
}
+ counterexample_init ();
conflicts_print ();
timevar_pop (tv_conflicts);
@@ -217,6 +219,7 @@ main (int argc, char *argv[])
reduce_free ();
conflicts_free ();
grammar_free ();
+ counterexample_free ();
output_file_names_free ();
/* The scanner memory cannot be released right after parsing, as it
--
2.20.1 (Apple Git-117)