Segfault on OpenBSD #6902
Comments
|
it doesn't repro for me (but not on your arch/opsys). What is your architecture? Specifically pointer alignment may be at stake. |
This is on amd64. |
|
Here’s a minimal reproducer. This input crashes with the same backtrace: |
|
The reproducer does not crash on my side. It did exhibit an issue with the parser. It should have failed earlier when reading the ")". This was fixed. I have to suspect there is an issue specific with respect to the toolchain you are using. |
|
While that’s possible, in my experience it’s more likely to be OpenBSD’s strong malloc catching some hidden memory corruption. Of course, I can’t guarantee that’s the case (though it’s at least consistent with its failure to crash on your end). The latest git prints out an error for |
|
The asan heap sanitizer does not suggest any memory corruptions. |
|
I can confirm that 4.13.0 does crashes on OpenBSD current/amd64 with similar stacktrace: with very trivial input: which I run as |
|
@NikolajBjorner I think that this issue should be reoppened. I can easy reproduce it, and if I build z3 without optimization, it simple works. Here a good example of an issue with similar symptopms: yrutschle/sslh#270 |
|
@catap did you try building Z3 with ASAN or UBSAN? |
|
@intrigus-lgtm I had build it as simple as |
|
These smells of an alignment bug. Either z3 or the compiler (yes it happens sometimes). |
|
@NikolajBjorner I just rebuild z3 with using clang-13 instead of clang-16 and it had crashed the same way. |
|
@NikolajBjorner meanwhile, when I build z3 without any optimization ( with stack trace: |
|
and that's interesting python API on the same theoreme on the same build works fine: |
This would be platform specific. It doesn't reproduce on other platforms. |
|
@NikolajBjorner if you may give any advice how to track such issue, I willing to invest some time. I've tried As other solution you may virtual machine. I may run for you VM with OpenBSD, or you may run it inside Github CI by this method: https://github.com/catap/shell |
|
I checked about OpenBSD yesterday. Yes, a VM setup appears to be the way to go for local use. I use wsl2 where only ubuntu (debian/arch/alpine) appear handy and setting up these other environments tends to take quite some time on my side (mainly due to my limited skillsets when it comes to using tools effectively). The basic culprit was in the past our custom vector class: util/vector.h Line 183 in f6dbaee Since unsigned is 4 bytes, a 16 byte alignment requirement could break things, but then alignof would lie or be the incorrect way to ensure validity of alignment. Your stacks use constructors that use the vector class so there is some plausible correlation. |
|
Another takeaway from this may be that I create another GitHub action: https://github.com/vmactions/openbsd-vm for building z3. |
Well, I can make for you a VM with SSH access with z3, git and cmake / ninja. |
|
@NikolajBjorner I think this is different things. It's crashed on the first call of diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index 2be2ace58..1cfd731ef 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
b/src/smt/tactic/smt_tactic_core.cpp
@@ -41,7 41,7 @@ class smt_tactic : public tactic {
smt_params m_params;
params_ref m_params_ref;
expr_ref_vector m_vars;
- statistics m_stats;
// statistics m_stats;
smt::kernel* m_ctx = nullptr;
symbol m_logic;
progress_callback* m_callback = nullptr;
@@ -100,17 100,17 @@ public:
void collect_statistics(statistics & st) const override {
- if (m_ctx)
- m_ctx->collect_statistics(st); // ctx is still running...
- else
- st.copy(m_stats);
// if (m_ctx)
// m_ctx->collect_statistics(st); // ctx is still running...
// else
// st.copy(m_stats);
}
void cleanup() override {
}
void reset_statistics() override {
- m_stats.reset();
// m_stats.reset();
}
void set_logic(symbol const & l) override {
@@ -210,11 210,11 @@ public:
}
catch(...) {
TRACE("smt_tactic", tout << "exception\n";);
- m_ctx->collect_statistics(m_stats);
// m_ctx->collect_statistics(m_stats);
throw;
}
SASSERT(m_ctx);
- m_ctx->collect_statistics(m_stats);
// m_ctx->collect_statistics(m_stats);
proof_ref pr(m_ctx->get_proof(), m);
TRACE("smt_tactic", tout << r << " " << pr << "\n";);
switch (r) {it fails on almost the same time, but on different field: Something very odd here. |
|
Can you disassemble the instructions around the crashing pc? |
|
@intrigus-lgtm thanks for suggestion. With and without diff from #6902 (comment) it crashes on the same place / function which looks like: |
|
BTW this is |
|
Here a some how similar issue llvm/llvm-project#89341 |
|
Well, I just tried gcc, and it builds z3 which works. |
|
and for comparing dissasembled output for As you may see here no Yes, it defently smells like padding or alignment issue. |
|
Quite probably that it is this clang issue: llvm/llvm-project#55844 |
Signed-off-by: Nikolaj Bjorner <[email protected]>
|
You can try to change the #if in util/vector.h to check if removing the dirty trick with memory helps. |
|
@NikolajBjorner a3eb2ff crashes the same way. |
|
I think you need the commit before that. |
|
@NikolajBjorner well, something here quite wrong. I just tried a1bcf13 and it works very long. Long mean minutes, like ten, before I interrupt it. Inside gdb I see that it iterates inside |
I might have some time while waiting for some unrelated |
|
@intrigus-lgtm feel free to connect to This is today's snapshot of OpenBSD 7.6-beta. Inside home of catap user you may |
|
Okay, this was a fun bug :)
To fix:
|
|
Thanks for the thorough analysis! |
|
@NikolajBjorner : we can't do better than your fix, I'm afraid. Because deallocate() doesn't know the type that was allocated, so it always has to lookup for a fixed offset. |
|
I doubt that issue is closed. I just tried 6086a30 on provided VM and it crashes as: |
Obviously :D My analysis regarding openbsd missing in z3/src/util/memory_manager.cpp Lines 23 to 25 in ef58376 |
@NikolajBjorner I think you missed a case here: z3/src/util/memory_manager.cpp Line 325 in db4176a the |
|
reopen until missing use of SIZE_T_ALIGN is checked. |
|
@NikolajBjorner if you have some tests which can be used to confirm that it's ok, I willing to help to run it on OpenBSD. Anyway, a models in |
|
We have tests in several of the existing pipelines. ./test-z3 -a And run the files in z3test/regressions/smt2 repository. |
no crash
run as: no crash here as well. |
|
together with the usual BVT CI passing, I would declare this as settled. |
|
FYI: the next release of OpenBSD (7.6) contains patches which we had discussed on this PR make z3 quite usefull on that platfrom. |
The following testcase from Symbiyosys (executed with
z3 -smt2 -in) crashes on OpenBSD -current.Backtrace:
This crash occurs with both the 4.12.2 release and git master (e718bb6).
The text was updated successfully, but these errors were encountered: