From af0441cfd214b6fd322579d91c0588f50666eb50 Mon Sep 17 00:00:00 2001 From: Vincent Imbimbo Date: Tue, 12 May 2020 22:01:08 -0400 Subject: [PATCH] cex: bind counterexample generation * src/complain.h, src/complain.c: Add support for -Wcounterexample. * src/conflicts.c (report_counterexamples): New. (rule_conflicts_print): Use it when -Wcounterexample is given. * src/getargs.h, src/getargs.c: Add support for --trace=cex. * src/main.c (main): Init and deinit counterexample generation. --- src/complain.c | 2 ++ src/complain.h | 4 ++- src/conflicts.c | 69 +++++++++++++++++++++++++++++++++++++++++++++++++ src/getargs.c | 2 ++ src/getargs.h | 1 + src/local.mk | 10 +++++++ src/main.c | 4 +++ 7 files changed, 91 insertions(+), 1 deletion(-) diff --git a/src/complain.c b/src/complain.c index 6a78d40e..1c2ba797 100644 --- a/src/complain.c +++ b/src/complain.c @@ -114,6 +114,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") }, { "dangling-alias", N_("string aliases not attached to a symbol") }, { "deprecated", N_("obsolete constructs") }, { "empty-rule", N_("empty rules without %empty") }, @@ -133,6 +134,7 @@ static const argmatch_warning_arg argmatch_warning_args[] = { "all", Wall }, { "conflicts-rr", Wconflicts_rr }, { "conflicts-sr", Wconflicts_sr }, + { "counterexample", Wcounterexample }, { "dangling-alias", Wdangling_alias }, { "deprecated", Wdeprecated }, { "empty-rule", Wempty_rule }, diff --git a/src/complain.h b/src/complain.h index a6f0253a..63a14f76 100644 --- a/src/complain.h +++ b/src/complain.h @@ -46,6 +46,7 @@ typedef enum { warning_conflicts_rr, warning_conflicts_sr, + warning_counterexample, warning_dangling_alias, warning_deprecated, warning_empty_rule, @@ -106,6 +107,7 @@ typedef enum Wconflicts_rr = 1 << warning_conflicts_rr, Wconflicts_sr = 1 << warning_conflicts_sr, + Wcounterexample = 1 << warning_counterexample, Wdangling_alias = 1 << warning_dangling_alias, Wdeprecated = 1 << warning_deprecated, Wempty_rule = 1 << warning_empty_rule, @@ -122,7 +124,7 @@ typedef enum /**< All above warnings. */ Weverything = ~complaint & ~fatal & ~silent, - Wall = Weverything & ~Wdangling_alias & ~Wyacc + Wall = Weverything & ~Wcounterexample & ~Wdangling_alias & ~Wyacc } warnings; /** Whether the warnings of \a flags are all unset. diff --git a/src/conflicts.c b/src/conflicts.c index 5ecd7d17..3cf21c47 100644 --- a/src/conflicts.c +++ b/src/conflicts.c @@ -25,6 +25,7 @@ #include "complain.h" #include "conflicts.h" +#include "counterexample.h" #include "files.h" #include "getargs.h" #include "gram.h" @@ -624,6 +625,72 @@ conflicts_total_count (void) return count_sr_conflicts () + count_rr_conflicts (); } +static void +report_state_counterexamples (const state *s) +{ + const state_number sn = s->number; + const 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 +report_counterexamples (void) +{ + for (state_number sn = 0; sn < nstates; ++sn) + if (conflicts[sn]) + report_state_counterexamples (states[sn]); +} + /*------------------------------. | Reporting per-rule conflicts. | `------------------------------*/ @@ -653,6 +720,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 4815eaa2..2c65e7b5 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 39741926..524f56bd 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 c072d998..d96ecc45 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 f758a1c3..30e3ca69 100644 --- a/src/main.c +++ b/src/main.c @@ -33,6 +33,7 @@ #include "complain.h" #include "conflicts.h" +#include "counterexample.h" #include "derives.h" #include "files.h" #include "fixits.h" @@ -144,6 +145,8 @@ main (int argc, char *argv[]) conflicts_update_state_numbers (old_to_new, nstates_old); free (old_to_new); } + if (warning_is_enabled (Wcounterexample)) + counterexample_init (); conflicts_print (); timevar_pop (tv_conflicts); @@ -217,6 +220,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