-
Notifications
You must be signed in to change notification settings - Fork 463
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
one more misalignment #24
Changes from all commits
f36107a
8dd58ef
f2c529c
4549e8f
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -28,6 +28,12 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich | |
#include "library/time_task.h" | ||
#include "library/util.h" | ||
|
||
#if defined(__has_feature) | ||
#if __has_feature(address_sanitizer) | ||
#include <sanitizer/lsan_interface.h> | ||
#endif | ||
#endif | ||
|
||
namespace lean { | ||
// manually padded to multiple of word size, see `initialize_module` | ||
static char const * g_olean_header = "oleanfile!!!!!!!"; | ||
|
@@ -82,6 +88,12 @@ extern "C" object * lean_read_module_data(object * fname, object * w) { | |
in.close(); | ||
/* We don't free compacted_region objects */ | ||
compacted_region * region = new compacted_region(size - header_size, buffer); | ||
#if defined(__has_feature) | ||
#if __has_feature(address_sanitizer) | ||
// do not report as leak | ||
__lsan_ignore_object(region); | ||
#endif | ||
#endif | ||
object * mod = region->read(); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What is this? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Added a comment. I'd like to add sanitized builds to our CI in the future so that we immediately become aware of such problems. |
||
return set_io_result(w, mod); | ||
} catch (exception & ex) { | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -14,6 +14,16 @@ Author: Leonardo de Moura | |
namespace lean { | ||
#define TERMINATOR_ID (static_cast<unsigned>(object_kind::External) + 1) | ||
|
||
// special object that terminates the data block constructing the object graph rooted in `m_value` | ||
struct terminator_object : public object { | ||
object * m_value; | ||
|
||
explicit terminator_object(object * value) : object(object_kind::External, object_memory_kind::Region), m_value(value) { | ||
// not an actual `object_kind`, so write to the field directly | ||
m_kind = TERMINATOR_ID; | ||
} | ||
}; | ||
|
||
object_compactor::object_compactor(): | ||
m_begin(malloc(LEAN_COMPACTOR_INIT_SZ)), | ||
m_end(m_begin), | ||
|
@@ -60,11 +70,8 @@ object_offset object_compactor::to_offset(object * o) { | |
} | ||
|
||
void object_compactor::insert_terminator(object * o) { | ||
void * mem = alloc(sizeof(object) + sizeof(object*)); | ||
object * r = new (mem) object(object_kind::External, object_memory_kind::Region); | ||
r->m_kind = TERMINATOR_ID; | ||
object** ptr = reinterpret_cast<object**>(reinterpret_cast<char*>(r) + sizeof(object)); | ||
*ptr = to_offset(o); | ||
void * mem = alloc(sizeof(terminator_object)); | ||
new (mem) terminator_object(to_offset(o)); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why do we need this modification? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The old There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I see, There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, exactly |
||
} | ||
|
||
object * object_compactor::copy_object(object * o) { | ||
|
@@ -296,8 +303,8 @@ object * compacted_region::read() { | |
lean_assert(static_cast<char*>(m_next) + sizeof(object) <= m_end); | ||
object * curr = reinterpret_cast<object*>(m_next); | ||
if (curr->m_kind == TERMINATOR_ID) { | ||
object * r = *reinterpret_cast<object**>(static_cast<char*>(m_next) + sizeof(object)); | ||
move(sizeof(object) + sizeof(object*)); | ||
object * r = reinterpret_cast<terminator_object*>(m_next)->m_value; | ||
move(sizeof(terminator_object)); | ||
return fix_object_ptr(r); | ||
} else { | ||
switch (get_kind(curr)) { | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@leodemoura It's not clear to me why this one doesn't hold
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I will take a look. What is it holding before?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't know
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I investigated this issue. This assertion does not hold anymore.
A few months ago, I added the following function that combines
csimp
,cse
and deadlet
elimination in a loop until no further simplifications are possible. I reuse the simplifier object. Thus, an expression may be top-level and have already been simplified in the previous iteration.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
https://github.com/leanprover/lean4/blob/master/src/library/compiler/csimp.cpp#L2001