From 86646ac31f7540af750e810247f22e46ff596e5a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 Feb 2016 19:12:48 +0100 Subject: [PATCH] bin: fix destruction order of global variables Fixes #142, reported by Joachim Klein. * bin/autfilt.cc, bin/ltlfilt.cc, bin/randaut.cc, bin/randltl.cc: Make sure all global variables that have a destructor are destructed in the main. Otherwise they risk being destructed after the library's global structures are destructed, causing access to freed memory. * NEWS: Mention the bug. --- NEWS | 4 +- bin/autfilt.cc | 18 ++++----- bin/ltlfilt.cc | 54 +++++++++++++++++--------- bin/randaut.cc | 103 ++++++++++++++++++++++++++++--------------------- bin/randltl.cc | 48 +++++++++++++++-------- 5 files changed, 137 insertions(+), 90 deletions(-) diff --git a/NEWS b/NEWS index 7c6a06c90..d91043dff 100644 --- a/NEWS +++ b/NEWS @@ -52,10 +52,12 @@ New in spot 1.99.7a (not yet released) pointers) for some concepts used in Spot. See https://spot.lrde.epita.fr/concepts.html - Bugs: + Bug fixes: * Using ltl2tgba -U would fail to output the unambiguous property (regression introduced in 1.99.7) + * ltlfilt, autfilt, randltl, and randaut could easily crash when + compiled statically (i.e., with configure --disable-shared). New in spot 1.99.7 (2016-01-15) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 317facbfa..f8c53bb5b 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -249,7 +249,7 @@ static bool randomize_st = false; static bool randomize_tr = false; static int opt_seed = 0; -// We want all these variable to be destroyed when we exit main, to +// We want all these variables to be destroyed when we exit main, to // make sure it happens before all other global variables (like the // atomic propositions maps) are destroyed. Otherwise we risk // accessing deleted stuff. @@ -263,6 +263,8 @@ static struct opt_t std::unique_ptr isomorphism_checker = nullptr; std::unique_ptr uniq = nullptr; + spot::exclusive_ap excl_ap; + spot::remove_ap rem_ap; }* opt; static bool opt_merge = false; @@ -291,8 +293,6 @@ static char* opt_decompose_strength = nullptr; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; -static spot::exclusive_ap excl_ap; -static spot::remove_ap rem_ap; static bool opt_simplify_exclusive_ap = false; static bool opt_rem_dead = false; static bool opt_rem_unreach = false; @@ -361,7 +361,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; case OPT_EXCLUSIVE_AP: - excl_ap.add_group(arg); + opt->excl_ap.add_group(arg); break; case OPT_INSTUT: if (!arg || (arg[0] == '1' && arg[1] == 0)) @@ -474,7 +474,7 @@ parse_opt(int key, char* arg, struct argp_state*) } break; case OPT_REM_AP: - rem_ap.add_ap(arg); + opt->rem_ap.add_ap(arg); break; case OPT_REM_DEAD: opt_rem_dead = true; @@ -619,11 +619,11 @@ namespace if (opt_mask_acc) aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); - if (!excl_ap.empty()) - aut = excl_ap.constrain(aut, opt_simplify_exclusive_ap); + if (!opt->excl_ap.empty()) + aut = opt->excl_ap.constrain(aut, opt_simplify_exclusive_ap); - if (!rem_ap.empty()) - aut = rem_ap.strip(aut); + if (!opt->rem_ap.empty()) + aut = opt->rem_ap.strip(aut); if (opt_destut) aut = spot::closure(std::move(aut)); diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 7f811b3a3..d832d9411 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -258,13 +258,23 @@ static bool ap = false; static unsigned ap_n = 0; static int opt_max_count = -1; static long int match_count = 0; -static spot::exclusive_ap excl_ap; -static std::unique_ptr output_define = nullptr; + + +// We want all these variables to be destroyed when we exit main, to +// make sure it happens before all other global variables (like the +// atomic propositions maps) are destroyed. Otherwise we risk +// accessing deleted stuff. +static struct opt_t +{ + spot::exclusive_ap excl_ap; + std::unique_ptr output_define = nullptr; + spot::formula implied_by = nullptr; + spot::formula imply = nullptr; + spot::formula equivalent_to = nullptr; +}* opt; + static std::string unabbreviate; -static spot::formula implied_by = nullptr; -static spot::formula imply = nullptr; -static spot::formula equivalent_to = nullptr; static spot::formula parse_formula_arg(const std::string& input) @@ -317,7 +327,7 @@ parse_opt(int key, char* arg, struct argp_state*) bsize_max = to_int(arg); break; case OPT_DEFINE: - output_define.reset(new output_file(arg ? arg : "-")); + opt->output_define.reset(new output_file(arg ? arg : "-")); break; case OPT_DROP_ERRORS: error_style = drop_errors; @@ -327,13 +337,13 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_EQUIVALENT_TO: { - if (equivalent_to) + if (opt->equivalent_to) error(2, 0, "only one --equivalent-to option can be given"); - equivalent_to = parse_formula_arg(arg); + opt->equivalent_to = parse_formula_arg(arg); break; } case OPT_EXCLUSIVE_AP: - excl_ap.add_group(arg); + opt->excl_ap.add_group(arg); break; case OPT_GUARANTEE: guarantee = obligation = true; @@ -345,14 +355,14 @@ parse_opt(int key, char* arg, struct argp_state*) { spot::formula i = parse_formula_arg(arg); // a→c∧b→c ≡ (a∨b)→c - implied_by = spot::formula::Or({implied_by, i}); + opt->implied_by = spot::formula::Or({opt->implied_by, i}); break; } case OPT_IMPLY: { // a→b∧a→c ≡ a→(b∧c) spot::formula i = parse_formula_arg(arg); - imply = spot::formula::And({imply, i}); + opt->imply = spot::formula::And({opt->imply, i}); break; } case OPT_LTL: @@ -536,8 +546,8 @@ namespace if (!unabbreviate.empty()) f = spot::unabbreviate(f, unabbreviate.c_str()); - if (!excl_ap.empty()) - f = excl_ap.constrain(f); + if (!opt->excl_ap.empty()) + f = opt->excl_ap.constrain(f); bool matched = true; @@ -568,9 +578,10 @@ namespace matched &= (bsize_max < 0) || (l <= bsize_max); } - matched &= !implied_by || simpl.implication(implied_by, f); - matched &= !imply || simpl.implication(f, imply); - matched &= !equivalent_to || simpl.are_equivalent(f, equivalent_to); + matched &= !opt->implied_by || simpl.implication(opt->implied_by, f); + matched &= !opt->imply || simpl.implication(f, opt->imply); + matched &= !opt->equivalent_to + || simpl.are_equivalent(f, opt->equivalent_to); matched &= !stutter_insensitive || spot::is_stutter_invariant(f); // Match obligations and subclasses using WDBA minimization. @@ -601,7 +612,7 @@ namespace if (matched) { - if (output_define + if (opt->output_define && output_format != count_output && output_format != quiet_output) { @@ -610,7 +621,7 @@ namespace for (auto& p: relmap) m.emplace(str_psl(p.first), p.second); for (auto& p: m) - stream_formula(output_define->ostream() + stream_formula(opt->output_define->ostream() << "#define " << p.first << " (", p.second, filename, linenum) << ")\n"; } @@ -633,6 +644,11 @@ main(int argc, char** argv) try { + // This will ensure that all objects stored in this struct are + // destroyed before global variables. + opt_t o; + opt = &o; + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); diff --git a/bin/randaut.cc b/bin/randaut.cc index 95e060e5a..58dd51047 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -132,10 +132,18 @@ static const struct argp_child children[] = { nullptr, 0, nullptr, 0 } }; +// We want all these variables to be destroyed when we exit main, to +// make sure it happens before all other global variables (like the +// atomic propositions maps) are destroyed. Otherwise we risk +// accessing deleted stuff. +static struct opt_t +{ + spot::atomic_prop_set aprops; +}* opt; + static const char* opt_acceptance = nullptr; typedef spot::twa_graph::graph_t::edge_storage_t tr_t; typedef std::set> unique_aut_t; -static spot::atomic_prop_set aprops; static range ap_count_given = {-1, -2}; // Must be two different negative val static int opt_seed = 0; static const char* opt_seed_str = "0"; @@ -246,15 +254,16 @@ parse_opt(int key, char* arg, struct argp_state* as) // non-options. So if as->argc == as->next we know this is the // last non-option argument, and if aprops.empty() we know this // is the also the first one. - if (aprops.empty() && as->argc == as->next && looks_like_a_range(arg)) + if (opt->aprops.empty() + && as->argc == as->next && looks_like_a_range(arg)) { ap_count_given = parse_range(arg); // Create the set once if the count is fixed. if (ap_count_given.min == ap_count_given.max) - aprops = spot::create_atomic_prop_set(ap_count_given.min); + opt->aprops = spot::create_atomic_prop_set(ap_count_given.min); break; } - aprops.insert(spot::formula::ap(arg)); + opt->aprops.insert(spot::formula::ap(arg)); break; default: @@ -274,46 +283,52 @@ main(int argc, char** argv) const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc, children, nullptr, nullptr }; - if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) - exit(err); - - // running 'randaut 0' is one way to generate automata using no - // atomic propositions so do not complain in that case. - if (aprops.empty() && ap_count_given.max < 0) - error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.", - program_name); - - if (generic_wanted && automaton_format == Spin) - error(2, 0, "--spin implies --ba so should not be used with --acceptance"); - if (generic_wanted && ba_wanted) - error(2, 0, "--acceptance and --ba may not be used together"); - - if (automaton_format == Spin && opt_acc_sets.max > 1) - error(2, 0, "--spin is incompatible with --acceptance=%d..%d", - opt_acc_sets.min, opt_acc_sets.max); - if (ba_wanted && opt_acc_sets.min != 1 && opt_acc_sets.max != 1) - error(2, 0, "--ba is incompatible with --acceptance=%d..%d", - opt_acc_sets.min, opt_acc_sets.max); - if (ba_wanted && generic_wanted) - error(2, 0, "--ba is incompatible with --acceptance=%s", opt_acceptance); - - if (automaton_format == Spin) - ba_options(); - - if (opt_colored && opt_acc_sets.min == -1 && !generic_wanted) - error(2, 0, "--colored requires at least one acceptance set; " - "use --acceptance"); - if (opt_colored && opt_acc_sets.min == 0) - error(2, 0, "--colored requires at least one acceptance set; " - "fix the range of --acceptance"); - - if (opt_acc_sets.min == -1) - opt_acc_sets.min = 0; - - - try { + // This will ensure that all objects stored in this struct are + // destroyed before global variables. + opt_t o; + opt = &o; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) + exit(err); + + // running 'randaut 0' is one way to generate automata using no + // atomic propositions so do not complain in that case. + if (opt->aprops.empty() && ap_count_given.max < 0) + error(2, 0, + "No atomic proposition supplied? Run '%s --help' for usage.", + program_name); + + if (generic_wanted && automaton_format == Spin) + error(2, 0, + "--spin implies --ba so should not be used with --acceptance"); + if (generic_wanted && ba_wanted) + error(2, 0, "--acceptance and --ba may not be used together"); + + if (automaton_format == Spin && opt_acc_sets.max > 1) + error(2, 0, "--spin is incompatible with --acceptance=%d..%d", + opt_acc_sets.min, opt_acc_sets.max); + if (ba_wanted && opt_acc_sets.min != 1 && opt_acc_sets.max != 1) + error(2, 0, "--ba is incompatible with --acceptance=%d..%d", + opt_acc_sets.min, opt_acc_sets.max); + if (ba_wanted && generic_wanted) + error(2, 0, + "--ba is incompatible with --acceptance=%s", opt_acceptance); + + if (automaton_format == Spin) + ba_options(); + + if (opt_colored && opt_acc_sets.min == -1 && !generic_wanted) + error(2, 0, "--colored requires at least one acceptance set; " + "use --acceptance"); + if (opt_colored && opt_acc_sets.min == 0) + error(2, 0, "--colored requires at least one acceptance set; " + "fix the range of --acceptance"); + + if (opt_acc_sets.min == -1) + opt_acc_sets.min = 0; + spot::srand(opt_seed); auto d = spot::make_bdd_dict(); @@ -333,7 +348,7 @@ main(int argc, char** argv) && ap_count_given.min != ap_count_given.max) { int c = spot::rrand(ap_count_given.min, ap_count_given.max); - aprops = spot::create_atomic_prop_set(c); + opt->aprops = spot::create_atomic_prop_set(c); } int size = opt_states.min; @@ -355,7 +370,7 @@ main(int argc, char** argv) } auto aut = - spot::random_graph(size, opt_density, &aprops, d, + spot::random_graph(size, opt_density, &opt->aprops, d, accs, opt_acc_prob, 0.5, opt_deterministic, opt_state_acc, opt_colored); diff --git a/bin/randltl.cc b/bin/randltl.cc index 569c46051..091ff3b3b 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -130,7 +130,15 @@ const struct argp_child children[] = { nullptr, 0, nullptr, 0 } }; -spot::atomic_prop_set aprops; +// We want all these variables to be destroyed when we exit main, to +// make sure it happens before all other global variables (like the +// atomic propositions maps) are destroyed. Otherwise we risk +// accessing deleted stuff. +static struct opt_t +{ + spot::atomic_prop_set aprops; +}* opt; + static int output = OUTPUTLTL; static char* opt_pL = nullptr; static char* opt_pS = nullptr; @@ -202,18 +210,18 @@ parse_opt(int key, char* arg, struct argp_state* as) // non-options. So if as->argc == as->next we know this is the // last non-option argument, and if aprops.empty() we know this // is the also the first one. - if (aprops.empty() && as->argc == as->next) + if (opt->aprops.empty() && as->argc == as->next) { char* endptr; int res = strtol(arg, &endptr, 10); if (!*endptr && res >= 0) // arg is a number { ap_count_given = true; - aprops = spot::create_atomic_prop_set(res); + opt->aprops = spot::create_atomic_prop_set(res); break; } } - aprops.insert(spot::default_environment::instance().require(arg)); + opt->aprops.insert(spot::default_environment::instance().require(arg)); break; default: return ARGP_ERR_UNKNOWN; @@ -229,20 +237,26 @@ main(int argc, char** argv) const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc, children, nullptr, nullptr }; - if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) - exit(err); - - // running 'randltl 0' is one way to generate formulas using no - // atomic propositions so do not complain in that case. - if (aprops.empty() && !ap_count_given) - error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.", - program_name); - - spot::srand(opt_seed); try { + // This will ensure that all objects stored in this struct are + // destroyed before global variables. + opt_t o; + opt = &o; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) + exit(err); + + // running 'randltl 0' is one way to generate formulas using no + // atomic propositions so do not complain in that case. + if (opt->aprops.empty() && !ap_count_given) + error(2, 0, "No atomic proposition supplied? " + "Run '%s --help' for usage.", program_name); + + spot::srand(opt_seed); + spot::randltlgenerator rg - (aprops, + (opt->aprops, [&] (){ spot::option_map opts; opts.set("output", output);