1 /* Counterexample Generation Search Nodes
2
3 Copyright (C) 2020-2021 Free Software Foundation, Inc.
4
5 This file is part of Bison, the GNU Compiler Compiler.
6
7 This program is free software: you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation, either version 3 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program. If not, see <https://www.gnu.org/licenses/>. */
19
20 #include <config.h>
21
22 #include "state-item.h"
23
24 #include <assert.h>
25 #include <gl_linked_list.h>
26 #include <gl_xlist.h>
27 #include <stdlib.h>
28 #include <time.h>
29
30 #include "closure.h"
31 #include "getargs.h"
32 #include "nullable.h"
33
34 size_t nstate_items;
35 state_item_number *state_item_map;
36 state_item *state_items;
37
38 // Hash functions for index -> bitset hash maps.
39 typedef struct
40 {
41 int key;
42 bitset l;
43 } hash_pair;
44
45 static size_t
46 hash_pair_hasher (const hash_pair *sl, size_t max)
47 {
48 return sl->key % max;
49 }
50
51 static bool
52 hash_pair_comparator (const hash_pair *l, const hash_pair *r)
53 {
54 return l->key == r->key;
55 }
56
57 static void
58 hash_pair_free (hash_pair *hp)
59 {
60 bitset_free (hp->l);
61 free (hp);
62 }
63
64 static Hash_table *
65 hash_pair_table_create (int size)
66 {
67 return hash_xinitialize (size,
68 NULL,
69 (Hash_hasher) hash_pair_hasher,
70 (Hash_comparator) hash_pair_comparator,
71 (Hash_data_freer) hash_pair_free);
72 }
73
74 static bitset
75 hash_pair_lookup (Hash_table *tab, int key)
76 {
77 hash_pair probe;
78 probe.key = key;
79 hash_pair *hp = hash_lookup (tab, &probe);
80 return hp ? hp->l : NULL;
81 }
82
83 static void
84 hash_pair_insert (Hash_table *tab, int key, bitset val)
85 {
86 hash_pair *hp = xmalloc (sizeof *hp);
87 hp->key = key;
88 hp->l = val;
89 hash_pair *res = hash_xinsert (tab, hp);
90 // This must be the first insertion.
91 (void) res;
92 assert (res == hp);
93 }
94
95 /* A state_item from a state's id and the offset of the item within
96 the state. */
97 state_item *
98 state_item_lookup (state_number s, state_item_number off)
99 {
100 return &state_items[state_item_index_lookup (s, off)];
101 }
102
103 static inline void
104 state_item_set (state_item_number sidx, const state *s, item_number off)
105 {
106 state_items[sidx].state = s;
107 state_items[sidx].item = &ritem[off];
108 state_items[sidx].lookahead = NULL;
109 state_items[sidx].trans = -1;
110 state_items[sidx].prods = NULL;
111 state_items[sidx].revs = bitset_create (nstate_items, BITSET_SPARSE);
112 }
113
114 /**
115 * Initialize state_items set
116 */
117 static void
118 init_state_items (void)
119 {
120 nstate_items = 0;
121 bitsetv production_items = bitsetv_create (nstates, nritems, BITSET_SPARSE);
122 for (int i = 0; i < nstates; ++i)
123 {
124 const state *s = states[i];
125 nstate_items += s->nitems;
126 closure (s->items, s->nitems);
127 for (size_t j = 0; j < nitemset; ++j)
128 if (0 < itemset[j]
129 && item_number_is_rule_number (ritem[itemset[j] - 1]))
130 {
131 bitset_set (production_items[i], itemset[j]);
132 ++nstate_items;
133 }
134 }
135 state_item_map = xnmalloc (nstates + 1, sizeof (state_item_number));
136 state_items = xnmalloc (nstate_items, sizeof (state_item));
137 state_item_number sidx = 0;
138 for (int i = 0; i < nstates; ++i)
139 {
140 state_item_map[i] = sidx;
141 int rule_search_idx = 0;
142 const state *s = states[i];
143 const reductions *red = s->reductions;
144 for (int j = 0; j < s->nitems; ++j)
145 {
146 state_item_set (sidx, s, s->items[j]);
147 state_item *si = &state_items[sidx];
148 const rule *r = item_rule (si->item);
149 if (rule_search_idx < red->num && red->rules[rule_search_idx] < r)
150 ++rule_search_idx;
151 if (rule_search_idx < red->num && r == red->rules[rule_search_idx])
152 {
153 bitsetv lookahead = red->lookaheads;
154 if (lookahead)
155 si->lookahead = lookahead[rule_search_idx];
156 }
157 ++sidx;
158 }
159 bitset_iterator biter;
160 item_number off;
161 BITSET_FOR_EACH (biter, production_items[i], off, 0)
162 {
163 state_item_set (sidx, s, off);
164 if (item_number_is_rule_number (ritem[off]))
165 {
166 bitsetv lookahead = red->lookaheads;
167 if (lookahead)
168 state_items[sidx].lookahead = lookahead[rule_search_idx];
169 ++rule_search_idx;
170 }
171 ++sidx;
172 }
173
174 }
175 state_item_map[nstates] = nstate_items;
176 bitsetv_free (production_items);
177 }
178
179 static size_t
180 state_sym_hasher (const void *st, size_t max)
181 {
182 return ((state *) st)->accessing_symbol % max;
183 }
184
185 static bool
186 state_sym_comparator (const void *s1, const void *s2)
187 {
188 return ((state *) s1)->accessing_symbol == ((state *) s2)->accessing_symbol;
189 }
190
191 static state *
192 state_sym_lookup (symbol_number sym, Hash_table *h)
193 {
194 state probe;
195 probe.accessing_symbol = sym;
196 return hash_lookup (h, &probe);
197 }
198
199 static void
200 init_trans (void)
201 {
202 for (state_number i = 0; i < nstates; ++i)
203 {
204 // Generate a hash set that maps from accepting symbols to the states
205 // this state transitions to.
206 state *s = states[i];
207 transitions *t = s->transitions;
208 Hash_table *transition_set
209 = hash_xinitialize (t->num, NULL, (Hash_hasher) state_sym_hasher,
210 (Hash_comparator) state_sym_comparator, NULL);
211 for (int j = 0; j < t->num; ++j)
212 if (!TRANSITION_IS_DISABLED (t, j))
213 hash_xinsert (transition_set, t->states[j]);
214 for (state_item_number j = state_item_map[i]; j < state_item_map[i + 1]; ++j)
215 {
216 item_number *item = state_items[j].item;
217 if (item_number_is_rule_number (*item))
218 continue;
219 state *dst = state_sym_lookup (*item, transition_set);
220 if (!dst)
221 continue;
222 // find the item in the destination state that corresponds
223 // to the transition of item
224 for (int k = 0; k < dst->nitems; ++k)
225 if (item + 1 == ritem + dst->items[k])
226 {
227 state_item_number dstSI =
228 state_item_index_lookup (dst->number, k);
229
230 state_items[j].trans = dstSI;
231 bitset_set (state_items[dstSI].revs, j);
232 break;
233 }
234 }
235 hash_free (transition_set);
236 }
237 }
238
239 static void
240 init_prods (void)
241 {
242 for (int i = 0; i < nstates; ++i)
243 {
244 state *s = states[i];
245 // closure_map is a hash map from nonterminals to a set
246 // of the items that produce those nonterminals
247 Hash_table *closure_map = hash_pair_table_create (nsyms - ntokens);
248
249 // Add the nitems of state to skip to the production portion
250 // of that state's state_items
251 for (state_item_number j = state_item_map[i] + s->nitems;
252 j < state_item_map[i + 1]; ++j)
253 {
254 state_item *src = &state_items[j];
255 item_number *item = src->item;
256 symbol_number lhs = item_rule (item)->lhs->number;
257 bitset itms = hash_pair_lookup (closure_map, lhs);
258 if (!itms)
259 {
260 itms = bitset_create (nstate_items, BITSET_SPARSE);
261 hash_pair_insert (closure_map, lhs, itms);
262 }
263 bitset_set (itms, j);
264 }
265 // For each item with a dot followed by a nonterminal,
266 // try to create a production edge.
267 for (state_item_number j = state_item_map[i]; j < state_item_map[i + 1]; ++j)
268 {
269 state_item *src = &state_items[j];
270 item_number item = *(src->item);
271 // Skip reduce items and items with terminals after the dot
272 if (item_number_is_rule_number (item) || ISTOKEN (item))
273 continue;
274 symbol_number sym = item_number_as_symbol_number (item);
275 bitset lb = hash_pair_lookup (closure_map, sym);
276 if (lb)
277 {
278 bitset copy = bitset_create (nstate_items, BITSET_SPARSE);
279 bitset_copy (copy, lb);
280 // update prods.
281 state_items[j].prods = copy;
282
283 // update revs.
284 bitset_iterator biter;
285 state_item_number prod;
286 BITSET_FOR_EACH (biter, copy, prod, 0)
287 bitset_set (state_items[prod].revs, j);
288 }
289 }
290 hash_free (closure_map);
291 }
292 }
293
294 /* Since lookaheads are only generated for reductions, we need to
295 propagate lookahead sets backwards as the searches require each
296 state_item to have a lookahead. */
297 static inline void
298 gen_lookaheads (void)
299 {
300 for (state_item_number i = 0; i < nstate_items; ++i)
301 {
302 state_item *si = &state_items[i];
303 if (item_number_is_symbol_number (*(si->item)) || !si->lookahead)
304 continue;
305
306 bitset lookahead = si->lookahead;
307 state_item_list queue =
308 gl_list_create (GL_LINKED_LIST, NULL, NULL, NULL, true, 1,
309 (const void **) &si);
310
311 // For each reduction item, traverse through all state_items
312 // accessible through reverse transition steps, and set their
313 // lookaheads to the reduction items lookahead
314 while (gl_list_size (queue) > 0)
315 {
316 state_item *prev = (state_item *) gl_list_get_at (queue, 0);
317 gl_list_remove_at (queue, 0);
318 prev->lookahead = lookahead;
319 if (SI_TRANSITION (prev))
320 {
321 bitset rsi = state_items[prev - state_items].revs;
322 bitset_iterator biter;
323 state_item_number sin;
324 BITSET_FOR_EACH (biter, rsi, sin, 0)
325 gl_list_add_first (queue, &state_items[sin]);
326 }
327 }
328 gl_list_free (queue);
329 }
330 }
331
332 bitsetv firsts = NULL;
333
334 static void
335 init_firsts (void)
336 {
337 firsts = bitsetv_create (nnterms, nsyms, BITSET_FIXED);
338 for (rule_number i = 0; i < nrules; ++i)
339 {
340 rule *r = &rules[i];
341 item_number *n = r->rhs;
342 // Iterate through nullable nonterminals to try to find a terminal.
343 while (item_number_is_symbol_number (*n) && ISVAR (*n)
344 && nullable[*n - ntokens])
345 ++n;
346 if (item_number_is_rule_number (*n) || ISVAR (*n))
347 continue;
348
349 symbol_number lhs = r->lhs->number;
350 bitset_set (FIRSTS (lhs), *n);
351 }
352 bool change = true;
353 while (change)
354 {
355 change = false;
356 for (rule_number i = 0; i < nrules; ++i)
357 {
358 rule *r = &rules[i];
359 symbol_number lhs = r->lhs->number;
360 bitset f_lhs = FIRSTS (lhs);
361 for (item_number *n = r->rhs;
362 item_number_is_symbol_number (*n) && ISVAR (*n);
363 ++n)
364 {
365 bitset f = FIRSTS (*n);
366 if (!bitset_subset_p (f_lhs, f))
367 {
368 change = true;
369 bitset_union (f_lhs, f_lhs, f);
370 }
371 if (!nullable[*n - ntokens])
372 break;
373 }
374 }
375 }
376 }
377
378 static inline void
379 disable_state_item (state_item *si)
380 {
381 si->trans = -2;
382 bitset_free (si->revs);
383 if (si->prods)
384 bitset_free (si->prods);
385 }
386
387 /* Disable all state_item paths that lead to/from SI and nowhere
388 else. */
389 static void
390 prune_state_item (const state_item *si)
391 {
392 state_item_list queue =
393 gl_list_create (GL_LINKED_LIST, NULL, NULL, NULL, true, 1,
394 (const void **) &si);
395
396 while (gl_list_size (queue) > 0)
397 {
398 state_item *dsi = (state_item *) gl_list_get_at (queue, 0);
399 gl_list_remove_at (queue, 0);
400 if (SI_DISABLED (dsi - state_items))
401 continue;
402
403 if (dsi->trans >= 0 && !SI_DISABLED (dsi->trans))
404 {
405 const state_item *trans = &state_items[dsi->trans];
406 bitset_reset (trans->revs, dsi - state_items);
407 if (bitset_empty_p (trans->revs))
408 gl_list_add_last (queue, trans);
409 }
410
411 if (dsi->prods)
412 {
413 bitset_iterator biter;
414 state_item_number sin;
415 BITSET_FOR_EACH (biter, dsi->prods, sin, 0)
416 {
417 if (SI_DISABLED (sin))
418 continue;
419 const state_item *prod = &state_items[sin];
420 bitset_reset (prod->revs, dsi - state_items);
421 if (bitset_empty_p (prod->revs))
422 gl_list_add_last (queue, prod);
423 }
424 }
425
426 bitset_iterator biter;
427 state_item_number sin;
428 BITSET_FOR_EACH (biter, dsi->revs, sin, 0)
429 {
430 if (SI_DISABLED (sin))
431 continue;
432 state_item *rev = &state_items[sin];
433 if (&state_items[rev->trans] == dsi)
434 gl_list_add_last (queue, rev);
435 else if (rev->prods)
436 {
437 bitset_reset (rev->prods, dsi - state_items);
438 if (bitset_empty_p (rev->prods))
439 gl_list_add_last (queue, rev);
440 }
441 else
442 gl_list_add_last (queue, rev);
443 }
444 disable_state_item (dsi);
445 }
446 gl_list_free (queue);
447 }
448
449 /* To make searches more efficient, prune away paths that are caused
450 by disabled transitions. */
451 static void
452 prune_disabled_paths (void)
453 {
454 for (int i = nstate_items - 1; i >= 0; --i)
455 {
456 state_item *si = &state_items[i];
457 if (si->trans == -1 && item_number_is_symbol_number (*si->item))
458 prune_state_item (si);
459 }
460 }
461
462 void
463 state_item_print (const state_item *si, FILE *out, const char *prefix)
464 {
465 fputs (prefix, out);
466 item_print (si->item, NULL, out);
467 putc ('\n', out);
468 }
469
470 const rule*
471 state_item_rule (const state_item *si)
472 {
473 return item_rule (si->item);
474 }
475
476 /**
477 * Report the state_item graph
478 */
479 static void
480 state_items_report (FILE *out)
481 {
482 fprintf (out, "# state items: %zu\n", nstate_items);
483 for (state_number i = 0; i < nstates; ++i)
484 {
485 fprintf (out, "State %d:\n", i);
486 for (state_item_number j = state_item_map[i]; j < state_item_map[i + 1]; ++j)
487 {
488 const state_item *si = &state_items[j];
489 item_print (si->item, NULL, out);
490 if (SI_DISABLED (j))
491 fputs (" DISABLED\n", out);
492 else
493 {
494 putc ('\n', out);
495 if (si->trans >= 0)
496 {
497 fputs (" -> ", out);
498 state_item_print (&state_items[si->trans], out, "");
499 }
500
501 bitset sets[2] = { si->prods, si->revs };
502 const char *txt[2] = { " => ", " <- " };
503 for (int seti = 0; seti < 2; ++seti)
504 {
505 bitset b = sets[seti];
506 if (b)
507 {
508 bitset_iterator biter;
509 state_item_number sin;
510 BITSET_FOR_EACH (biter, b, sin, 0)
511 {
512 fputs (txt[seti], out);
513 state_item_print (&state_items[sin], out, "");
514 }
515 }
516 }
517 }
518 putc ('\n', out);
519 }
520 }
521 fprintf (out, "FIRSTS\n");
522 for (symbol_number i = ntokens; i < nsyms; ++i)
523 {
524 fprintf (out, " %s firsts\n", symbols[i]->tag);
525 bitset_iterator iter;
526 symbol_number j;
527 BITSET_FOR_EACH (iter, FIRSTS (i), j, 0)
528 fprintf (out, " %s\n", symbols[j]->tag);
529 }
530 fputs ("\n\n", out);
531 }
532
533 void
534 state_items_init (void)
535 {
536 time_t start = time (NULL);
537 init_state_items ();
538 init_trans ();
539 init_prods ();
540 gen_lookaheads ();
541 init_firsts ();
542 prune_disabled_paths ();
543 if (trace_flag & trace_cex)
544 {
545 fprintf (stderr, "init: %f\n", difftime (time (NULL), start));
546 state_items_report (stderr);
547 }
548 }
549
550 void
551 state_items_free (void)
552 {
553 for (state_item_number i = 0; i < nstate_items; ++i)
554 if (!SI_DISABLED (i))
555 {
556 state_item *si = &state_items[i];
557 if (si->prods)
558 bitset_free (si->prods);
559 bitset_free (si->revs);
560 }
561 free (state_items);
562 bitsetv_free (firsts);
563 }
564
565 /**
566 * Determine, using precedence and associativity, whether the next
567 * production is allowed from the current production.
568 */
569 bool
570 production_allowed (const state_item *si, const state_item *next)
571 {
572 sym_content *s1 = item_rule (si->item)->lhs;
573 sym_content *s2 = item_rule (next->item)->lhs;
574 int prec1 = s1->prec;
575 int prec2 = s2->prec;
576 if (prec1 >= 0 && prec2 >= 0)
577 {
578 // Do not expand if lower precedence.
579 if (prec1 > prec2)
580 return false;
581 // Do not expand if same precedence, but left-associative.
582 if (prec1 == prec2 && s1->assoc == left_assoc)
583 return false;
584 }
585 return true;
586 }