max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/trace): prevent memory corruption with scope_traces_as_messages

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-12 10:52:10 -04:00 • committed by Leonardo de Moura
parent 9e518efe46
commit 60afce092a
3 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/parser.cpp
View file

@ -2029,7 +2029,7 @@ void parser::parse_command() {
lazy_type_context tc(m_env, get_options());
scope_global_ios scope1(m_ios);
scope_trace_env scope2(m_env, m_ios.get_options(), tc);
scope_traces_as_messages traces_as_messages(get_file_name(), pos());
scope_traces_as_messages traces_as_messages(get_stream_name(), pos());
if (is_notation_cmd(cmd_name)) {
in_notation_ctx ctx(*this);
if (it->get_skip_token())

5
src/library/trace.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <vector>
#include <string>
#include "util/sexpr/option_declarations.h"
#include "kernel/environment.h"
#include "kernel/type_checker.h"
@ -218,7 +219,7 @@ void finalize_trace() {
delete g_trace_as_messages;
}
scope_traces_as_messages::scope_traces_as_messages(char const * stream_name, pos_info const & pos) :
scope_traces_as_messages::scope_traces_as_messages(std::string const & stream_name, pos_info const & pos) :
m_stream_name(stream_name), m_pos(pos) {
if (get_global_ios().get_options().get_bool(*g_trace_as_messages, false)) {
m_redirected_ios = std::unique_ptr<io_state>(new io_state(get_global_ios()));
@ -231,7 +232,7 @@ scope_traces_as_messages::scope_traces_as_messages(char const * stream_name, pos
scope_traces_as_messages::scope_traces_as_messages(pos_info_provider const *provider, expr const &ref) :
scope_traces_as_messages(provider ? provider->get_file_name() : "<unknown>",
provider ? provider->get_pos_info_or_some(ref) : pos_info(0, 0)) {}
provider ? provider->get_pos_info_or_some(ref) : pos_info(1, 0)) {}
scope_traces_as_messages::~scope_traces_as_messages() {
if (enabled()) {

5
src/library/trace.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include <string>
#include "library/io_state_stream.h"
namespace lean {
@ -31,14 +32,14 @@ public:
};
class scope_traces_as_messages {
char const * m_stream_name;
std::string m_stream_name;
pos_info m_pos;
std::unique_ptr<io_state> m_redirected_ios;
std::unique_ptr<scope_global_ios> m_scoped_ios;
std::shared_ptr<string_output_channel> m_buffer;
public:
scope_traces_as_messages(char const * stream_name, pos_info const & pos);
scope_traces_as_messages(std::string const & stream_name, pos_info const & pos);
scope_traces_as_messages(pos_info_provider const * provider, expr const & ref);
~scope_traces_as_messages();
bool enabled() const { return static_cast<bool>(m_scoped_ios); }