Future/bison
1
0
Fork 0
mirror of https://git.savannah.gnu.org/git/bison.git synced 2026-03-13 14:23:04 +00:00
Code Issues Packages Projects Releases Wiki Activity

cex: provide the user with a means to change the timeout

Browse Source 
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.
This commit is contained in:
Akim Demaille
2022-09-13 08:25:59 +02:00
parent 15b97a0a6a
commit c025891547
9 changed files with 48 additions and 18 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
src/counterexample.c
View File

@@ -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);

3
src/muscle-tab.c
View File

@@ -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"));
}

5
src/state-item.c
View File

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