@@ -46,6 +46,31 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
4646
4747namespace lean {
4848
49+ /* * Trivial RAII wrapper for file descriptors so we don't have to worry about `close` management. */
50+ class file_descriptor {
51+ private:
52+ int m_fd;
53+ public:
54+ explicit file_descriptor (int fd) : m_fd(fd) {}
55+
56+ // It should not be copyable
57+ file_descriptor (const file_descriptor&) = delete ;
58+ file_descriptor& operator =(const file_descriptor&) = delete ;
59+
60+ file_descriptor (file_descriptor&& other) noexcept : m_fd(other.m_fd) {
61+ other.m_fd = -1 ;
62+ }
63+
64+ ~file_descriptor () {
65+ if (m_fd != -1 ) {
66+ close (m_fd);
67+ }
68+ }
69+
70+ int get () const { return m_fd; }
71+ operator bool () const { return m_fd != -1 ; }
72+ };
73+
4974/* * On-disk format of a .olean file. */
5075struct olean_header {
5176 // 5 bytes: magic number
@@ -169,7 +194,7 @@ extern "C" LEAN_EXPORT object * lean_save_module_data_parts(b_obj_arg mod, b_obj
169194
170195struct module_file {
171196 std::string m_fname;
172- std::ifstream m_in ;
197+ file_descriptor m_fd ;
173198 char * m_base_addr;
174199 size_t m_size;
175200 char * m_buffer;
@@ -184,22 +209,25 @@ extern "C" LEAN_EXPORT object * lean_read_module_data_parts(b_obj_arg ofnames, o
184209 for (auto const & fname : fnames) {
185210 std::string olean_fn = fname.to_std_string ();
186211 try {
187- std::ifstream in ( olean_fn, std::ios_base::binary );
188- if (in. fail () ) {
189- return io_result_mk_error ((sstream () << " failed to open file '" << olean_fn << " '" ).str ());
212+ file_descriptor fd ( open ( olean_fn. c_str (), O_RDONLY) );
213+ if (!fd ) {
214+ return io_result_mk_error ((sstream () << " failed to open file '" << olean_fn << " ': " << strerror (errno) ).str ());
190215 }
216+
191217 /* Get file size */
192- in.seekg (0 , in.end );
193- size_t size = in.tellg ();
194- in.seekg (0 );
218+ struct stat st;
219+ if (fstat (fd.get (), &st) == -1 ) {
220+ return io_result_mk_error ((sstream () << " failed to stat file '" << olean_fn << " ': " << strerror (errno)).str ());
221+ }
222+ size_t size = st.st_size ;
195223
196224 olean_header default_header = {};
197225 olean_header header;
198- if (!in. read (reinterpret_cast < char *>( &header) , sizeof (header))
226+ if (read (fd. get (), &header, sizeof (header)) != sizeof (header )
199227 || memcmp (header.marker , default_header.marker , sizeof (header.marker )) != 0 ) {
200228 return io_result_mk_error ((sstream () << " failed to read file '" << olean_fn << " ', invalid header" ).str ());
201229 }
202- in. seekg ( 0 );
230+ lseek (fd. get (), 0 , SEEK_SET );
203231 if (header.version != default_header.version || header.flags != default_header.flags
204232#ifdef LEAN_CHECK_OLEAN_VERSION
205233 || strncmp (header.githash , LEAN_GITHASH, sizeof (header.githash )) != 0
@@ -208,7 +236,7 @@ extern "C" LEAN_EXPORT object * lean_read_module_data_parts(b_obj_arg ofnames, o
208236 return io_result_mk_error ((sstream () << " failed to read file '" << olean_fn << " ', incompatible header" ).str ());
209237 }
210238 char * base_addr = reinterpret_cast <char *>(header.base_addr );
211- files.push_back ({olean_fn, std::move (in ), base_addr, size, nullptr , nullptr });
239+ files.push_back ({olean_fn, std::move (fd ), base_addr, size, nullptr , nullptr });
212240 } catch (exception & ex) {
213241 return io_result_mk_error ((sstream () << " failed to read '" << olean_fn << " ': " << ex.what ()).str ());
214242 }
@@ -244,16 +272,13 @@ extern "C" LEAN_EXPORT object * lean_read_module_data_parts(b_obj_arg ofnames, o
244272 lean_always_assert (UnmapViewOfFile (base_addr));
245273 };
246274#else
247- int fd = open (olean_fn.c_str (), O_RDONLY);
248- if (fd == -1 ) {
249- return io_result_mk_error ((sstream () << " failed to open '" << olean_fn << " ': " << strerror (errno)).str ());
250- }
275+ int fd = file.m_fd .get ();
276+ // NOTE: `file.m_fd` does NOT need to outlive `buffer` after this call
251277 char * buffer = static_cast <char *>(mmap (base_addr, file.m_size , PROT_READ, MAP_PRIVATE, fd, 0 ));
252278 if (buffer == MAP_FAILED) {
253279 is_mmap = false ;
254280 break ;
255281 }
256- close (fd);
257282 size_t size = file.m_size ;
258283 file.m_free_data = [=]() {
259284 lean_always_assert (munmap (buffer, size) == 0 );
@@ -287,11 +312,9 @@ extern "C" LEAN_EXPORT object * lean_read_module_data_parts(b_obj_arg ofnames, o
287312 std::string const & olean_fn = file.m_fname ;
288313 try {
289314 file.m_buffer = big_buffer + (file.m_base_addr - files[0 ].m_base_addr );
290- file.m_in .read (file.m_buffer , file.m_size );
291- if (!file.m_in ) {
315+ if (read (file.m_fd .get (), file.m_buffer , file.m_size ) != file.m_size ) {
292316 return io_result_mk_error ((sstream () << " failed to read file '" << olean_fn << " '" ).str ());
293317 }
294- file.m_in .close ();
295318 } catch (exception & ex) {
296319 return io_result_mk_error ((sstream () << " failed to read '" << olean_fn << " ': " << ex.what ()).str ());
297320 }
0 commit comments