1 /* Conflict counterexample generation
3 Copyright (C) 2020-2021 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 <https://www.gnu.org/licenses/>. */
22 #include "counterexample.h"
27 #include <gl_linked_list.h>
28 #include <gl_rbtreehash_list.h>
32 #include <textstyle.h>
37 #include "derivation.h"
43 #include "parse-simulation.h"
46 #define TIME_LIMIT_ENFORCED true
47 /** If set to false, only consider the states on the shortest
48 * lookahead-sensitive path when constructing a unifying counterexample. */
49 #define EXTENDED_SEARCH false
51 /* costs for making various steps in a search */
52 #define PRODUCTION_COST 50
55 #define UNSHIFT_COST 1
56 #define EXTENDED_COST 10000
58 /** The time limit before printing an assurance message to the user to
59 * indicate that the search is still running. */
60 #define ASSURANCE_LIMIT 2.0f
62 /* The time limit before giving up looking for unifying counterexample. */
63 static float time_limit
= 5.0f
;
65 #define CUMULATIVE_TIME_LIMIT 120.0f
67 // This is the fastest way to get the tail node from the gl_list API.
69 list_get_end (gl_list_t list
)
71 gl_list_node_t sentinel
= gl_list_add_last (list
, NULL
);
72 gl_list_node_t res
= gl_list_previous_node (list
, sentinel
);
73 gl_list_remove_node (list
, sentinel
);
86 static counterexample
*
87 new_counterexample (derivation
*d1
, derivation
*d2
,
91 counterexample
*res
= xmalloc (sizeof *res
);
92 res
->shift_reduce
= shift_reduce
;
95 // Display the shift first.
110 free_counterexample (counterexample
*cex
)
112 derivation_free (cex
->d1
);
113 derivation_free (cex
->d2
);
118 counterexample_print (const counterexample
*cex
, FILE *out
, const char *prefix
)
120 const bool flat
= getenv ("YYFLAT");
121 const char *example1_label
122 = cex
->unifying
? _("Example") : _("First example");
123 const char *example2_label
124 = cex
->unifying
? _("Example") : _("Second example");
125 const char *deriv1_label
126 = cex
->shift_reduce
? _("Shift derivation") : _("First reduce derivation");
127 const char *deriv2_label
128 = cex
->shift_reduce
? _("Reduce derivation") : _("Second reduce derivation");
130 max_int (max_int (mbswidth (example1_label
, 0), mbswidth (example2_label
, 0)),
131 max_int (mbswidth (deriv1_label
, 0), mbswidth (deriv2_label
, 0)));
133 fprintf (out
, " %s%s%*s ", prefix
,
134 example1_label
, width
- mbswidth (example1_label
, 0), "");
136 fprintf (out
, " %s%s: ", prefix
, example1_label
);
137 derivation_print_leaves (cex
->d1
, out
);
139 fprintf (out
, " %s%s%*s ", prefix
,
140 deriv1_label
, width
- mbswidth (deriv1_label
, 0), "");
142 fprintf (out
, " %s%s", prefix
, deriv1_label
);
143 derivation_print (cex
->d1
, out
, prefix
);
145 // If we output to the terminal (via stderr) and we have color
146 // support, display unifying examples a second time, as color allows
147 // to see the differences.
148 if (!cex
->unifying
|| is_styled (stderr
))
151 fprintf (out
, " %s%s%*s ", prefix
,
152 example2_label
, width
- mbswidth (example2_label
, 0), "");
154 fprintf (out
, " %s%s: ", prefix
, example2_label
);
155 derivation_print_leaves (cex
->d2
, out
);
158 fprintf (out
, " %s%s%*s ", prefix
,
159 deriv2_label
, width
- mbswidth (deriv2_label
, 0), "");
161 fprintf (out
, " %s%s", prefix
, deriv2_label
);
162 derivation_print (cex
->d2
, out
, prefix
);
170 * NON UNIFYING COUNTER EXAMPLES
174 // Search node for BFS on state items
176 typedef struct si_bfs_node
178 state_item_number si
;
179 struct si_bfs_node
*parent
;
184 si_bfs_new (state_item_number si
, si_bfs_node
*parent
)
186 si_bfs_node
*res
= xcalloc (1, sizeof *res
);
188 res
->parent
= parent
;
189 res
->reference_count
= 1;
191 ++parent
->reference_count
;
196 si_bfs_contains (const si_bfs_node
*n
, state_item_number sin
)
198 for (const si_bfs_node
*search
= n
; search
!= NULL
; search
= search
->parent
)
199 if (search
->si
== sin
)
205 si_bfs_free (si_bfs_node
*n
)
209 --n
->reference_count
;
210 if (n
->reference_count
== 0)
212 si_bfs_free (n
->parent
);
217 typedef gl_list_t si_bfs_node_list
;
220 * start is a state_item such that conflict_sym is an element of FIRSTS of the
221 * nonterminal after the dot in start. Because of this, we should be able to
222 * find a production item starting with conflict_sym by only searching productions
223 * of the nonterminal and shifting over nullable nonterminals
225 * this returns the derivation of the productions that lead to conflict_sym
227 static inline derivation_list
228 expand_to_conflict (state_item_number start
, symbol_number conflict_sym
)
230 si_bfs_node
*init
= si_bfs_new (start
, NULL
);
232 si_bfs_node_list queue
233 = gl_list_create (GL_LINKED_LIST
, NULL
, NULL
,
234 (gl_listelement_dispose_fn
) si_bfs_free
,
235 true, 1, (const void **) &init
);
236 si_bfs_node
*node
= NULL
;
237 // breadth-first search for a path of productions to the conflict symbol
238 while (gl_list_size (queue
) > 0)
240 node
= (si_bfs_node
*) gl_list_get_at (queue
, 0);
241 state_item
*silast
= &state_items
[node
->si
];
242 symbol_number sym
= item_number_as_symbol_number (*silast
->item
);
243 if (sym
== conflict_sym
)
247 // add each production to the search
248 bitset_iterator biter
;
249 state_item_number sin
;
250 bitset sib
= silast
->prods
;
251 BITSET_FOR_EACH (biter
, sib
, sin
, 0)
253 // ignore productions already in the path
254 if (si_bfs_contains (node
, sin
))
256 si_bfs_node
*next
= si_bfs_new (sin
, node
);
257 gl_list_add_last (queue
, next
);
259 // for nullable nonterminals, add its goto to the search
260 if (nullable
[sym
- ntokens
])
262 si_bfs_node
*next
= si_bfs_new (silast
->trans
, node
);
263 gl_list_add_last (queue
, next
);
266 gl_list_remove_at (queue
, 0);
268 if (gl_list_size (queue
) == 0)
270 gl_list_free (queue
);
271 fputs ("Error expanding derivation\n", stderr
);
275 derivation
*dinit
= derivation_new_leaf (conflict_sym
);
276 derivation_list result
= derivation_list_new ();
277 derivation_list_append (result
, dinit
);
278 // iterate backwards through the generated path to create a derivation
279 // of the conflict symbol containing derivations of each production step.
281 for (si_bfs_node
*n
= node
; n
!= NULL
; n
= n
->parent
)
283 state_item
*si
= &state_items
[n
->si
];
284 item_number
*pos
= si
->item
;
285 if (SI_PRODUCTION (si
))
287 item_number
*i
= NULL
;
288 for (i
= pos
+ 1; !item_number_is_rule_number (*i
); ++i
)
289 derivation_list_append (result
, derivation_new_leaf (*i
));
291 rules
[item_number_as_rule_number (*i
)].lhs
->number
;
292 derivation
*deriv
= derivation_new (lhs
, result
);
293 result
= derivation_list_new ();
294 derivation_list_append (result
, deriv
);
298 symbol_number sym
= item_number_as_symbol_number (*(pos
- 1));
299 derivation
*deriv
= derivation_new_leaf (sym
);
300 derivation_list_prepend (result
, deriv
);
303 gl_list_free (queue
);
304 derivation_free ((derivation
*)gl_list_get_at (result
, 0));
305 gl_list_remove_at (result
, 0);
310 * Complete derivations for any pending productions in the given
311 * sequence of state-items. For example, the input could be a path
312 * of states that would give us the following input:
313 * Stmt ::= [lval ::= [VAR] '=' e ::=[ e::=['0'] '+' •
314 * So to complete the derivation of Stmt, we need an output like:
315 * Stmt ::= [lval ::= [VAR] '=' e ::=[ e::=['0'] '+' • e ] ';' ]
318 complete_diverging_example (symbol_number conflict_sym
,
319 state_item_list path
, derivation_list derivs
)
321 // The idea is to transfer each pending symbol on the productions
322 // associated with the given StateItems to the resulting derivation.
323 derivation_list result
= derivation_list_new ();
324 bool lookahead_required
= false;
327 derivs
= derivation_list_new ();
328 gl_list_add_last (result
, derivation_dot ());
329 lookahead_required
= true;
332 gl_list_node_t deriv
= list_get_end (derivs
);
334 // We go backwards through the path to create the derivation tree bottom-up.
335 // Effectively this loops through each production once, and generates a
336 // derivation of the left hand side by appending all of the rhs symbols.
337 // this becomes the derivation of the nonterminal after the dot in the
338 // next production, and all of the other symbols of the rule are added as normal.
339 for (gl_list_node_t state_node
= list_get_end (path
);
341 state_node
= gl_list_previous_node (path
, state_node
))
343 state_item
*si
= (state_item
*) gl_list_node_value (path
, state_node
);
344 item_number
*item
= si
->item
;
345 item_number pos
= *item
;
347 if (gl_list_size (result
) == 1 && !item_number_is_rule_number (pos
)
348 && gl_list_get_at (result
, 0) == derivation_dot ())
350 derivation_list_append (result
,
351 derivation_new_leaf (item_number_as_symbol_number (pos
)));
352 lookahead_required
= false;
354 item_number
*i
= item
;
355 // go through each symbol after the dot in the current rule, and
356 // add each symbol to its derivation.
357 for (state_item_number nsi
= si
- state_items
;
358 !item_number_is_rule_number (*i
);
359 ++i
, nsi
= state_items
[nsi
].trans
)
361 // if the item is a reduction, we could skip to the wrong rule
362 // by starting at i + 1, so this continue is necessary
365 symbol_number sym
= item_number_as_symbol_number (*i
);
366 if (!lookahead_required
|| sym
== conflict_sym
)
368 derivation_list_append (result
, derivation_new_leaf (sym
));
369 lookahead_required
= false;
372 // Since PATH is a path to the conflict state-item,
373 // for a reduce conflict item, we will want to have a derivation
374 // that shows the conflict symbol from its lookahead set being used.
376 // Since reductions have the dot at the end of the item,
377 // this loop will be first executed on the last item in the path
378 // that's not a reduction. When that happens,
379 // the symbol after the dot should be a nonterminal,
380 // and we can look through successive nullable nonterminals
381 // for one with the conflict symbol in its first set.
382 if (bitset_test (FIRSTS (sym
), conflict_sym
))
384 lookahead_required
= false;
385 derivation_list next_derivs
=
386 expand_to_conflict (nsi
, conflict_sym
);
387 derivation
*d
= NULL
;
388 for (gl_list_iterator_t it
= gl_list_iterator (next_derivs
);
389 derivation_list_next (&it
, &d
);)
390 derivation_list_append (result
, d
);
391 i
+= gl_list_size (next_derivs
) - 1;
392 derivation_list_free (next_derivs
);
394 else if (nullable
[sym
- ntokens
])
396 derivation
*d
= derivation_new_leaf (sym
);
397 derivation_list_append (result
, d
);
401 // We found a path to the conflict item, and despite it
402 // having the conflict symbol in its lookahead, no example
403 // containing the symbol after the conflict item
405 derivation_list_append (result
, derivation_new_leaf (1));
406 lookahead_required
= false;
409 const rule
*r
= &rules
[item_number_as_rule_number (*i
)];
410 // add derivations for symbols before dot
411 for (i
= item
- 1; !item_number_is_rule_number (*i
) && i
>= ritem
; i
--)
413 gl_list_node_t p
= gl_list_previous_node (path
, state_node
);
418 const void *tmp_deriv
= gl_list_node_value (derivs
, deriv
);
419 deriv
= gl_list_previous_node (derivs
, deriv
);
420 derivation_list_prepend (result
, (derivation
*)tmp_deriv
);
423 derivation_list_prepend (result
, derivation_new_leaf (*i
));
425 // completing the derivation
426 derivation
*new_deriv
= derivation_new (r
->lhs
->number
, result
);
427 result
= derivation_list_new ();
428 derivation_list_append (result
, new_deriv
);
430 derivation
*res
= (derivation
*) gl_list_get_at (result
, 0);
431 derivation_retain (res
);
432 derivation_list_free (result
);
433 derivation_list_free (derivs
);
437 /* Iterate backwards through the shifts of the path in the reduce
438 conflict, and find a path of shifts from the shift conflict that
439 goes through the same states. */
440 static state_item_list
441 nonunifying_shift_path (state_item_list reduce_path
, state_item
*shift_conflict
)
443 gl_list_node_t tmp
= gl_list_add_last (reduce_path
, NULL
);
444 gl_list_node_t next_node
= gl_list_previous_node (reduce_path
, tmp
);
445 gl_list_node_t node
= gl_list_previous_node (reduce_path
, next_node
);
446 gl_list_remove_node (reduce_path
, tmp
);
447 state_item
*si
= shift_conflict
;
448 state_item_list result
=
449 gl_list_create_empty (GL_LINKED_LIST
, NULL
, NULL
, NULL
, true);
450 // FIXME: bool paths_merged;
451 for (; node
!= NULL
; next_node
= node
,
452 node
= gl_list_previous_node (reduce_path
, node
))
455 (state_item
*) gl_list_node_value (reduce_path
, node
);
456 state_item
*nextrefsi
=
457 (state_item
*) gl_list_node_value (reduce_path
, next_node
);
460 gl_list_add_first (result
, refsi
);
464 // skip reduction items
465 if (nextrefsi
->item
!= refsi
->item
+ 1 && refsi
->item
!= ritem
)
468 // bfs to find a shift to the right state
469 si_bfs_node
*init
= si_bfs_new (si
- state_items
, NULL
);
470 si_bfs_node_list queue
471 = gl_list_create (GL_LINKED_LIST
, NULL
, NULL
,
472 (gl_listelement_dispose_fn
) si_bfs_free
,
473 true, 1, (const void **) &init
);
474 si_bfs_node
*sis
= NULL
;
475 state_item
*prevsi
= NULL
;
476 while (gl_list_size (queue
) > 0)
478 sis
= (si_bfs_node
*) gl_list_get_at (queue
, 0);
479 // if we end up in the start state, the shift couldn't be found.
483 state_item
*search_si
= &state_items
[sis
->si
];
484 // if the current state-item is a production item,
485 // its reverse production items get added to the queue.
486 // Otherwise, look for a reverse transition to the target state.
487 bitset rsi
= search_si
->revs
;
488 bitset_iterator biter
;
489 state_item_number sin
;
490 BITSET_FOR_EACH (biter
, rsi
, sin
, 0)
492 prevsi
= &state_items
[sin
];
493 if (SI_TRANSITION (search_si
))
495 if (prevsi
->state
== refsi
->state
)
498 else if (!si_bfs_contains (sis
, sin
))
500 si_bfs_node
*prevsis
= si_bfs_new (sin
, sis
);
501 gl_list_add_last (queue
, prevsis
);
504 gl_list_remove_at (queue
, 0);
507 // prepend path to shift we found
510 gl_list_node_t ln
= gl_list_add_first (result
, &state_items
[sis
->si
]);
511 for (si_bfs_node
*n
= sis
->parent
; n
; n
= n
->parent
)
512 ln
= gl_list_add_after (result
, ln
, &state_items
[n
->si
]);
516 gl_list_free (queue
);
518 if (trace_flag
& trace_cex
)
520 fputs ("SHIFT ITEM PATH:\n", stderr
);
521 state_item
*sip
= NULL
;
522 for (gl_list_iterator_t it
= gl_list_iterator (result
);
523 state_item_list_next (&it
, &sip
);
525 state_item_print (sip
, stderr
, "");
532 * Construct a nonunifying counterexample from the shortest
533 * lookahead-sensitive path.
535 static counterexample
*
536 example_from_path (bool shift_reduce
,
537 state_item_number itm2
,
538 state_item_list shortest_path
, symbol_number next_sym
)
541 complete_diverging_example (next_sym
, shortest_path
, NULL
);
542 state_item_list path_2
544 ? nonunifying_shift_path (shortest_path
, &state_items
[itm2
])
545 : shortest_path_from_start (itm2
, next_sym
);
546 derivation
*deriv2
= complete_diverging_example (next_sym
, path_2
, NULL
);
547 gl_list_free (path_2
);
548 return new_counterexample (deriv1
, deriv2
, shift_reduce
, false, true);
553 * UNIFYING COUNTER EXAMPLES
557 /* A search state keeps track of two parser simulations,
558 * one starting at each conflict. Complexity is a metric
559 * which sums different parser actions with varying weights.
563 parse_state
*states
[2];
567 static search_state
*
568 initial_search_state (state_item
*conflict1
, state_item
*conflict2
)
570 search_state
*res
= xmalloc (sizeof *res
);
571 res
->states
[0] = new_parse_state (conflict1
);
572 res
->states
[1] = new_parse_state (conflict2
);
573 parse_state_retain (res
->states
[0]);
574 parse_state_retain (res
->states
[1]);
579 static search_state
*
580 new_search_state (parse_state
*ps1
, parse_state
*ps2
, int complexity
)
582 search_state
*res
= xmalloc (sizeof *res
);
583 res
->states
[0] = ps1
;
584 res
->states
[1] = ps2
;
585 parse_state_retain (res
->states
[0]);
586 parse_state_retain (res
->states
[1]);
587 res
->complexity
= complexity
;
591 static search_state
*
592 copy_search_state (search_state
*parent
)
594 search_state
*res
= xmalloc (sizeof *res
);
596 parse_state_retain (res
->states
[0]);
597 parse_state_retain (res
->states
[1]);
602 search_state_free_children (search_state
*ss
)
604 free_parse_state (ss
->states
[0]);
605 free_parse_state (ss
->states
[1]);
609 search_state_free (search_state
*ss
)
613 search_state_free_children (ss
);
617 /* For debugging traces. */
619 search_state_print (search_state
*ss
)
621 fputs ("CONFLICT 1 ", stderr
);
622 print_parse_state (ss
->states
[0]);
623 fputs ("CONFLICT 2 ", stderr
);
624 print_parse_state (ss
->states
[1]);
628 typedef gl_list_t search_state_list
;
631 search_state_list_next (gl_list_iterator_t
*it
, search_state
**ss
)
633 const void *p
= NULL
;
634 bool res
= gl_list_iterator_next (it
, &p
, NULL
);
636 *ss
= (search_state
*) p
;
638 gl_list_iterator_free (it
);
643 * When a search state is copied, this is used to
644 * directly set one of the parse states
647 ss_set_parse_state (search_state
*ss
, int idx
, parse_state
*ps
)
649 free_parse_state (ss
->states
[idx
]);
650 ss
->states
[idx
] = ps
;
651 parse_state_retain (ps
);
655 * Construct a nonunifying example from a search state
656 * which has its parse states unified at the beginning
657 * but not the end of the example.
659 static counterexample
*
660 complete_diverging_examples (search_state
*ss
,
661 symbol_number next_sym
,
664 derivation
*new_derivs
[2];
665 for (int i
= 0; i
< 2; ++i
)
667 state_item_list sitems
;
668 derivation_list derivs
;
669 parse_state_lists (ss
->states
[i
], &sitems
, &derivs
);
670 new_derivs
[i
] = complete_diverging_example (next_sym
, sitems
, derivs
);
671 gl_list_free (sitems
);
673 return new_counterexample (new_derivs
[0], new_derivs
[1],
674 shift_reduce
, false, true);
678 * Search states are stored in bundles with those that
679 * share the same complexity. This is so the priority
680 * queue takes less overhead.
684 search_state_list states
;
686 } search_state_bundle
;
689 ssb_free (search_state_bundle
*ssb
)
691 gl_list_free (ssb
->states
);
696 ssb_hasher (search_state_bundle
*ssb
)
698 return ssb
->complexity
;
702 ssb_comp (const search_state_bundle
*s1
, const search_state_bundle
*s2
)
704 return s1
->complexity
- s2
->complexity
;
708 ssb_equals (const search_state_bundle
*s1
, const search_state_bundle
*s2
)
710 return s1
->complexity
== s2
->complexity
;
713 typedef gl_list_t ssb_list
;
716 visited_hasher (const search_state
*ss
, size_t max
)
718 return (parse_state_hasher (ss
->states
[0], max
)
719 + parse_state_hasher (ss
->states
[1], max
)) % max
;
723 visited_comparator (const search_state
*ss1
, const search_state
*ss2
)
725 return parse_state_comparator (ss1
->states
[0], ss2
->states
[0])
726 && parse_state_comparator (ss1
->states
[1], ss2
->states
[1]);
729 /* Priority queue for search states with minimal complexity. */
730 static ssb_list ssb_queue
;
731 static Hash_table
*visited
;
732 /* The set of parser states on the shortest lookahead-sensitive path. */
733 static bitset scp_set
= NULL
;
734 /* The set of parser states used for the conflict reduction rule. */
735 static bitset rpp_set
= NULL
;
738 ssb_append (search_state
*ss
)
740 if (hash_lookup (visited
, ss
))
742 search_state_free (ss
);
745 hash_xinsert (visited
, ss
);
746 // if states are only referenced by the visited set,
747 // their contents should be freed as we only need
748 // the metadata necessary to compute a hash.
749 parse_state_free_contents_early (ss
->states
[0]);
750 parse_state_free_contents_early (ss
->states
[1]);
751 parse_state_retain (ss
->states
[0]);
752 parse_state_retain (ss
->states
[1]);
753 search_state_bundle
*ssb
= xmalloc (sizeof *ssb
);
754 ssb
->complexity
= ss
->complexity
;
755 gl_list_node_t n
= gl_list_search (ssb_queue
, ssb
);
759 gl_list_create_empty (GL_LINKED_LIST
, NULL
, NULL
,
760 (gl_listelement_dispose_fn
)search_state_free_children
,
762 gl_sortedlist_add (ssb_queue
, (gl_listelement_compar_fn
) ssb_comp
, ssb
);
767 ssb
= (search_state_bundle
*) gl_list_node_value (ssb_queue
, n
);
769 gl_list_add_last (ssb
->states
, ss
);
773 * The following functions perform various actions on parse states
774 * and assign complexities to the newly generated search states.
777 production_step (search_state
*ss
, int parser_state
)
779 const state_item
*other_si
= parse_state_tail (ss
->states
[1 - parser_state
]);
780 symbol_number other_sym
= item_number_as_symbol_number (*other_si
->item
);
781 parse_state_list prods
=
782 simulate_production (ss
->states
[parser_state
], other_sym
);
783 int complexity
= ss
->complexity
+ PRODUCTION_COST
;
785 parse_state
*ps
= NULL
;
786 for (gl_list_iterator_t it
= gl_list_iterator (prods
);
787 parse_state_list_next (&it
, &ps
);
790 search_state
*copy
= copy_search_state (ss
);
791 ss_set_parse_state (copy
, parser_state
, ps
);
792 copy
->complexity
= complexity
;
795 gl_list_free (prods
);
799 reduction_cost (const parse_state
*ps
)
803 parse_state_completed_steps (ps
, &shifts
, &productions
);
804 return SHIFT_COST
* shifts
+ PRODUCTION_COST
* productions
;
807 static search_state_list
808 reduction_step (search_state
*ss
, const item_number
*conflict_item
,
809 int parser_state
, int rule_len
)
811 (void) conflict_item
; // FIXME: Unused
812 search_state_list result
=
813 gl_list_create_empty (GL_LINKED_LIST
, NULL
, NULL
, NULL
, 1);
815 parse_state
*ps
= ss
->states
[parser_state
];
816 const state_item
*si
= parse_state_tail (ps
);
817 bitset symbol_set
= si
->lookahead
;
818 parse_state
*other
= ss
->states
[1 - parser_state
];
819 const state_item
*other_si
= parse_state_tail (other
);
820 // if the other state can transition on a symbol,
821 // the reduction needs to have that symbol in its lookahead
822 if (item_number_is_symbol_number (*other_si
->item
))
824 symbol_number other_sym
=
825 item_number_as_symbol_number (*other_si
->item
);
826 if (!intersect_symbol (other_sym
, symbol_set
))
828 symbol_set
= bitset_create (nsyms
, BITSET_FIXED
);
829 bitset_set (symbol_set
, other_sym
);
832 // FIXME: search_state *new_root = copy_search_state (ss);
833 parse_state_list reduced
=
834 simulate_reduction (ps
, rule_len
, symbol_set
);
835 parse_state
*reduced_ps
= NULL
;
836 for (gl_list_iterator_t it
= gl_list_iterator (reduced
);
837 parse_state_list_next (&it
, &reduced_ps
);
840 search_state
*copy
= copy_search_state (ss
);
841 ss_set_parse_state (copy
, parser_state
, reduced_ps
);
842 int r_cost
= reduction_cost (reduced_ps
);
843 copy
->complexity
+= r_cost
+ PRODUCTION_COST
+ 2 * SHIFT_COST
;
844 gl_list_add_last (result
, copy
);
846 gl_list_free (reduced
);
847 if (symbol_set
!= si
->lookahead
)
848 bitset_free (symbol_set
);
853 * Attempt to prepend the given symbol to this search state, respecting
854 * the given subsequent next symbol on each path. If a reverse transition
855 * cannot be made on both states, possible reverse productions are prepended
858 search_state_prepend (search_state
*ss
, symbol_number sym
, bitset guide
)
860 (void) sym
; // FIXME: Unused.
861 const state_item
*si1src
= parse_state_head (ss
->states
[0]);
862 const state_item
*si2src
= parse_state_head (ss
->states
[1]);
864 bool prod1
= SI_PRODUCTION (si1src
);
865 // If one can make a reverse transition and the other can't, only apply
866 // the reverse productions that the other state can make in an attempt to
868 if (prod1
!= SI_PRODUCTION (si2src
))
870 int prod_state
= prod1
? 0 : 1;
871 parse_state_list prev
= parser_prepend (ss
->states
[prod_state
]);
872 parse_state
*ps
= NULL
;
873 for (gl_list_iterator_t iter
= gl_list_iterator (prev
);
874 parse_state_list_next (&iter
, &ps
);
877 const state_item
*psi
= parse_state_head (ps
);
878 bool guided
= bitset_test (guide
, psi
->state
->number
);
879 if (!guided
&& !EXTENDED_SEARCH
)
882 search_state
*copy
= copy_search_state (ss
);
883 ss_set_parse_state (copy
, prod_state
, ps
);
884 copy
->complexity
+= PRODUCTION_COST
;
886 copy
->complexity
+= EXTENDED_COST
;
892 // The parse state heads are either both production items or both
893 // transition items. So all prepend options will either be
894 // reverse transitions or reverse productions
895 int complexity_cost
= prod1
? PRODUCTION_COST
: UNSHIFT_COST
;
896 complexity_cost
*= 2;
898 parse_state_list prev1
= parser_prepend (ss
->states
[0]);
899 parse_state_list prev2
= parser_prepend (ss
->states
[1]);
901 // loop through each pair of possible prepend states and append search
902 // states for each pair where the parser states correspond to the same
904 parse_state
*ps1
= NULL
;
905 for (gl_list_iterator_t iter1
= gl_list_iterator (prev1
);
906 parse_state_list_next (&iter1
, &ps1
);
909 const state_item
*psi1
= parse_state_head (ps1
);
910 bool guided1
= bitset_test (guide
, psi1
->state
->number
);
911 if (!guided1
&& !EXTENDED_SEARCH
)
914 parse_state
*ps2
= NULL
;
915 for (gl_list_iterator_t iter2
= gl_list_iterator (prev2
);
916 parse_state_list_next (&iter2
, &ps2
);
919 const state_item
*psi2
= parse_state_head (ps2
);
921 bool guided2
= bitset_test (guide
, psi2
->state
->number
);
922 if (!guided2
&& !EXTENDED_SEARCH
)
924 // Only consider prepend state items that share the same state.
925 if (psi1
->state
!= psi2
->state
)
928 int complexity
= ss
->complexity
;
930 complexity
+= PRODUCTION_COST
* 2;
932 complexity
+= UNSHIFT_COST
* 2;
933 // penalty for not being along the guide path
934 if (!guided1
|| !guided2
)
935 complexity
+= EXTENDED_COST
;
936 ssb_append (new_search_state (ps1
, ps2
, complexity
));
939 gl_list_free (prev1
);
940 gl_list_free (prev2
);
944 * Determine if the productions associated with the given parser items have
945 * the same prefix up to the dot.
948 have_common_prefix (const item_number
*itm1
, const item_number
*itm2
)
951 for (; !item_number_is_rule_number (itm1
[i
]); ++i
)
952 if (itm1
[i
] != itm2
[i
])
954 return item_number_is_rule_number (itm2
[i
]);
958 * The start and end locations of an item in ritem.
960 static const item_number
*
961 item_rule_start (const item_number
*item
)
963 const item_number
*res
= NULL
;
965 ritem
< res
&& item_number_is_symbol_number (*(res
- 1));
971 static const item_number
*
972 item_rule_end (const item_number
*item
)
974 const item_number
*res
= NULL
;
975 for (res
= item
; item_number_is_symbol_number (*res
); ++res
)
981 * Perform the appropriate possible parser actions
982 * on a search state and add the results to the
983 * search state priority queue.
986 generate_next_states (search_state
*ss
, state_item
*conflict1
,
987 state_item
*conflict2
)
989 // Compute the successor configurations.
990 parse_state
*ps1
= ss
->states
[0];
991 parse_state
*ps2
= ss
->states
[1];
992 const state_item
*si1
= parse_state_tail (ps1
);
993 const state_item
*si2
= parse_state_tail (ps2
);
994 bool si1reduce
= item_number_is_rule_number (*si1
->item
);
995 bool si2reduce
= item_number_is_rule_number (*si2
->item
);
996 if (!si1reduce
&& !si2reduce
)
998 // Transition if both paths end at the same symbol
999 if (*si1
->item
== *si2
->item
)
1001 int complexity
= ss
->complexity
+ 2 * SHIFT_COST
;
1002 parse_state_list trans1
= simulate_transition (ps1
);
1003 parse_state_list trans2
= simulate_transition (ps2
);
1004 parse_state
*tps1
= NULL
;
1005 parse_state
*tps2
= NULL
;
1006 for (gl_list_iterator_t it1
= gl_list_iterator (trans1
);
1007 parse_state_list_next (&it1
, &tps1
);
1009 for (gl_list_iterator_t it2
= gl_list_iterator (trans2
);
1010 parse_state_list_next (&it2
, &tps2
);
1012 ssb_append (new_search_state (tps1
, tps2
, complexity
));
1013 gl_list_free (trans1
);
1014 gl_list_free (trans2
);
1017 // Take production steps if possible.
1018 production_step (ss
, 0);
1019 production_step (ss
, 1);
1021 // One of the states requires a reduction
1024 const item_number
*rhs1
= item_rule_start (si1
->item
);
1025 const item_number
*rhe1
= item_rule_end (si1
->item
);
1026 int len1
= rhe1
- rhs1
;
1027 int size1
= parse_state_length (ps1
);
1028 bool ready1
= si1reduce
&& len1
< size1
;
1030 const item_number
*rhs2
= item_rule_start (si2
->item
);
1031 const item_number
*rhe2
= item_rule_end (si2
->item
);
1032 int len2
= rhe2
- rhs2
;
1033 int size2
= parse_state_length (ps2
);
1034 bool ready2
= si2reduce
&& len2
< size2
;
1035 // If there is a path ready for reduction without being
1036 // prepended further, reduce.
1037 if (ready1
&& ready2
)
1039 search_state_list reduced1
= reduction_step (ss
, conflict1
->item
, 0, len1
);
1040 gl_list_add_last (reduced1
, ss
);
1041 search_state
*red1
= NULL
;
1042 for (gl_list_iterator_t iter
= gl_list_iterator (reduced1
);
1043 search_state_list_next (&iter
, &red1
);
1046 search_state_list reduced2
=
1047 reduction_step (red1
, conflict2
->item
, 1, len2
);
1048 search_state
*red2
= NULL
;
1049 for (gl_list_iterator_t iter2
= gl_list_iterator (reduced2
);
1050 search_state_list_next (&iter2
, &red2
);
1053 // Avoid duplicates.
1056 gl_list_free (reduced2
);
1058 gl_list_free (reduced1
);
1062 search_state_list reduced1
= reduction_step (ss
, conflict1
->item
, 0, len1
);
1063 search_state
*red1
= NULL
;
1064 for (gl_list_iterator_t iter
= gl_list_iterator (reduced1
);
1065 search_state_list_next (&iter
, &red1
);
1068 gl_list_free (reduced1
);
1072 search_state_list reduced2
= reduction_step (ss
, conflict2
->item
, 1, len2
);
1073 search_state
*red2
= NULL
;
1074 for (gl_list_iterator_t iter2
= gl_list_iterator (reduced2
);
1075 search_state_list_next (&iter2
, &red2
);
1078 gl_list_free (reduced2
);
1080 /* Both states end with a reduction, yet they don't have enough symbols
1081 * to reduce. This means symbols are missing from the beginning of the
1082 * rule, so we must prepend */
1085 const symbol_number sym
1086 = si1reduce
&& !ready1
1089 search_state_prepend (ss
, sym
,
1090 parse_state_depth (ss
->states
[0]) >= 0
1091 ? rpp_set
: scp_set
);
1097 * Perform the actual counterexample search,
1098 * keeps track of what stage of the search algorithm
1099 * we are at and gives the appropriate counterexample
1100 * type based off of time constraints.
1102 static counterexample
*
1103 unifying_example (state_item_number itm1
,
1104 state_item_number itm2
,
1106 state_item_list reduce_path
, symbol_number next_sym
)
1108 state_item
*conflict1
= &state_items
[itm1
];
1109 state_item
*conflict2
= &state_items
[itm2
];
1110 search_state
*initial
= initial_search_state (conflict1
, conflict2
);
1111 ssb_queue
= gl_list_create_empty (GL_RBTREEHASH_LIST
,
1112 (gl_listelement_equals_fn
) ssb_equals
,
1113 (gl_listelement_hashcode_fn
) ssb_hasher
,
1114 (gl_listelement_dispose_fn
) ssb_free
,
1117 hash_initialize (32, NULL
, (Hash_hasher
) visited_hasher
,
1118 (Hash_comparator
) visited_comparator
,
1119 (Hash_data_freer
) search_state_free
);
1120 ssb_append (initial
);
1121 time_t start
= time (NULL
);
1122 bool assurance_printed
= false;
1123 search_state
*stage3result
= NULL
;
1124 counterexample
*cex
= NULL
;
1125 while (gl_list_size (ssb_queue
) > 0)
1127 const search_state_bundle
*ssb
= gl_list_get_at (ssb_queue
, 0);
1129 search_state
*ss
= NULL
;
1130 for (gl_list_iterator_t it
= gl_list_iterator (ssb
->states
);
1131 search_state_list_next (&it
, &ss
);
1134 if (trace_flag
& trace_cex
)
1135 search_state_print (ss
);
1136 // Stage 1/2 completing the rules containing the conflicts
1137 parse_state
*ps1
= ss
->states
[0];
1138 parse_state
*ps2
= ss
->states
[1];
1139 if (parse_state_depth (ps1
) < 0 && parse_state_depth (ps2
) < 0)
1141 // Stage 3: reduce and shift conflict items completed.
1142 const state_item
*si1src
= parse_state_head (ps1
);
1143 const state_item
*si2src
= parse_state_head (ps2
);
1144 if (item_rule (si1src
->item
)->lhs
== item_rule (si2src
->item
)->lhs
1145 && have_common_prefix (si1src
->item
, si2src
->item
))
1147 // Stage 4: both paths share a prefix
1148 derivation
*d1
= parse_state_derivation (ps1
);
1149 derivation
*d2
= parse_state_derivation (ps2
);
1150 if (parse_state_derivation_completed (ps1
)
1151 && parse_state_derivation_completed (ps2
))
1153 // Once we have two derivations for the same symbol,
1154 // we've found a unifying counterexample.
1155 cex
= new_counterexample (d1
, d2
, shift_reduce
, true, false);
1156 derivation_retain (d1
);
1157 derivation_retain (d2
);
1158 goto cex_search_end
;
1161 stage3result
= copy_search_state (ss
);
1164 if (TIME_LIMIT_ENFORCED
)
1166 float time_passed
= difftime (time (NULL
), start
);
1167 if (!assurance_printed
&& time_passed
> ASSURANCE_LIMIT
1170 fputs ("Productions leading up to the conflict state found. "
1171 "Still finding a possible unifying counterexample...",
1173 assurance_printed
= true;
1175 if (time_passed
> time_limit
)
1177 fprintf (stderr
, "time limit exceeded: %f\n", time_passed
);
1178 goto cex_search_end
;
1181 generate_next_states (ss
, conflict1
, conflict2
);
1183 gl_sortedlist_remove (ssb_queue
,
1184 (gl_listelement_compar_fn
) ssb_comp
, ssb
);
1189 // No unifying counterexamples
1190 // If a search state from Stage 3 is available, use it
1191 // to construct a more compact nonunifying counterexample.
1193 cex
= complete_diverging_examples (stage3result
, next_sym
, shift_reduce
);
1194 // Otherwise, construct a nonunifying counterexample that
1195 // begins from the start state using the shortest
1196 // lookahead-sensitive path to the reduce item.
1198 cex
= example_from_path (shift_reduce
, itm2
, reduce_path
, next_sym
);
1200 gl_list_free (ssb_queue
);
1201 hash_free (visited
);
1203 search_state_free (stage3result
);
1207 static time_t cumulative_time
;
1210 counterexample_init (void)
1212 /* Recognize $TIME_LIMIT. Not a public feature, just to help
1213 debugging. If we need something public, a %define/-D/-F variable
1214 would be more appropriate. */
1216 const char *cp
= getenv ("TIME_LIMIT");
1220 float v
= strtof (cp
, &end
);
1221 if (*end
== '\0' && errno
== 0)
1225 time (&cumulative_time
);
1226 scp_set
= bitset_create (nstates
, BITSET_FIXED
);
1227 rpp_set
= bitset_create (nstates
, BITSET_FIXED
);
1228 state_items_init ();
1233 counterexample_free (void)
1237 bitset_free (scp_set
);
1238 bitset_free (rpp_set
);
1239 state_items_free ();
1244 * Report a counterexample for conflict on symbol next_sym
1245 * between the given state-items
1248 counterexample_report (state_item_number itm1
, state_item_number itm2
,
1249 symbol_number next_sym
, bool shift_reduce
,
1250 FILE *out
, const char *prefix
)
1252 // Compute the shortest lookahead-sensitive path and associated sets of
1254 state_item_list shortest_path
= shortest_path_from_start (itm1
, next_sym
);
1255 bool reduce_prod_reached
= false;
1256 const rule
*reduce_rule
= item_rule (state_items
[itm1
].item
);
1258 bitset_zero (scp_set
);
1259 bitset_zero (rpp_set
);
1261 state_item
*si
= NULL
;
1262 for (gl_list_iterator_t it
= gl_list_iterator (shortest_path
);
1263 state_item_list_next (&it
, &si
);
1266 bitset_set (scp_set
, si
->state
->number
);
1267 reduce_prod_reached
= reduce_prod_reached
1268 || item_rule (si
->item
) == reduce_rule
;
1269 if (reduce_prod_reached
)
1270 bitset_set (rpp_set
, si
->state
->number
);
1272 time_t t
= time (NULL
);
1274 = difftime (t
, cumulative_time
) < CUMULATIVE_TIME_LIMIT
1275 ? unifying_example (itm1
, itm2
, shift_reduce
, shortest_path
, next_sym
)
1276 : example_from_path (shift_reduce
, itm2
, shortest_path
, next_sym
);
1278 gl_list_free (shortest_path
);
1279 counterexample_print (cex
, out
, prefix
);
1280 free_counterexample (cex
);
1284 // ITM1 denotes a shift, ITM2 a reduce.
1286 counterexample_report_shift_reduce (state_item_number itm1
, state_item_number itm2
,
1287 symbol_number next_sym
,
1288 FILE *out
, const char *prefix
)
1291 complain (NULL
, Wcounterexamples
,
1292 _("shift/reduce conflict on token %s"), symbols
[next_sym
]->tag
);
1295 fputs (prefix
, out
);
1296 fprintf (out
, _("shift/reduce conflict on token %s"), symbols
[next_sym
]->tag
);
1297 fprintf (out
, "%s\n", _(":"));
1299 // In the report, print the items.
1300 if (out
!= stderr
|| trace_flag
& trace_cex
)
1302 state_item_print (&state_items
[itm1
], out
, prefix
);
1303 state_item_print (&state_items
[itm2
], out
, prefix
);
1305 counterexample_report (itm1
, itm2
, next_sym
, true, out
, prefix
);
1309 counterexample_report_reduce_reduce (state_item_number itm1
, state_item_number itm2
,
1310 bitset conflict_syms
,
1311 FILE *out
, const char *prefix
)
1314 struct obstack obstack
;
1315 obstack_init (&obstack
);
1316 bitset_iterator biter
;
1317 state_item_number sym
;
1318 const char *sep
= "";
1319 BITSET_FOR_EACH (biter
, conflict_syms
, sym
, 0)
1321 obstack_printf (&obstack
, "%s%s", sep
, symbols
[sym
]->tag
);
1324 char *tokens
= obstack_finish0 (&obstack
);
1326 complain (NULL
, Wcounterexamples
,
1327 ngettext ("reduce/reduce conflict on token %s",
1328 "reduce/reduce conflict on tokens %s",
1329 bitset_count (conflict_syms
)),
1333 fputs (prefix
, out
);
1335 ngettext ("reduce/reduce conflict on token %s",
1336 "reduce/reduce conflict on tokens %s",
1337 bitset_count (conflict_syms
)),
1339 fprintf (out
, "%s\n", _(":"));
1341 obstack_free (&obstack
, NULL
);
1343 // In the report, print the items.
1344 if (out
!= stderr
|| trace_flag
& trace_cex
)
1346 state_item_print (&state_items
[itm1
], out
, prefix
);
1347 state_item_print (&state_items
[itm2
], out
, prefix
);
1349 counterexample_report (itm1
, itm2
, bitset_first (conflict_syms
),
1350 false, out
, prefix
);
1353 static state_item_number
1354 find_state_item_number (const rule
*r
, state_number sn
)
1356 for (state_item_number i
= state_item_map
[sn
]; i
< state_item_map
[sn
+ 1]; ++i
)
1357 if (!SI_DISABLED (i
)
1358 && item_number_as_rule_number (*state_items
[i
].item
) == r
->number
)
1364 counterexample_report_state (const state
*s
, FILE *out
, const char *prefix
)
1366 const state_number sn
= s
->number
;
1367 const reductions
*reds
= s
->reductions
;
1368 bitset lookaheads
= bitset_create (ntokens
, BITSET_FIXED
);
1369 for (int i
= 0; i
< reds
->num
; ++i
)
1371 const rule
*r1
= reds
->rules
[i
];
1372 const state_item_number c1
= find_state_item_number (r1
, sn
);
1373 for (state_item_number c2
= state_item_map
[sn
]; c2
< state_item_map
[sn
+ 1]; ++c2
)
1374 if (!SI_DISABLED (c2
))
1376 item_number conf
= *state_items
[c2
].item
;
1377 if (item_number_is_symbol_number (conf
)
1378 && bitset_test (reds
->lookaheads
[i
], conf
))
1379 counterexample_report_shift_reduce (c1
, c2
, conf
, out
, prefix
);
1381 for (int j
= i
+1; j
< reds
->num
; ++j
)
1383 const rule
*r2
= reds
->rules
[j
];
1384 // Conflicts: common lookaheads.
1385 bitset_intersection (lookaheads
,
1386 reds
->lookaheads
[i
],
1387 reds
->lookaheads
[j
]);
1388 if (!bitset_empty_p (lookaheads
))
1389 for (state_item_number c2
= state_item_map
[sn
]; c2
< state_item_map
[sn
+ 1]; ++c2
)
1390 if (!SI_DISABLED (c2
)
1391 && item_rule (state_items
[c2
].item
) == r2
)
1393 counterexample_report_reduce_reduce (c1
, c2
, lookaheads
, out
, prefix
);
1398 bitset_free (lookaheads
);