diff --git a/src/library/module.cpp b/src/library/module.cpp index 445a47fa0e..04566c164b 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -188,8 +188,8 @@ deserializer & operator>>(deserializer & d, module_name & r) { return d; } -static unsigned olean_hash(const char * data, unsigned size) { - return hash(size, [&] (unsigned i) { return static_cast(data[i]); }); +static unsigned olean_hash(std::string const & data) { + return hash(data.size(), [&] (unsigned i) { return static_cast(data[i]); }); } void write_module(loaded_module const & mod, std::ostream & out) { @@ -203,20 +203,26 @@ void write_module(loaded_module const & mod, std::ostream & out) { } s1 << g_olean_end_file; - serializer s2(out); + if (!out1.good()) { + throw exception(sstream() << "error during serialization of '" << mod.m_module_name << "'"); + } + std::string r = out1.str(); - unsigned h = olean_hash(r.data(), r.size()); - s2 << g_olean_header << LEAN_VERSION_MAJOR << LEAN_VERSION_MINOR << LEAN_VERSION_PATCH; + unsigned h = olean_hash(r); + + unsigned major = LEAN_VERSION_MAJOR, minor = LEAN_VERSION_MINOR, patch = LEAN_VERSION_PATCH; + bool uses_sorry = get(mod.m_uses_sorry); + + serializer s2(out); + s2 << g_olean_header << major << minor << patch; s2 << h; - s2 << static_cast(get(mod.m_uses_sorry)); + s2 << uses_sorry; // store imported files s2 << static_cast(mod.m_imports.size()); for (auto m : mod.m_imports) s2 << m; // store object code - s2.write_unsigned(r.size()); - for (unsigned i = 0; i < r.size(); i++) - s2.write_char(r[i]); + s2.write_blob(r); } static task has_sorry(modification_list const & mods) { @@ -485,9 +491,7 @@ environment add_inductive(environment env, olean_data parse_olean(std::istream & in, std::string const & file_name, bool check_hash) { unsigned major, minor, patch, claimed_hash; - unsigned code_size; std::vector imports; - std::vector code; bool uses_sorry; deserializer d1(in, optional(file_name)); @@ -507,9 +511,7 @@ olean_data parse_olean(std::istream & in, std::string const & file_name, bool ch imports.push_back(r); } - code_size = d1.read_unsigned(); - code.resize(code_size); - d1.read(code); + auto code = d1.read_blob(); if (!in.good()) { throw exception(sstream() << "file '" << file_name << "' has been corrupted"); @@ -517,7 +519,7 @@ olean_data parse_olean(std::istream & in, std::string const & file_name, bool ch // if (m_senv.env().trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL) { if (check_hash) { - unsigned computed_hash = olean_hash(code.data(), code_size); + unsigned computed_hash = olean_hash(code); if (claimed_hash != computed_hash) throw exception(sstream() << "file '" << file_name << "' has been corrupted, checksum mismatch"); } @@ -597,10 +599,9 @@ std::shared_ptr cache_preimported_env( return lm; } -modification_list parse_olean_modifications(std::vector const & olean_code, std::string const & file_name) { +modification_list parse_olean_modifications(std::string const & olean_code, std::string const & file_name) { modification_list ms; - std::string s(olean_code.data(), olean_code.size()); - std::istringstream in(s, std::ios_base::binary); + std::istringstream in(olean_code, std::ios_base::binary); scoped_expr_caching enable_caching(false); deserializer d(in, optional(file_name)); object_readers & readers = get_object_readers(); diff --git a/src/library/module.h b/src/library/module.h index 06f012610c..607c930435 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -94,11 +94,11 @@ std::shared_ptr cache_preimported_env( struct olean_data { std::vector m_imports; - std::vector m_serialized_modifications; + std::string m_serialized_modifications; bool m_uses_sorry; }; olean_data parse_olean(std::istream & in, std::string const & file_name, bool check_hash = true); -modification_list parse_olean_modifications(std::vector const & serialized_modifications, std::string const & file_name); +modification_list parse_olean_modifications(std::string const & serialized_modifications, std::string const & file_name); void import_module(modification_list const & modifications, std::string const & file_name, environment & env); struct modification { diff --git a/src/util/serializer.cpp b/src/util/serializer.cpp index bb0ee34935..8e6f93b5b2 100644 --- a/src/util/serializer.cpp +++ b/src/util/serializer.cpp @@ -102,8 +102,15 @@ double deserializer_core::read_double() { return r; } -void deserializer_core::read(std::vector & data) { - unsigned sz = data.size(); - m_in.read(data.data(), sz); +void serializer_core::write_blob(std::string const & s) { + write_unsigned(s.size()); + m_out.write(&s[0], s.size()); +} + +std::string deserializer_core::read_blob() { + unsigned sz = read_unsigned(); + std::string s(sz, '\0'); + m_in.read(&s[0], sz); + return s; } } diff --git a/src/util/serializer.h b/src/util/serializer.h index 1bc00322ce..4bff30ad92 100644 --- a/src/util/serializer.h +++ b/src/util/serializer.h @@ -27,13 +27,14 @@ class serializer_core { public: serializer_core(std::ostream & out):m_out(out) {} void write_string(char const * str) { m_out.write(str, strlen(str) + 1); } - void write_string(std::string const & str) { m_out.write(str.c_str(), str.size() + 1); } + void write_string(std::string const & str) { write_string(str.c_str()); } void write_unsigned(unsigned i); void write_uint64(uint64 i); void write_int(int i); void write_char(char c) { m_out.put(c); } void write_bool(bool b) { m_out.put(b ? 1 : 0); } void write_double(double b); + void write_blob(std::string const &); }; typedef extensible_object serializer; @@ -70,8 +71,7 @@ public: char read_char() { return m_in.get(); } bool read_bool() { return m_in.get() != 0; } double read_double(); - // read data.size() bytes from input stream and store it at data - void read(std::vector & data); + std::string read_blob(); optional get_fname() const { return m_fname; } };