Re: Counterexamples timeout

[Akim Demaille]

Hi Frank,

> Le 29 juil. 2022 à 14:09, Frank Heckenbach <f.heckenbach@fh-soft.de> a écrit :
> 
> Hi,
> 
> I don't know if it's something peculiar about my grammars, but it
> seems when using "-Wcounterexamples", Bison either finds
> counterexamples almost immediately or runs into the timeout.
> (Or maybe 6 seconds (see below) are just so eternally long to a
> modern CPU that there's not much between that and infinity. ;)
> [...]

I agree.  Let's change that.  What do you think about this proposal?

commit 6a15951030ade757de13159e545394af3cd40205
Author: Akim Demaille <akim.demaille@gmail.com>
Date:   Tue Sep 13 08:25:59 2022 +0200

    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.

diff --git a/NEWS b/NEWS
index f480cb95..32e7361a 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 give 1/2s of credit.
+
 * 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..d0074765 100644
--- a/doc/bison.texi
+++ b/doc/bison.texi
@@ -6894,6 +6894,23 @@ @node %define Summary
 @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 credit allocated to 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 <c-strtod.h>
 #include <errno.h>
+#include <gethrxtime.h>
 #include <gl_linked_list.h>
 #include <gl_rbtreehash_list.h>
 #include <hash.h>
@@ -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..40295542 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 called -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 <assert.h>
+#include <gethrxtime.h>
 #include <gl_linked_list.h>
 #include <gl_xlist.h>
 #include <stdlib.h>
@@ -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 @@ AT_SETUP([[%nonassoc error actions for multiple 
reductions in a state]])
 
 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