From c0258915474496874318f4767ba6ebcc1e9471f0 Mon Sep 17 00:00:00 2001 From: Akim Demaille Date: Tue, 13 Sep 2022 08:25:59 +0200 Subject: cex: provide the user with a means to change the timeout Reported by Frank Heckenbach. https://lists.gnu.org/r/bug-bison/2022-07/msg00011.html * bootstrap.conf: Use c_strtod, so that even in French locales "1.5" is accepted, instead of "1,5". * src/counterexample.c, src/state-item.c: Use xtime_t instead of time_t, so that accuracy goes from seconds to nanoseconds. ( counterexample_init): Depend on cex.timeout rather than $TIME_LIMIT. * doc/bison.texi (%define Summary): Document cex.timeout. --- NEWS | 4 ++++ bootstrap.conf | 4 ++-- doc/bison.texi | 17 +++++++++++++++++ lib/.gitignore | 2 ++ m4/.gitignore | 2 ++ src/counterexample.c | 27 ++++++++++++++------------- src/muscle-tab.c | 3 +++ src/state-item.c | 5 +++-- tests/conflicts.at | 2 +- 9 files changed, 48 insertions(+), 18 deletions(-) diff --git a/NEWS b/NEWS index f480cb95..40199a7a 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,10 @@ GNU Bison NEWS The C++ skeletons now expose copy and move operators for symbols. + The `cex.timeout` %define variable allows to control when we give up + finding a unifying counterexample. For instance `bison -Wcex + -Dcex.timeout=.5 gram.y` to limit to 1/2s. + * Noteworthy changes in release 3.8.2 (2021-09-25) [stable] Fixed portability issues of bison on Cygwin. diff --git a/bootstrap.conf b/bootstrap.conf index 9a6070ba..fbe89422 100644 --- a/bootstrap.conf +++ b/bootstrap.conf @@ -19,7 +19,7 @@ gnulib_modules=' argmatch array-list assert assure attribute bitsetv - calloc-posix close closeout config-h c-strcase + calloc-posix close closeout config-h c-strcase c-strtod configmake dirname error execute extensions @@ -44,7 +44,7 @@ gnulib_modules=' realloc-posix relocatable-prog relocatable-script rename - spawn-pipe stdbool stpcpy stpncpy strdup-posix strerror strtod strverscmp + spawn-pipe stdbool stpcpy stpncpy strdup-posix strerror strverscmp sys_ioctl termios timevar diff --git a/doc/bison.texi b/doc/bison.texi index b2eddcf8..5ffe21d0 100644 --- a/doc/bison.texi +++ b/doc/bison.texi @@ -6894,6 +6894,23 @@ Introduced in Bison 3.0.3. @c api.value.union.name +@c ================================================== cex.timeout + +@deffn Directive {%define cex.timeout} @var{duration} + +@itemize @bullet +@item Language(s): all + +@item Purpose: +Define the time limit for finding unifying counterexamples. + +@item Accepted Values: duration in seconds, e.g., @samp{1}, @samp{0.5}. + +@item Default Value: 5 +@end itemize +@end deffn + + @c ================================================== lr.default-reduction @deffn Directive {%define lr.default-reduction} @var{when} diff --git a/lib/.gitignore b/lib/.gitignore index 03d09956..9f15868f 100644 --- a/lib/.gitignore +++ b/lib/.gitignore @@ -40,6 +40,8 @@ /c-strcasecmp.c /c-strcaseeq.h /c-strncasecmp.c +/c-strtod.c +/c-strtod.h /calloc.c /canonicalize-lgpl.c /canonicalize.c diff --git a/m4/.gitignore b/m4/.gitignore index c3a50c44..4748c6e0 100644 --- a/m4/.gitignore +++ b/m4/.gitignore @@ -7,6 +7,7 @@ /asm-underscore.m4 /assert.m4 /builtin-expect.m4 +/c-strtod.m4 /calloc.m4 /canonicalize.m4 /chdir-long.m4 @@ -83,6 +84,7 @@ /include_next.m4 /inline.m4 /intdiv0.m4 +/intl-thread-locale.m4 /intl.m4 /intldir.m4 /intlmacosx.m4 diff --git a/src/counterexample.c b/src/counterexample.c index 71436fd6..8a4f8b2c 100644 --- a/src/counterexample.c +++ b/src/counterexample.c @@ -23,7 +23,9 @@ #include "system.h" +#include #include +#include #include #include #include @@ -39,6 +41,7 @@ #include "gram.h" #include "lalr.h" #include "lssi.h" +#include "muscle-tab.h" #include "nullable.h" #include "parse-simulation.h" @@ -1115,7 +1118,7 @@ unifying_example (state_item_number itm1, (Hash_comparator) visited_comparator, (Hash_data_freer) search_state_free); ssb_append (initial); - time_t start = time (NULL); + xtime_t start = gethrxtime (); bool assurance_printed = false; search_state *stage3result = NULL; counterexample *cex = NULL; @@ -1160,7 +1163,7 @@ unifying_example (state_item_number itm1, } if (TIME_LIMIT_ENFORCED) { - double time_passed = difftime (time (NULL), start); + double time_passed = (gethrxtime () - start) / 1e9; if (!assurance_printed && time_passed > ASSURANCE_LIMIT && stage3result) { @@ -1201,25 +1204,24 @@ cex_search_end:; return cex; } -static time_t cumulative_time; +static xtime_t cumulative_time; void counterexample_init (void) { - /* Recognize $TIME_LIMIT. Not a public feature, just to help - debugging. If we need something public, a %define/-D/-F variable - would be more appropriate. */ { - const char *cp = getenv ("TIME_LIMIT"); - if (cp) + char *cp = muscle_percent_define_get ("cex.timeout"); + if (*cp != '\0') { char *end = NULL; - double v = strtod (cp, &end); + double v = c_strtod (cp, &end); if (*end == '\0' && errno == 0) time_limit = v; + fprintf (stderr, "lim: %f from %s\n", time_limit, cp); } - } - time (&cumulative_time); + free (cp); + } + cumulative_time = gethrxtime (); scp_set = bitset_create (nstates, BITSET_FIXED); rpp_set = bitset_create (nstates, BITSET_FIXED); state_items_init (); @@ -1266,9 +1268,8 @@ counterexample_report (state_item_number itm1, state_item_number itm2, if (reduce_prod_reached) bitset_set (rpp_set, si->state->number); } - time_t t = time (NULL); counterexample *cex - = difftime (t, cumulative_time) < CUMULATIVE_TIME_LIMIT + = (gethrxtime () - cumulative_time) / 1e9 < CUMULATIVE_TIME_LIMIT ? unifying_example (itm1, itm2, shift_reduce, shortest_path, next_sym) : example_from_path (shift_reduce, itm2, shortest_path, next_sym); diff --git a/src/muscle-tab.c b/src/muscle-tab.c index 0945d609..f4d84d6a 100644 --- a/src/muscle-tab.c +++ b/src/muscle-tab.c @@ -127,6 +127,9 @@ muscle_init (void) muscle_table = hash_xinitialize (HT_INITIAL_CAPACITY, NULL, hash_muscle, hash_compare_muscles, muscle_entry_free); + /* Avoid warnings if the user defined this variable, but did not + actually call -Wcex. */ + free (muscle_percent_define_get ("cex.timeout")); } diff --git a/src/state-item.c b/src/state-item.c index c9635c6a..cc1602cc 100644 --- a/src/state-item.c +++ b/src/state-item.c @@ -22,6 +22,7 @@ #include "state-item.h" #include +#include #include #include #include @@ -533,7 +534,7 @@ state_items_report (FILE *out) void state_items_init (void) { - time_t start = time (NULL); + xtime_t start = gethrxtime (); init_state_items (); init_trans (); init_prods (); @@ -542,7 +543,7 @@ state_items_init (void) prune_disabled_paths (); if (trace_flag & trace_cex) { - fprintf (stderr, "init: %f\n", difftime (time (NULL), start)); + fprintf (stderr, "state_items_init: %.3fs\n", (gethrxtime () - start) / 1e9); state_items_report (stderr); } } diff --git a/tests/conflicts.at b/tests/conflicts.at index 52caa208..4356b6b8 100644 --- a/tests/conflicts.at +++ b/tests/conflicts.at @@ -1958,7 +1958,7 @@ empty_c3: %prec 'c' ; AT_BISON_CHECK([[--trace=cex -fcaret --report=all -o input.c input.y]], 0, [], [[bison (GNU Bison) ]AT_PACKAGE_VERSION[ -init: 0.000000 +state_items_init: 0.000s # state items: 26 State 0: 0 $accept: . start $end -- cgit v1.2.1