1 /* Counterexample Generation Search Nodes
3 Copyright (C) 2020 Free Software Foundation, Inc.
5 This file is part of Bison, the GNU Compiler Compiler.
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.
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.
17 You should have received a copy of the GNU General Public License
18 along with this program. If not, see <http://www.gnu.org/licenses/>. */
22 #include "state-item.h"
25 #include <gl_linked_list.h>
35 state_item_number
*state_item_map
;
36 state_item
*state_items
;
38 // Hash functions for index -> bitset hash maps.
46 hash_pair_hasher (const hash_pair
*sl
, size_t max
)
52 hash_pair_comparator (const hash_pair
*l
, const hash_pair
*r
)
54 return l
->key
== r
->key
;
58 hash_pair_free (hash_pair
*hp
)
65 hash_pair_table_create (int size
)
67 return hash_xinitialize (size
,
69 (Hash_hasher
) hash_pair_hasher
,
70 (Hash_comparator
) hash_pair_comparator
,
71 (Hash_data_freer
) hash_pair_free
);
75 hash_pair_lookup (Hash_table
*tab
, int key
)
79 hash_pair
*hp
= hash_lookup (tab
, &probe
);
80 return hp
? hp
->l
: NULL
;
84 hash_pair_insert (Hash_table
*tab
, int key
, bitset val
)
86 hash_pair
*hp
= xmalloc (sizeof *hp
);
89 hash_pair
*res
= hash_xinsert (tab
, hp
);
90 // This must be the first insertion.
95 /* A state_item from a state's id and the offset of the item within
98 state_item_lookup (state_number s
, state_item_number off
)
100 return &state_items
[state_item_index_lookup (s
, off
)];
104 state_item_set (state_item_number sidx
, const state
*s
, item_number off
)
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
);
115 * Initialize state_items set
118 init_state_items (void)
121 bitsetv production_items
= bitsetv_create (nstates
, nritems
, BITSET_SPARSE
);
122 for (int i
= 0; i
< nstates
; ++i
)
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
)
129 && item_number_is_rule_number (ritem
[itemset
[j
] - 1]))
131 bitset_set (production_items
[i
], itemset
[j
]);
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
)
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
)
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
)
151 if (rule_search_idx
< red
->num
&& r
== red
->rules
[rule_search_idx
])
153 bitsetv lookahead
= red
->lookaheads
;
155 si
->lookahead
= lookahead
[rule_search_idx
];
159 bitset_iterator biter
;
161 BITSET_FOR_EACH (biter
, production_items
[i
], off
, 0)
163 state_item_set (sidx
, s
, off
);
164 if (item_number_is_rule_number (ritem
[off
]))
166 bitsetv lookahead
= red
->lookaheads
;
168 state_items
[sidx
].lookahead
= lookahead
[rule_search_idx
];
175 state_item_map
[nstates
] = nstate_items
;
176 bitsetv_free (production_items
);
180 state_sym_hasher (const void *st
, size_t max
)
182 return ((state
*) st
)->accessing_symbol
% max
;
186 state_sym_comparator (const void *s1
, const void *s2
)
188 return ((state
*) s1
)->accessing_symbol
== ((state
*) s2
)->accessing_symbol
;
192 state_sym_lookup (symbol_number sym
, Hash_table
*h
)
195 probe
.accessing_symbol
= sym
;
196 return hash_lookup (h
, &probe
);
202 for (state_number i
= 0; i
< nstates
; ++i
)
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
)
216 item_number
*item
= state_items
[j
].item
;
217 if (item_number_is_rule_number (*item
))
219 state
*dst
= state_sym_lookup (*item
, transition_set
);
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
])
227 state_item_number dstSI
=
228 state_item_index_lookup (dst
->number
, k
);
230 state_items
[j
].trans
= dstSI
;
231 bitset_set (state_items
[dstSI
].revs
, j
);
235 hash_free (transition_set
);
242 for (int i
= 0; i
< nstates
; ++i
)
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
);
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
)
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
);
260 itms
= bitset_create (nstate_items
, BITSET_SPARSE
);
261 hash_pair_insert (closure_map
, lhs
, itms
);
263 bitset_set (itms
, j
);
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
)
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
))
274 symbol_number sym
= item_number_as_symbol_number (item
);
275 bitset lb
= hash_pair_lookup (closure_map
, sym
);
278 bitset copy
= bitset_create (nstate_items
, BITSET_SPARSE
);
279 bitset_copy (copy
, lb
);
281 state_items
[j
].prods
= copy
;
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
);
290 hash_free (closure_map
);
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. */
298 gen_lookaheads (void)
300 for (state_item_number i
= 0; i
< nstate_items
; ++i
)
302 state_item
*si
= &state_items
[i
];
303 if (item_number_is_symbol_number (*(si
->item
)) || !si
->lookahead
)
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
);
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)
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
))
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
]);
328 gl_list_free (queue
);
332 bitsetv firsts
= NULL
;
337 firsts
= bitsetv_create (nnterms
, nsyms
, BITSET_FIXED
);
338 for (rule_number i
= 0; i
< nrules
; ++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
])
346 if (item_number_is_rule_number (*n
) || ISVAR (*n
))
349 symbol_number lhs
= r
->lhs
->number
;
350 bitset_set (FIRSTS (lhs
), *n
);
356 for (rule_number i
= 0; i
< nrules
; ++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
);
365 bitset f
= FIRSTS (*n
);
366 if (!bitset_subset_p (f_lhs
, f
))
369 bitset_union (f_lhs
, f_lhs
, f
);
371 if (!nullable
[*n
- ntokens
])
379 disable_state_item (state_item
*si
)
382 bitset_free (si
->revs
);
384 bitset_free (si
->prods
);
387 /* disable all transitions and productions that can only be
388 * reached through this state_item.
391 prune_forward (const state_item
*si
)
393 state_item_list queue
=
394 gl_list_create (GL_LINKED_LIST
, NULL
, NULL
, NULL
, true, 1,
395 (const void **) &si
);
397 while (gl_list_size (queue
) > 0)
399 state_item
*dsi
= (state_item
*) gl_list_get_at (queue
, 0);
400 gl_list_remove_at (queue
, 0);
402 gl_list_add_last (queue
, &state_items
[dsi
->trans
]);
406 bitset_iterator biter
;
407 state_item_number sin
;
408 BITSET_FOR_EACH (biter
, dsi
->prods
, sin
, 0)
410 const state_item
*prod
= &state_items
[sin
];
411 bitset_reset (prod
->revs
, dsi
- state_items
);
412 if (bitset_empty_p (prod
->revs
))
413 gl_list_add_last (queue
, prod
);
417 disable_state_item (dsi
);
419 gl_list_free (queue
);
422 /* disable all state_item paths that lead to
423 * si and nowhere else.
426 prune_backward (const state_item
*si
)
428 state_item_list queue
=
429 gl_list_create (GL_LINKED_LIST
, NULL
, NULL
, NULL
, true, 1,
430 (const void **) &si
);
432 while (gl_list_size (queue
) > 0)
434 state_item
*dsi
= (state_item
*) gl_list_get_at (queue
, 0);
435 gl_list_remove_at (queue
, 0);
436 bitset_iterator biter
;
437 state_item_number sin
;
438 BITSET_FOR_EACH (biter
, dsi
->revs
, sin
, 0)
440 if (SI_DISABLED (sin
))
442 state_item
*rev
= &state_items
[sin
];
445 bitset_reset (rev
->prods
, dsi
- state_items
);
446 if (bitset_empty_p (rev
->prods
))
447 gl_list_add_last (queue
, rev
);
450 gl_list_add_last (queue
, rev
);
453 disable_state_item (dsi
);
455 gl_list_free (queue
);
459 To make searches more efficient, we can prune away paths that are
460 caused by disabled transitions.
463 prune_disabled_paths (void)
465 for (int i
= nstate_items
- 1; i
>= 0; --i
)
467 state_item
*si
= &state_items
[i
];
468 if (si
->trans
== -1 && item_number_is_symbol_number (*si
->item
))
472 disable_state_item (si
);
478 state_item_print (const state_item
*si
, FILE *out
, const char *prefix
)
481 item_print (si
->item
, NULL
, out
);
486 * Report the state_item graph
489 state_items_report (FILE *out
)
491 fprintf (out
, "# state items: %zu\n", nstate_items
);
492 for (state_number i
= 0; i
< nstates
; ++i
)
494 fprintf (out
, "State %d:\n", i
);
495 for (state_item_number j
= state_item_map
[i
]; j
< state_item_map
[i
+ 1]; ++j
)
497 state_item
*si
= &state_items
[j
];
498 item_print (si
->item
, NULL
, out
);
501 item_print (si
->item
, NULL
, out
);
502 fputs (" DISABLED", out
);
508 state_item_print (&state_items
[si
->trans
], out
, "");
511 bitset sets
[2] = { si
->prods
, si
->revs
};
512 const char *txt
[2] = { " => ", " <- " };
513 for (int seti
= 0; seti
< 2; ++seti
)
515 bitset b
= sets
[seti
];
518 bitset_iterator biter
;
519 state_item_number sin
;
520 BITSET_FOR_EACH (biter
, b
, sin
, 0)
522 fputs (txt
[seti
], out
);
523 state_item_print (&state_items
[sin
], out
, "");
529 fprintf (out
, "FIRSTS\n");
530 for (symbol_number i
= ntokens
; i
< nsyms
; ++i
)
532 fprintf (out
, " %s firsts\n", symbols
[i
]->tag
);
533 bitset_iterator iter
;
535 BITSET_FOR_EACH (iter
, FIRSTS (i
), j
, 0)
536 fprintf (out
, " %s\n", symbols
[j
]->tag
);
542 state_items_init (void)
544 time_t start
= time (NULL
);
550 prune_disabled_paths ();
551 if (trace_flag
& trace_cex
)
553 fprintf (stderr
, "init: %f\n", difftime (time (NULL
), start
));
554 state_items_report (stderr
);
559 state_items_free (void)
561 for (state_item_number i
= 0; i
< nstate_items
; ++i
)
562 if (!SI_DISABLED (i
))
564 state_item
*si
= &state_items
[i
];
566 bitset_free (si
->prods
);
567 bitset_free (si
->revs
);
570 bitsetv_free (firsts
);
574 * Determine, using precedence and associativity, whether the next
575 * production is allowed from the current production.
578 production_allowed (const state_item
*si
, const state_item
*next
)
580 sym_content
*s1
= item_rule (si
->item
)->lhs
;
581 sym_content
*s2
= item_rule (next
->item
)->lhs
;
582 int prec1
= s1
->prec
;
583 int prec2
= s2
->prec
;
584 if (prec1
>= 0 && prec2
>= 0)
586 // Do not expand if lower precedence.
589 // Do not expand if same precedence, but left-associative.
590 if (prec1
== prec2
&& s1
->assoc
== left_assoc
)