one more misalignment #24

Kha · 2019-07-30T15:18:27Z

No description provided.

Kha · 2019-07-30T15:18:57Z

src/library/compiler/csimp.cpp

@@ -1136,7 +1136,6 @@ class csimp_fn {
    expr visit_lambda(expr e, bool is_join_point_def, bool top) {
        lean_assert(is_lambda(e));
        lean_assert(!top || m_fvars.size() == 0);
-        lean_assert(!top || !already_simplified(e));


@leodemoura It's not clear to me why this one doesn't hold

I will take a look. What is it holding before?

I don't know

I investigated this issue. This assertion does not hold anymore.
A few months ago, I added the following function that combines csimp, cse and dead let 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.

https://github.com/leanprover/lean4/blob/master/src/library/compiler/csimp.cpp#L2001

leodemoura · 2019-07-30T15:28:10Z

src/library/module.cpp

@@ -82,6 +86,9 @@ 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) && __has_feature(address_sanitizer)
+        __lsan_ignore_object(region);
+#endif
        object * mod = region->read();


What is this?

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.

leodemoura · 2019-07-30T15:29:24Z

src/runtime/compact.cpp

-    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));


Why do we need this modification?

The old ptr was misaligned. Using a struct for the two datums implicitly fixes the alignment.

I see, sizeof(object) was not a multiple of 8, right?

Yes, exactly

leodemoura · 2019-07-31T01:44:04Z

merged

…er#24)

@Kha

Mathlib is crashing with #4006. Here is the stacktrace produced by Kim: ``` * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x100000000000a) * frame #0: 0x00000001066db21c libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 2816 frame #1: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #2: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #3: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #4: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #5: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #6: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #7: 0x00000001066df288 libleanshared.dylib`lean::ir::interpreter::stub_m(lean_object**) + 556 frame #8: 0x00000001066d6ee0 libleanshared.dylib`lean_object* lean::ir::interpreter::with_interpreter<lean_object*>(lean::environment const&, lean::options const&, lean::name const&, std::__1::function<lean_object* (lean::ir::interpreter&)> const&) + 320 frame #9: 0x00000001066dee84 libleanshared.dylib`lean::ir::interpreter::stub_m_aux(lean_object**) + 92 frame #10: 0x00000001066deafc libleanshared.dylib`lean::ir::interpreter::stub_9_aux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*) + 60 frame #11: 0x00000001066f52a0 libleanshared.dylib`lean_apply_6 + 1748 frame #12: 0x00000001055d1ac8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2 + 156 frame #13: 0x00000001055d47e8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2___boxed + 144 frame #14: 0x00000001066f5bcc libleanshared.dylib`lean_apply_7 + 1348 frame #15: 0x00000001055ccccc libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__4 + 528 frame #16: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252 frame #17: 0x00000001055d1550 libleanshared.dylib`l_Lean_Elab_withLogging___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__6 + 240 frame #18: 0x00000001055d4cb4 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10 + 940 frame #19: 0x00000001055d5394 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1 + 60 frame #20: 0x00000001055d5740 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1___boxed + 148 frame #21: 0x00000001066f11f4 libleanshared.dylib`lean_apply_1 + 840 frame #22: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24 frame #23: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20 frame #24: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528 frame #25: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128 frame #26: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112 frame #27: 0x00000001055d564c libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore + 268 frame #28: 0x00000001055d6264 libleanshared.dylib`l_Lean_Elab_Term_applyAttributes + 52 frame #29: 0x000000010597b840 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1 + 740 frame #30: 0x000000010597daf4 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1___boxed + 124 frame #31: 0x00000001066f65d8 libleanshared.dylib`lean_apply_8 + 1252 frame #32: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252 frame #33: 0x0000000104f587b0 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg___lambda__1 + 344 frame #34: 0x0000000104f59ec4 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg + 280 frame #35: 0x0000000104f5af20 libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1 + 144 frame #36: 0x00000001066f5ab8 libleanshared.dylib`lean_apply_7 + 1072 frame #37: 0x0000000105636090 libleanshared.dylib`l_Lean_Elab_Term_TermElabM_run___rarg + 844 frame #38: 0x0000000104f5b8fc libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg + 1696 frame #39: 0x000000010597d67c libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6 + 928 frame #40: 0x000000010597de60 libleanshared.dylib`l_Lean_Elab_Command_elabAttr + 772 frame #41: 0x000000010597e838 libleanshared.dylib`l_Lean_Elab_Command_elabAttr___boxed + 20 frame #42: 0x00000001066f2cd4 libleanshared.dylib`lean_apply_3 + 868 frame #43: 0x0000000104f385f8 libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__2 + 396 frame #44: 0x0000000104f39e48 libleanshared.dylib`l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing + 484 frame #45: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896 frame #46: 0x0000000104f341d4 libleanshared.dylib`l_Lean_withTraceNode___at_Lean_Elab_Command_runLinters___spec__11 + 788 frame #47: 0x00000001066f2d54 libleanshared.dylib`lean_apply_3 + 996 frame #48: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896 frame #49: 0x0000000104f40e30 libleanshared.dylib`l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2 + 104 frame #50: 0x0000000104f4c51c libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel___lambda__1 + 432 frame #51: 0x00000001066f10e8 libleanshared.dylib`lean_apply_1 + 572 frame #52: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24 frame #53: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20 frame #54: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528 frame #55: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128 frame #56: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112 frame #57: 0x0000000104f4fce0 libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel + 1284 frame #58: 0x00000001057d2f30 libleanshared.dylib`l_Lean_Elab_Frontend_elabCommandAtFrontend + 1384 frame #59: 0x00000001057d63b8 libleanshared.dylib`l_Lean_Elab_Frontend_processCommand + 1332 frame #60: 0x00000001057d6e48 libleanshared.dylib`l_Lean_Elab_Frontend_processCommands + 72 frame #61: 0x00000001057d7248 libleanshared.dylib`l_Lean_Elab_IO_processCommands + 212 frame #62: 0x00000001057d83d0 libleanshared.dylib`l_Lean_Elab_runFrontend___lambda__3 + 76 frame #63: 0x00000001057d96d0 libleanshared.dylib`lean_run_frontend + 2436 frame #64: 0x00000001065e72b4 libleanshared.dylib`lean::run_new_frontend(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::options const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::name const&, unsigned int, lean::optional<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>>> const&, unsigned char) + 244 frame #65: 0x00000001065e9c8c libleanshared.dylib`lean_main + 8348 frame #66: 0x0000000184f93f28 dyld`start + 2236 ``` cc @Kha

@Kha

Mathlib is crashing with #4006. Here is the stacktrace produced by Kim: ``` * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x100000000000a) * frame #0: 0x00000001066db21c libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 2816 frame #1: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #2: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #3: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #4: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #5: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #6: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #7: 0x00000001066df288 libleanshared.dylib`lean::ir::interpreter::stub_m(lean_object**) + 556 frame #8: 0x00000001066d6ee0 libleanshared.dylib`lean_object* lean::ir::interpreter::with_interpreter<lean_object*>(lean::environment const&, lean::options const&, lean::name const&, std::__1::function<lean_object* (lean::ir::interpreter&)> const&) + 320 frame #9: 0x00000001066dee84 libleanshared.dylib`lean::ir::interpreter::stub_m_aux(lean_object**) + 92 frame #10: 0x00000001066deafc libleanshared.dylib`lean::ir::interpreter::stub_9_aux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*) + 60 frame #11: 0x00000001066f52a0 libleanshared.dylib`lean_apply_6 + 1748 frame #12: 0x00000001055d1ac8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2 + 156 frame #13: 0x00000001055d47e8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2___boxed + 144 frame #14: 0x00000001066f5bcc libleanshared.dylib`lean_apply_7 + 1348 frame #15: 0x00000001055ccccc libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__4 + 528 frame #16: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252 frame #17: 0x00000001055d1550 libleanshared.dylib`l_Lean_Elab_withLogging___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__6 + 240 frame #18: 0x00000001055d4cb4 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10 + 940 frame #19: 0x00000001055d5394 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1 + 60 frame #20: 0x00000001055d5740 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1___boxed + 148 frame #21: 0x00000001066f11f4 libleanshared.dylib`lean_apply_1 + 840 frame #22: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24 frame #23: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20 frame #24: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528 frame #25: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128 frame #26: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112 frame #27: 0x00000001055d564c libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore + 268 frame #28: 0x00000001055d6264 libleanshared.dylib`l_Lean_Elab_Term_applyAttributes + 52 frame #29: 0x000000010597b840 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1 + 740 frame #30: 0x000000010597daf4 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1___boxed + 124 frame #31: 0x00000001066f65d8 libleanshared.dylib`lean_apply_8 + 1252 frame #32: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252 frame #33: 0x0000000104f587b0 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg___lambda__1 + 344 frame #34: 0x0000000104f59ec4 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg + 280 frame #35: 0x0000000104f5af20 libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1 + 144 frame #36: 0x00000001066f5ab8 libleanshared.dylib`lean_apply_7 + 1072 frame #37: 0x0000000105636090 libleanshared.dylib`l_Lean_Elab_Term_TermElabM_run___rarg + 844 frame #38: 0x0000000104f5b8fc libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg + 1696 frame #39: 0x000000010597d67c libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6 + 928 frame #40: 0x000000010597de60 libleanshared.dylib`l_Lean_Elab_Command_elabAttr + 772 frame #41: 0x000000010597e838 libleanshared.dylib`l_Lean_Elab_Command_elabAttr___boxed + 20 frame #42: 0x00000001066f2cd4 libleanshared.dylib`lean_apply_3 + 868 frame #43: 0x0000000104f385f8 libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__2 + 396 frame #44: 0x0000000104f39e48 libleanshared.dylib`l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing + 484 frame #45: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896 frame #46: 0x0000000104f341d4 libleanshared.dylib`l_Lean_withTraceNode___at_Lean_Elab_Command_runLinters___spec__11 + 788 frame #47: 0x00000001066f2d54 libleanshared.dylib`lean_apply_3 + 996 frame #48: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896 frame #49: 0x0000000104f40e30 libleanshared.dylib`l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2 + 104 frame #50: 0x0000000104f4c51c libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel___lambda__1 + 432 frame #51: 0x00000001066f10e8 libleanshared.dylib`lean_apply_1 + 572 frame #52: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24 frame #53: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20 frame #54: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528 frame #55: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128 frame #56: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112 frame #57: 0x0000000104f4fce0 libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel + 1284 frame #58: 0x00000001057d2f30 libleanshared.dylib`l_Lean_Elab_Frontend_elabCommandAtFrontend + 1384 frame #59: 0x00000001057d63b8 libleanshared.dylib`l_Lean_Elab_Frontend_processCommand + 1332 frame #60: 0x00000001057d6e48 libleanshared.dylib`l_Lean_Elab_Frontend_processCommands + 72 frame #61: 0x00000001057d7248 libleanshared.dylib`l_Lean_Elab_IO_processCommands + 212 frame #62: 0x00000001057d83d0 libleanshared.dylib`l_Lean_Elab_runFrontend___lambda__3 + 76 frame #63: 0x00000001057d96d0 libleanshared.dylib`lean_run_frontend + 2436 frame #64: 0x00000001065e72b4 libleanshared.dylib`lean::run_new_frontend(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::options const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::name const&, unsigned int, lean::optional<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>>> const&, unsigned char) + 244 frame #65: 0x00000001065e9c8c libleanshared.dylib`lean_main + 8348 frame #66: 0x0000000184f93f28 dyld`start + 2236 ``` cc @Kha

fix(runtime/compact): badly aligned "field" in terminator

f36107a

Kha commented Jul 30, 2019

View reviewed changes

leodemoura reviewed Jul 30, 2019

View reviewed changes

Kha force-pushed the master branch from 757988f to 8267ab4 Compare July 30, 2019 15:35

joehendrix mentioned this pull request Jul 30, 2019

Add LLVM optional dependency #21

Closed

Kha added 3 commits July 30, 2019 18:39

chore(library/module): lsan: ignore module objects

8dd58ef

chore(runtime/object): LEAN_FAKE_FREE: assert on double-free

f2c529c

chore(library/compiler/csimp): remove wrong assertion

4549e8f

Kha force-pushed the master branch from 8267ab4 to 4549e8f Compare July 30, 2019 16:39

leodemoura closed this Jul 31, 2019

ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this pull request Dec 2, 2022

feat(Logic/Function) port everything up to partial_inv_left (leanprov…

2ea02e9

…er#24)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

one more misalignment #24

one more misalignment #24

Kha commented Jul 30, 2019

Kha Jul 30, 2019

leodemoura Jul 30, 2019 •

edited

Loading

Kha Jul 30, 2019

leodemoura Jul 30, 2019

leodemoura Jul 30, 2019

leodemoura Jul 30, 2019

Kha Jul 30, 2019

leodemoura Jul 30, 2019

Kha Jul 30, 2019

leodemoura Jul 30, 2019

Kha Jul 30, 2019

leodemoura commented Jul 31, 2019

one more misalignment #24

one more misalignment #24

Conversation

Kha commented Jul 30, 2019

Choose a reason for hiding this comment

leodemoura Jul 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

leodemoura commented Jul 31, 2019

leodemoura Jul 30, 2019 •

edited

Loading