20 Commits
Author SHA1 Message Date
Vincent ImbimboandAkim Demaille 2c294c1325 cex: fix state-item pruning
There were several bugs in pruning that would leave the state-item
graph in an inconsistent state which could cause crashes later on:

- Pruning now happens in one pass instead of two.

- Disabled state-items no longer prune the state-items they transition
  to if that state-item has other states that transition to it.

- State-items that transition to disabled state-items are always
  pruned even if they have productions.

Reported by Michal Bartkowiak <[email protected]>
https://lists.gnu.org/r/bug-bison/2021-01/msg00000.html
and Zartaj Majeed
https://github.com/akimd/bison/issues/71

* src/state-item.c (prune_forward, prune_backward): Fuse into...
(prune_state_item): this.
Adjust callers.
2021-01-24 08:24:56 +01:00
Vincent ImbimboandAkim Demaille 1247d94ba6 doc: cex documentation
* NEWS, doc/bison.texi: Add documentation for conflict counterexample
generation.
2020-06-30 08:01:40 +02:00
Vincent ImbimboandAkim Demaille 69e3b405d9 cex: fix reporting of null nonterminals
I implemented this to print A ::= [ ], but A ::= [ %empty ] might be
clearer.

* src/parse-simulation.c (nullable_closure): Don't generate null
nonterminal derivations as leaves.
* src/derivation.c (derivation_print_impl): Don't print seperator
spaces for null nonterminal.
* tests/counterexample.at: Update test results.
2020-06-22 07:11:31 +02:00
Vincent ImbimboandAkim Demaille 6a1a681fd2 style: decouple different uses of item_number
item_number is used for elements of ritem as well as indices into
ritem which is fairly confusing.  Introduce item_index to represent
indices into ritem.

* src/gram.h (item_index): Introduce it for ritem indices.
* src/closure.h, src/closure.c, src/ielr.c, src/lr0.c,
* src/print-graph.c, src/state.h, src/state.h:
Replace uses of item_number with item_index where appropriate.
2020-05-25 07:14:34 +02:00
Vincent ImbimboandAkim Demaille 50cd3f16de cex: fix pruning crash
Fixes a crash on Cim's grammar.
https://lists.gnu.org/r/bison-patches/2020-05/msg00107.html

* src/state-item.c (prune_disabled_paths): Prune forward and backwards
paths in seperate passes.
(prune_forward, prune_backward): New.
(disable_state_item): Change function argument from state_item_number
to state_item.
(state_items_report): Add disabling to graph print-out.
* src/conflicts.c (find_state_item_number,
report_state_counterexamples): Add SI_DISABLED checks.
2020-05-23 17:35:19 +02:00
Vincent ImbimboandAkim Demaille 99260caef9 cex: replace state-item data structures
* src/state-item.h: Add trans, prods, and revs edges to state-item
struct.
(si_trans, si_revs, si_prods_lookup): Remove.
* src/state-item.c, src/lssi.c, src/parse-simulation.c,
* src/counterexample.c: Update state-item API usage accordingly.
2020-05-22 08:45:44 +02:00
Vincent ImbimboandAkim Demaille c19af5cbb4 cex: fix bad reference counting
* src/counterexample.c (si_bfs_free): Fix reference_count
decrementing.
2020-05-22 08:45:44 +02:00
Vincent ImbimboandAkim Demaille b54181ff9b cex: fix miscellaneous leaks
* src/counterexample.c (unifying_counterexample): Always free
stage3result when it exists.
* src/conflicts.c (report_state_counterexamples): free leaked bitset.
* src/state-item.c (prune_disabled_paths): free leaked queue.
2020-05-22 08:45:44 +02:00
Vincent ImbimboandAkim Demaille 86c45be582 cex: fix counterexample leak
* src/counterexample.c (free_counterexample): New.
Free counterexamples after printing.
2020-05-22 08:45:44 +02:00
Vincent ImbimboandAkim Demaille b5e0351c3e cex: fix lssi leaks
* src/lssi.c (shortest_path_from_start): Free the root of
shortest_path_from_start search.
Free eligible bitset.
2020-05-22 08:45:44 +02:00
Vincent ImbimboandAkim Demaille 150b2318ed cex: fix parse state leaks
* src/parse_simulation.c: Fix bug in parse_state_free.
Free new_root when simulate_reduction generates zero states.

* src/parse-simulation.c, src/parse-simulation.h
(parse_state_list, parse_state_list_append): New.
* src/parse-simulation.c, src/parse-simulation.h,
* src/counterexample.c: Replace all uses of lists of parse states and
appends to parse_state_lists with the new API.
2020-05-22 08:45:44 +02:00
Vincent ImbimboandAkim Demaille 35c4a8e65e cex: derivation reference counting
* src/derivation.h, src/derivation.c: Make derivation struct opaque.
Add derivation_list type for clarity.
(derivation_list_new): New.
(derivation_list_append): New.
(derivation_list_prepend): New.
(derivation_new_leaf): New constructor for derivations with no
children.
* src/counterexample.c, src/parse-simulation.c,
* src/parse-simulation.h: Replace uses of gl_list_t containing
derivations with derivation_list and its API.
Replace calls of dervation_new using null children with
derivation_new_leaf.
* src/parse-simulation.c: replace ps_chunk and its API with typed
versions si_chunk and deriv_chunk.
* src/parse-simlation.h, src/parse-simulation.c: Remove
parse_state_retain_deriv in favor of derivation reference counting.
* src/counterexample.c: Remove search_state_retain_deriv.
2020-05-22 08:45:44 +02:00
Vincent ImbimboandAkim Demaille 2d8c3edbf8 cex: fix leaks
* src/state-item.c: Various functions were using heap allocated locals
and not freeing them.
2020-05-22 08:45:43 +02:00
Vincent ImbimboandAkim Demaille 482b370540 cex: fix stack overflow
* src/parse-simulation.c: Replace reference counting with
parse_state_retain everywhere.
(free_parse_state): Make this function iterative instead of
recursive. Long parse_state chains were causing stack exhaustion.

* tests/counterexample.at: Fix expectations.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille 66283fb625 cex: fix crash from zombie result
Fixes the SEGV in test 247 (counterexample.at:195): "S/R after first
token".

* src/counterexample.c: here.
* tests/counterexample.at: Fix expectations.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille dcb6c972a2 cex: add tests
* tests/counterexample.at: New.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille af0441cfd2 cex: bind counterexample generation
* src/complain.h, src/complain.c: Add support for -Wcounterexample.
* src/conflicts.c (report_counterexamples): New.
(rule_conflicts_print): Use it when -Wcounterexample is given.
* src/getargs.h, src/getargs.c: Add support for --trace=cex.
* src/main.c (main): Init and deinit counterexample generation.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille bbb63b1ca9 cex: introduce counterexample search
* src/counterexample.h, src/counterexample.c: New.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille ac54d19eba cex: introduce the parse simulator
* src/derivation.h, src/derivation.c,
* src/parse-simulation.h, src/parse-simulation.c: New.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille 5807dd9279 cex: add support for state-item pair graph generation
* src/lssi.h, src/lssi.c, src/state-item.h, src/state-item.c: New.
2020-05-22 07:52:27 +02:00