alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

bin: fix destruction order of global variables

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2016-02-10 19:12:48 +01:00
parent bceb54c80e
commit 86646ac31f
5 changed files with 137 additions and 90 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -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)

18
bin/autfilt.cc
View file

@ -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<spot::isomorphism_checker>
isomorphism_checker = nullptr;
std::unique_ptr<unique_aut_t> 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<bool> 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<int>::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));

54
bin/ltlfilt.cc
View file

@ -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_file> 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_file> 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);

43
bin/randaut.cc
View file

@ -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<std::vector<tr_t>> 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,17 +283,26 @@ main(int argc, char** argv)
const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
children, nullptr, nullptr };
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 (aprops.empty() && ap_count_given.max < 0)
error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.",
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");
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");
@ -295,7 +313,8 @@ main(int argc, char** argv)
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);
error(2, 0,
"--ba is incompatible with --acceptance=%s", opt_acceptance);
if (automaton_format == Spin)
ba_options();
@ -310,10 +329,6 @@ main(int argc, char** argv)
if (opt_acc_sets.min == -1)
opt_acc_sets.min = 0;
try
{
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);

38
bin/randltl.cc
View file

@ -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 };
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 (aprops.empty() && !ap_count_given)
error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.",
program_name);
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);
try
{
spot::randltlgenerator rg
(aprops,
(opt->aprops,
[&] (){
spot::option_map opts;
opts.set("output", output);