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.

3 files changed, 20 insertions, 15 deletions

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..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 <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);
     }
 }