diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index fcfc4097c..d573ca95d 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -63,7 +63,7 @@ public: case level_kind::Succ: return mk_succ(read()); } - throw_corrupted_file(); + throw corrupted_stream_exception(); }); } }; @@ -247,7 +247,7 @@ public: binder_info bi = read_binder_info(d); return mk_local(n, pp_n, read(), bi); }} - throw_corrupted_file(); // LCOV_EXCL_LINE + throw corrupted_stream_exception(); // LCOV_EXCL_LINE }); } }; @@ -363,7 +363,7 @@ static register_macro_deserializer_fn annotation_des_fn(get_annotation_opcode(), [](deserializer & d, unsigned num, expr const * args) { if (num != 1) - throw_corrupted_file(); + throw corrupted_stream_exception(); name k; d >> k; return mk_annotation(k, args[0]); diff --git a/src/library/module.cpp b/src/library/module.cpp index 1c9d5fada..522a7ae88 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -28,6 +28,10 @@ Author: Leonardo de Moura #endif namespace lean { +corrupted_file_exception::corrupted_file_exception(std::string const & fname): + exception(sstream() << "failed to import '" << fname << "', file is corrupted") { +} + typedef std::pair> writer; struct module_ext : public environment_extension { @@ -229,47 +233,50 @@ struct import_modules_fn { std::ifstream in(fname, std::ifstream::binary); if (!in.good()) throw exception(sstream() << "failed to open file '" << fname << "'"); - deserializer d1(in); - std::string header; - d1 >> header; - if (header != g_olean_header) - throw exception(sstream() << "file '" << fname << "' does not seem to be a valid object Lean file, invalid header"); - unsigned major, minor, claimed_hash; - d1 >> major >> minor >> claimed_hash; - // Enforce version? + try { + deserializer d1(in); + std::string header; + d1 >> header; + if (header != g_olean_header) + throw exception(sstream() << "file '" << fname << "' does not seem to be a valid object Lean file, invalid header"); + unsigned major, minor, claimed_hash; + d1 >> major >> minor >> claimed_hash; + // Enforce version? - unsigned num_imports = d1.read_unsigned(); - buffer imports; - for (unsigned i = 0; i < num_imports; i++) - imports.push_back(read_module_name(d1)); + unsigned num_imports = d1.read_unsigned(); + buffer imports; + for (unsigned i = 0; i < num_imports; i++) + imports.push_back(read_module_name(d1)); - unsigned code_size = d1.read_unsigned(); - std::vector code(code_size); - for (unsigned i = 0; i < code_size; i++) - code[i] = d1.read_char(); + unsigned code_size = d1.read_unsigned(); + std::vector code(code_size); + for (unsigned i = 0; i < code_size; i++) + code[i] = d1.read_char(); - unsigned computed_hash = hash(code_size, [&](unsigned i) { return code[i]; }); - if (claimed_hash != computed_hash) - throw exception(sstream() << "file '" << fname << "' has been corrupted, checksum mismatch"); + unsigned computed_hash = hash(code_size, [&](unsigned i) { return code[i]; }); + if (claimed_hash != computed_hash) + throw exception(sstream() << "file '" << fname << "' has been corrupted, checksum mismatch"); - module_info_ptr r = std::make_shared(); - r->m_fname = fname; - r->m_counter = imports.size(); - r->m_module_idx = g_null_module_idx; - m_import_counter++; - std::string new_base = dirname(fname.c_str()); - std::swap(r->m_obj_code, code); - for (auto i : imports) { - auto d = load_module_file(new_base, i); - d->m_dependents.push_back(r); + module_info_ptr r = std::make_shared(); + r->m_fname = fname; + r->m_counter = imports.size(); + r->m_module_idx = g_null_module_idx; + m_import_counter++; + std::string new_base = dirname(fname.c_str()); + std::swap(r->m_obj_code, code); + for (auto i : imports) { + auto d = load_module_file(new_base, i); + d->m_dependents.push_back(r); + } + m_module_info.insert(fname, r); + r->m_module_idx = m_next_module_idx++; + + if (imports.empty()) + add_import_module_task(r); + return r; + } catch (corrupted_stream_exception&) { + throw corrupted_file_exception(fname); } - m_module_info.insert(fname, r); - r->m_module_idx = m_next_module_idx++; - - if (imports.empty()) - add_import_module_task(r); - - return r; } void add_asynch_task(asynch_update_fn const & f) { diff --git a/src/library/module.h b/src/library/module.h index ed6fe1c3c..fff16a638 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -14,6 +14,11 @@ Author: Leonardo de Moura #include "library/io_state.h" namespace lean { +class corrupted_file_exception : public exception { +public: + corrupted_file_exception(std::string const & fname); +}; + class module_name { optional m_relative; name m_name; diff --git a/src/library/resolve_macro.cpp b/src/library/resolve_macro.cpp index d71d9bb55..ebcf18e2b 100644 --- a/src/library/resolve_macro.cpp +++ b/src/library/resolve_macro.cpp @@ -293,7 +293,7 @@ static register_macro_deserializer_fn resolve_macro_des_fn(g_resolve_opcode, [](deserializer &, unsigned num, expr const * args) { if (num != 3) - throw_corrupted_file(); + throw corrupted_stream_exception(); return mk_resolve_macro(args[0], args[1], args[2]); }); diff --git a/src/library/string.cpp b/src/library/string.cpp index 31fdd704f..f7f895764 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -92,7 +92,7 @@ static register_macro_deserializer_fn string_macro_des_fn(g_string_opcode, [](deserializer & d, unsigned num, expr const *) { if (num != 0) - throw_corrupted_file(); + throw corrupted_stream_exception(); std::string v = d.read_string(); return mk_string_macro(v); }); diff --git a/src/util/name.cpp b/src/util/name.cpp index b75a01002..41ab6e5ae 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -449,7 +449,7 @@ public: name prefix = read(); return name(prefix, d.read_unsigned()); }} - throw_corrupted_file(); + throw corrupted_stream_exception(); }); } }; diff --git a/src/util/object_serializer.h b/src/util/object_serializer.h index 34b5a8e10..3354872eb 100644 --- a/src/util/object_serializer.h +++ b/src/util/object_serializer.h @@ -61,7 +61,7 @@ public: } else { unsigned i = d.read_unsigned(); if (i >= m_table.size()) - throw_corrupted_file(); + throw corrupted_stream_exception(); return m_table[i]; } } diff --git a/src/util/serializer.cpp b/src/util/serializer.cpp index 90db9921b..da3283d49 100644 --- a/src/util/serializer.cpp +++ b/src/util/serializer.cpp @@ -27,9 +27,8 @@ void serializer_core::write_int(int i) { #define BIG_BUFFER 1024 -void throw_corrupted_file() { - throw exception("corrupted binary file"); -} +corrupted_stream_exception::corrupted_stream_exception(): + exception("corrupted binary file") {} void serializer_core::write_double(double d) { std::ostringstream out; @@ -49,7 +48,7 @@ std::string deserializer_core::read_string() { if (c == 0) break; if (c == EOF) - throw_corrupted_file(); + throw corrupted_stream_exception(); r += c; } return r; diff --git a/src/util/serializer.h b/src/util/serializer.h index 66807c2b4..080c5885f 100644 --- a/src/util/serializer.h +++ b/src/util/serializer.h @@ -66,7 +66,10 @@ inline deserializer & operator>>(deserializer & d, char & c) { c = d.read_char() inline deserializer & operator>>(deserializer & d, bool & b) { b = d.read_bool(); return d; } inline deserializer & operator>>(deserializer & d, double & b) { b = d.read_double(); return d; } -[[ noreturn ]] void throw_corrupted_file(); +class corrupted_stream_exception : public exception { +public: + corrupted_stream_exception(); +}; template serializer & write_list(serializer & s, list const & ls) { diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index 5f150b5b3..3d13ad23f 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -357,7 +357,7 @@ public: sexpr t = read(); return sexpr(h, t); }} - throw_corrupted_file(); + throw corrupted_stream_exception(); }); } };