From b82092a12395b1c23597e3b095848c14bec4eef3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Sep 2014 08:39:39 -0700 Subject: [PATCH] fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172 --- src/frontends/lean/parser.cpp | 24 ++++++++++++------- src/frontends/lean/parser.h | 19 ++++++++------- src/frontends/lean/server.cpp | 2 +- tests/lean/interactive/optstack.input | 5 ++++ .../interactive/optstack.input.expected.out | 4 ++++ tests/lean/interactive/whnfinst.lean | 14 +++++++++++ 6 files changed, 49 insertions(+), 19 deletions(-) create mode 100644 tests/lean/interactive/optstack.input create mode 100644 tests/lean/interactive/optstack.input.expected.out create mode 100644 tests/lean/interactive/whnfinst.lean diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index bab003324..8f1b1b3a1 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -82,15 +82,19 @@ static name g_tmp_prefix = name::mk_internal_unique_name(); parser::parser(environment const & env, io_state const & ios, std::istream & strm, char const * strm_name, bool use_exceptions, unsigned num_threads, - local_level_decls const & lds, local_expr_decls const & eds, - unsigned line, snapshot_vector * sv, info_manager * im): + snapshot const * s, snapshot_vector * sv, info_manager * im): m_env(env), m_ios(ios), m_ngen(g_tmp_prefix), m_verbose(true), m_use_exceptions(use_exceptions), - m_scanner(strm, strm_name, line), m_local_level_decls(lds), m_local_decls(eds), + m_scanner(strm, strm_name, s ? s->m_line : 1), m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) { + if (s) { + m_local_level_decls = s->m_lds; + m_local_decls = s->m_eds; + m_options_stack = s->m_options_stack; + } m_num_threads = num_threads; - m_no_undef_id_error = false; + m_no_undef_id_error = false; m_found_errors = false; m_used_sorry = false; updt_options(); @@ -393,19 +397,20 @@ void parser::push_local_scope(bool save_options) { m_local_level_decls.push(); m_local_decls.push(); if (save_options) - m_options_stack.push_back(optional(m_ios.get_options())); + m_options_stack = cons(optional(m_ios.get_options()), m_options_stack); else - m_options_stack.push_back(optional()); + m_options_stack = cons(optional(), m_options_stack); } void parser::pop_local_scope() { m_local_level_decls.pop(); m_local_decls.pop(); - if (auto const & it = m_options_stack.back()) { + lean_assert(!is_nil(m_options_stack)); + if (auto const & it = head(m_options_stack)) { m_ios.set_options(*it); updt_options(); } - m_options_stack.pop_back(); + m_options_stack = tail(m_options_stack); } void parser::add_local_level(name const & n, level const & l) { @@ -1316,7 +1321,8 @@ void parser::save_snapshot() { if (!m_snapshot_vector) return; if (m_snapshot_vector->empty() || static_cast(m_snapshot_vector->back().m_line) != m_scanner.get_line()) - m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_ios.get_options(), m_scanner.get_line())); + m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, + m_options_stack, m_ios.get_options(), m_scanner.get_line())); } void parser::save_pre_info_data() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index cbfbc7bb7..e35b6f26b 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -41,27 +41,29 @@ struct parser_error : public exception { }; struct interrupt_parser {}; -typedef local_decls local_expr_decls; -typedef local_decls local_level_decls; -typedef environment local_environment; +typedef local_decls local_expr_decls; +typedef local_decls local_level_decls; +typedef list> options_stack; +typedef environment local_environment; /** \brief Snapshot of the state of the Lean parser */ struct snapshot { environment m_env; local_level_decls m_lds; local_expr_decls m_eds; + options_stack m_options_stack; options m_options; unsigned m_line; snapshot():m_line(0) {} snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {} - snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds, options const & opts, unsigned line): - m_env(env), m_lds(lds), m_eds(eds), m_options(opts), m_line(line) {} + snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds, + options_stack const & os, options const & opts, unsigned line): + m_env(env), m_lds(lds), m_eds(eds), m_options_stack(os), m_options(opts), m_line(line) {} }; typedef std::vector snapshot_vector; class parser { - typedef std::vector> options_stack; environment m_env; io_state m_ios; name_generator m_ngen; @@ -183,9 +185,8 @@ public: parser(environment const & env, io_state const & ios, std::istream & strm, char const * str_name, bool use_exceptions = false, unsigned num_threads = 1, - local_level_decls const & lds = local_level_decls(), - local_expr_decls const & eds = local_expr_decls(), unsigned line = 1, - snapshot_vector * sv = nullptr, info_manager * im = nullptr); + snapshot const * s = nullptr, snapshot_vector * sv = nullptr, + info_manager * im = nullptr); ~parser(); void set_cache(definition_cache * c) { m_cache = c; } diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index c6c676bd3..ff8c8a615 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -202,7 +202,7 @@ server::worker::worker(environment const & env, io_state const & ios, definition bool use_exceptions = false; unsigned num_threads = 1; parser p(s.m_env, tmp_ios, strm, todo_file->m_fname.c_str(), use_exceptions, num_threads, - s.m_lds, s.m_eds, s.m_line, &todo_file->m_snapshots, &todo_file->m_info); + &s, &todo_file->m_snapshots, &todo_file->m_info); p.set_cache(&m_cache); p(); } catch (interrupted &) { diff --git a/tests/lean/interactive/optstack.input b/tests/lean/interactive/optstack.input new file mode 100644 index 000000000..0866da5ec --- /dev/null +++ b/tests/lean/interactive/optstack.input @@ -0,0 +1,5 @@ +LOAD whnfinst.lean +WAIT +REPLACE 14 +end +WAIT \ No newline at end of file diff --git a/tests/lean/interactive/optstack.input.expected.out b/tests/lean/interactive/optstack.input.expected.out new file mode 100644 index 000000000..2e3f2f194 --- /dev/null +++ b/tests/lean/interactive/optstack.input.expected.out @@ -0,0 +1,4 @@ +-- BEGINWAIT +-- ENDWAIT +-- BEGINWAIT +-- ENDWAIT diff --git a/tests/lean/interactive/whnfinst.lean b/tests/lean/interactive/whnfinst.lean new file mode 100644 index 000000000..f79626431 --- /dev/null +++ b/tests/lean/interactive/whnfinst.lean @@ -0,0 +1,14 @@ +import logic +open decidable + +abbreviation decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y) + +section + parameter {A : Type} + parameter (R : A → A → Prop) + + theorem tst1 (H : Πx y, decidable (R x y)) (a b c : A) : decidable (R a b ∧ R b a) + + theorem tst2 (H : decidable_bin_rel R) (a b c : A) : decidable (R a b ∧ R b a ∨ R b b) := + _ +end