SIGBUS due to unaligned access #6015

arrowd · 2022-05-02T21:24:41Z

I'm running Z3 4.8.16 compiled with Clang 13 on FreeBSD 14. Z3 is being used as a library by the KLEE project. A lot of KLEE testcases fail for me due to SIGBUS inside libz3.so. Here are my findings:

(gdb) bt
#0  smt::theory_seq::solution_map::solution_map (m=..., dm=..., this=<optimized out>) at ../src/smt/theory_seq.h:107
#1  smt::theory_seq::theory_seq (this=0x20ae408, ctx=...) at ../src/smt/theory_seq.cpp:253
#2  0x0000000805893fcd in smt::setup::setup_seq_str (this=this@entry=0x21fcc98, st=...) at ../src/smt/smt_setup.cpp:909
#3  0x000000080588bc09 in smt::setup::setup_unknown (this=0x21fcc98, this@entry=0x21fccb0) at ../src/smt/smt_setup.cpp:960
#4  0x0000000805892b2b in smt::setup::setup_unknown (this=this@entry=0x21fcc98, st=...) at ../src/smt/smt_setup.cpp:1003
#5  0x000000080588cbaa in smt::setup::setup_auto_config (this=this@entry=0x21fcc98) at ../src/smt/smt_setup.cpp:205
#6  0x000000080588b8e8 in smt::setup::operator() (this=0x21fcc98, cm=smt::CFG_AUTO) at ../src/smt/smt_setup.cpp:66
#7  0x00000008055150e8 in smt::context::setup_context (this=0x21fcc08, use_static_features=<optimized out>) at ../src/smt/smt_context.cpp:3557
#8  0x00000008055131ce in smt::context::setup_and_check (this=0x21fcc08, reset_cancel=true) at ../src/smt/smt_context.cpp:3523
#9  0x00000008053c00ea in smt_tactic::operator() (this=<optimized out>, in=..., result=...) at ../src/smt/tactic/smt_tactic_core.cpp:207
#10 0x00000008060c3e9e in and_then_tactical::operator() (this=0x1e84a28, in=..., result=...) at ../src/tactic/tactical.cpp:121
#11 0x00000008060c3e9e in and_then_tactical::operator() (this=0x202f3e8, in=..., result=...) at ../src/tactic/tactical.cpp:121
#12 0x00000008060beccc in exec (t=..., in=..., result=...) at ../src/tactic/tactic.cpp:153
#13 0x00000008060befd9 in check_sat (t=..., g=..., md=..., labels=..., pr=..., core=..., reason_unknown=...) at ../src/tactic/tactic.cpp:173
#14 0x0000000806075790 in (anonymous namespace)::tactic2solver::check_sat_core2 (this=<optimized out>, num_assumptions=0, assumptions=<optimized out>) at ../src/solver/tactic2solver.cpp:229
#15 0x000000080607b072 in solver_na2as::check_sat_core (this=0x2011ba8, num_assumptions=<optimized out>, assumptions=<optimized out>) at ../src/solver/solver_na2as.cpp:67
#16 0x000000080606e2cb in combined_solver::check_sat_core (this=0x204db28, num_assumptions=<optimized out>, assumptions=0x0) at ../src/solver/combined_solver.cpp:252
#17 0x0000000806084e6e in solver::check_sat (this=0x204db28, num_assumptions=0, assumptions=0x0) at ../src/solver/solver.cpp:318
#18 0x0000000804ee7464 in _solver_check (c=c@entry=0xc12008, s=s@entry=0xbb4d88, num_assumptions=num_assumptions@entry=0, assumptions=assumptions@entry=0x0) at ../src/api/api_solver.cpp:599
#19 0x0000000804ee7203 in Z3_solver_check (c=0xc12008, s=0xbb4d88) at ../src/api/api_solver.cpp:627
#20 ...KLEE-related frames...

(gdb) disas
Dump of assembler code for function _ZN3smt10theory_seqC2ERNS_7contextE:
   0x00000008058a7ac0 <+0>:     push   %rbp
   0x00000008058a7ac1 <+1>:     mov    %rsp,%rbp
   0x00000008058a7ac4 <+4>:     push   %r15
   0x00000008058a7ac6 <+6>:     push   %r14
   0x00000008058a7ac8 <+8>:     push   %r13
   0x00000008058a7aca <+10>:    push   %r12
   0x00000008058a7acc <+12>:    push   %rbx
   0x00000008058a7acd <+13>:    sub    $0x78,%rsp
...
=> 0x00000008058a7b61 <+161>:   movaps %xmm0,0x80(%rbx)
...

The address being access is not aligned to 64:

(gdb) print $rbx+0x80
34268296

Let me know if I can provide more info to debug this.

The text was updated successfully, but these errors were encountered:

NikolajBjorner · 2022-05-03T16:01:29Z

I don't see where the code on the stack is associated with unaligned access.
It is in startup code that gets exercised on almost all code paths.

arrowd · 2022-05-04T14:40:59Z

Some more info. I reproduced this issue in test-z3:

* thread #1, name = 'test-z3', stop reason = signal SIGBUS: hardware error
  * frame #0: 0x0000000000be6d7c test-z3`smt::theory_seq::theory_seq(smt::context&) [inlined] vector<unsigned int, false, unsigned int>::vector() at vector.h:166:9
    frame #1: 0x0000000000be6d7c test-z3`smt::theory_seq::theory_seq(smt::context&) [inlined] svector<unsigned int, unsigned int>::svector() at vector.h:739:15
    frame #2: 0x0000000000be6d7c test-z3`smt::theory_seq::theory_seq(smt::context&) [inlined] smt::theory_seq::exclusion_table::exclusion_table(m=0x0000000821c27d70) at theory_seq.h:136:13
    frame #3: 0x0000000000be6cf8 test-z3`smt::theory_seq::theory_seq(this=0x0000000826ff7808, ctx=<unavailable>) at theory_seq.cpp:261:5
    frame #4: 0x0000000000bd3398 test-z3`smt::setup::setup_seq_str(this=0x0000000826fe1898, st=0x0000000821c27090) at smt_setup.cpp:0
    frame #5: 0x0000000000bce780 test-z3`smt::setup::setup_unknown(this=0x0000000826fe1898) at smt_setup.cpp:960:9
    frame #6: 0x0000000000bce64b test-z3`smt::setup::operator(this=0x0000000826fe1898, cm=<unavailable>)(smt::config_mode) at smt_setup.cpp:65:25
    frame #7: 0x0000000000bc6ec2 test-z3`smt::context::setup_context(this=0x0000000826fe1808, use_static_features=<unavailable>) at smt_context.cpp:3557:9
    frame #8: 0x0000000000bc68a6 test-z3`smt::context::check(this=0x0000000826fe1808, num_assumptions=0, assumptions=0x0000000000000000, reset_cancel=<unavailable>) at smt_context.cpp:3585:9
    frame #9: 0x00000000006a2122 test-z3`test_doc_cls::check_equiv(this=0x0000000821c27d68, fml1=0x0000000821c278c8, fml2=0x0000000821c278b8) at doc.cpp:343:28
    frame #10: 0x00000000006a27ea test-z3`test_doc_cls::test_project(this=0x0000000821c27d68, num_clauses=7) at doc.cpp:259:9
    frame #11: 0x000000000069cf0d test-z3`tst_doc() at doc.cpp:364:13
    frame #12: 0x000000000069cf00 test-z3`tst_doc() at doc.cpp:483:8
    frame #13: 0x000000000067cdbf test-z3`main(argc=2, argv=0x0000000821c28688) at main.cpp:163:5
    frame #14: 0x000000000055dce0 test-z3`_start(ap=<unavailable>, cleanup=<unavailable>) at crt1_c.c:73:7

And this is disassembly mapped to source lines:

(lldb) disas -l
test-z3`smt::theory_seq::theory_seq:
->  0xbe6d7c <+668>: movaps %xmm0, 0x390(%rbx)

   260      m_factory(nullptr),
   261      m_exclude(m),
** 262      m_axioms(m),
   263      m_axioms_head(0),
   264      m_int_string(m),

    0xbe6d83 <+675>: movq   0x18(%rbx), %rax

   51  
   52       ref_vector_core() = default;
** 53       ref_vector_core(Ref const & r) : Ref(r) {}
   54  
   55       ref_vector_core(const ref_vector_core & other) {

    0xbe6d87 <+679>: movq   %rax, 0x3a0(%rbx)

   164  #define SIZE_IDX     -1
   165  #define CAPACITY_IDX -2
** 166      T * m_data = nullptr;
   167 
   168      void destroy_elements() {

    0xbe6d8e <+686>: movq   $0x0, 0x3a8(%rbx)

I also found out that disabling optimization makes the bug go away. Could it be a miscompilation on the Clang side?

arrowd · 2022-05-04T14:43:56Z

Thinking about it, the xmm0 register is 16-byte wide, while T* is 8-byte on x86_64.

nunoplopes · 2022-05-10T16:34:58Z

Can you try replacing line 936 of src/smt/smt_setup.cpp with:

m_context.register_plugin(new smt::theory_seq(m_context));

Just wanted to test a theory.

arrowd · 2022-05-10T17:33:12Z

This changes the error message to:

<jemalloc>: jemalloc_jemalloc.c:2576: Failed assertion: "alloc_ctx.szind != SC_NSIZES"
Abort trap (core dumped)

This usually means memory corruption. Any hints what to do with this?

NikolajBjorner · 2022-05-10T17:49:08Z

~~Do you have incompatible libraries on your path?~~

(updated useless comment)

arrowd · 2022-05-10T17:50:34Z

What libraries exactly?

nunoplopes · 2022-05-10T17:51:11Z

This changes the error message to:
<jemalloc>: jemalloc_jemalloc.c:2576: Failed assertion: "alloc_ctx.szind != SC_NSIZES"
Abort trap (core dumped)
This usually means memory corruption. Any hints what to do with this?

Can you try without jemalloc? It may not be aligning the allocation sufficiently.
To debug memory corruptions, either use valgrind or compile with -fsanitize=address,undefined

arrowd · 2022-05-10T17:52:11Z

Can you try without jemalloc? It may not be aligning the allocation sufficiently.

I doubt it, it is a default malloc in FreeBSD libc. I'll try Clang sanitizers, then.

arrowd · 2022-05-10T18:00:26Z

The backtrace I get with debug build and 936 line patched:

<jemalloc>: jemalloc_arena.c:346: Failed assertion: "((uintptr_t)ptr - (uintptr_t)extent_addr_get(slab)) % (uintptr_t)bin_infos[binind].reg_size == 0"
(lldb) bt
* thread #1, name = 'test-z3', stop reason = signal SIGABRT
  * frame #0: 0x0000000827c7c4ea libc.so.7`__sys_thr_kill at thr_kill.S:4
    frame #1: 0x0000000827bf48f4 libc.so.7`__raise(s=6) at raise.c:52:10
    frame #2: 0x0000000827ca6259 libc.so.7`abort at abort.c:67:8
    frame #3: 0x0000000827ccd3c2 libc.so.7`arena_dalloc_bin_locked_impl(tsdn=<unavailable>, arena=<unavailable>, bin=<unavailable>, binind=<unavailable>, slab=<unavailable>, ptr=<unavailable>, junked=<unavailable>) at jemalloc_arena.c:0
    frame #4: 0x0000000827ccce34 libc.so.7`__je_arena_dalloc_bin_junked_locked(tsdn=<unavailable>, arena=<unavailable>, bin=<unavailable>, binind=<unavailable>, extent=<unavailable>, ptr=<unavailable>) at jemalloc_arena.c:1714:2
    frame #5: 0x0000000827d0cfa8 libc.so.7`__je_tcache_bin_flush_small(tsd=<unavailable>, tcache=0x00000008237d9280, tbin=<unavailable>, binind=29, rem=0) at jemalloc_tcache.c:189:5
    frame #6: 0x0000000827d0cadf libc.so.7`__je_tcache_event_hard(tsd=<unavailable>, tcache=0x00000008237d9280) at jemalloc_tcache.c:55:4
    frame #7: 0x0000000827cccd80 libc.so.7`arena_malloc [inlined] tcache_event(tsd=0x00000008237d9090, tcache=0x00000008237d9280) at tcache_inlines.h:37:3
    frame #8: 0x0000000827cccd6c libc.so.7`arena_malloc [inlined] tcache_alloc_small(tsd=<unavailable>, arena=<unavailable>, tcache=0x00000008237d9280, binind=<unavailable>, zero=false, slow_path=true) at tcache_inlines.h:99:2
    frame #9: 0x0000000827cccd6c libc.so.7`arena_malloc(tsdn=<unavailable>, arena=<unavailable>, size=<unavailable>, ind=<unavailable>, zero=<unavailable>, tcache=0x00000008237d9280, slow_path=true) at arena_inlines_b.h:165:11
    frame #10: 0x0000000827cce01e libc.so.7`__je_arena_ralloc [inlined] arena_ralloc_move_helper(tsdn=0x00000008237d9090, arena=0x0000000000000000, usize=48, alignment=<unavailable>, zero=false) at jemalloc_arena.c:1789:10
    frame #11: 0x0000000827ccdfc8 libc.so.7`__je_arena_ralloc(tsdn=0x00000008237d9090, arena=0x0000000000000000, ptr=<unavailable>, oldsize=16, size=<unavailable>, alignment=<unavailable>, zero=<unavailable>, tcache=0x00000008237d9280, hook_args=0x0000000822f3a8c8) at jemalloc_arena.c:1831:14
    frame #12: 0x0000000827cbbee2 libc.so.7`__realloc [inlined] iralloct(ptr=0x0000000828fbe370, oldsize=16, size=40, alignment=0, zero=false, tcache=0x00000008237d9280, arena=0x0000000000000000, hook_args=0x0000000822f3a8c8) at jemalloc_internal_inlines_c.h:192:9
    frame #13: 0x0000000827cbbe3b libc.so.7`__realloc [inlined] iralloc(ptr=<unavailable>, oldsize=16, size=40, alignment=0, zero=false, hook_args=0x0000000822f3a8c8) at jemalloc_internal_inlines_c.h:199:9
    frame #14: 0x0000000827cbbe12 libc.so.7`__realloc(ptr=<unavailable>, arg_size=<unavailable>) at jemalloc_jemalloc.c:2700:10
    frame #15: 0x0000000002b06f05 test-z3`memory::reallocate(p=0x0000000828fbe378, s=40) at memory_manager.cpp:366:15
    frame #16: 0x0000000002a667d8 test-z3`bit_vector::expand_to(this=0x0000000822f3b700, new_capacity=8) at bit_vector.cpp:29:29
    frame #17: 0x0000000002a66b17 test-z3`bit_vector::resize(this=0x0000000822f3b700, new_size=132, val=false) at bit_vector.cpp:47:9
    frame #18: 0x0000000002738340 test-z3`obj_mark<decl, bit_vector, ast_mark::decl2uint>::mark(this=0x0000000822f3b6f8, obj=0x000000082903b4e8, flag=true) at obj_mark.h:42:21
    frame #19: 0x00000000027338dc test-z3`obj_mark<decl, bit_vector, ast_mark::decl2uint>::mark(this=0x0000000822f3b6f8, obj=0x000000082903b4e8, flag=true) at obj_mark.h:46:43
    frame #20: 0x0000000002719c0e test-z3`ast_mark::mark(this=0x0000000822f3b6d8, n=0x000000082903b4e8, flag=true) at ast.cpp:3391:29
    frame #21: 0x000000000278d4c9 test-z3`static_features::mark_pre(this=0x0000000822f3b5b8, e=0x000000082903b4e8) at static_features.h:128:46
    frame #22: 0x0000000002789f23 test-z3`static_features::update_core(this=0x0000000822f3b5b8, e=0x0000000829018f58) at static_features.cpp:349:13
    frame #23: 0x000000000278aa54 test-z3`static_features::pre_process(this=0x0000000822f3b5b8, e=0x0000000829018f58, form_ctx=false, or_and_ctx=false, ite_ctx=false) at static_features.cpp:416:5
    frame #24: 0x000000000278b2c3 test-z3`static_features::process_all(this=0x0000000822f3b5b8) at static_features.cpp:543:14
    frame #25: 0x000000000278b681 test-z3`static_features::process_root(this=0x0000000822f3b5b8, e=0x000000082901a218) at static_features.cpp:602:5
    frame #26: 0x000000000278b6f2 test-z3`static_features::collect(this=0x0000000822f3b5b8, num_formulas=1, formulas=0x0000000829012e30) at static_features.cpp:607:9
    frame #27: 0x000000000139ba12 test-z3`smt::setup::setup_unknown(this=0x0000000829073098) at smt_setup.cpp:952:12
    frame #28: 0x000000000139c49a test-z3`smt::setup::setup_default(this=0x0000000829073098) at smt_setup.cpp:135:13
    frame #29: 0x000000000139b922 test-z3`smt::setup::operator(this=0x0000000829073098, cm=CFG_LOGIC)(smt::config_mode) at smt_setup.cpp:65:25
    frame #30: 0x00000000010c504e test-z3`smt::context::setup_context(this=0x0000000829073008, use_static_features=false) at smt_context.cpp:3557:9
    frame #31: 0x00000000010c2b30 test-z3`smt::context::check(this=0x0000000829073008, num_assumptions=0, assumptions=0x0000000000000000, reset_cancel=true) at smt_context.cpp:3585:9
    frame #32: 0x000000000157fe4b test-z3`smt::kernel::check(this=0x0000000822f3bd70, num_assumptions=0, assumptions=0x0000000000000000) at smt_kernel.cpp:128:35
    frame #33: 0x00000000008855d5 test-z3`test_doc_cls::check_equiv(this=0x0000000822f3c6f8, fml1=0x0000000822f3c230, fml2=0x0000000822f3c220) at doc.cpp:343:28
    frame #34: 0x0000000000887abd test-z3`test_doc_cls::test_project(this=0x0000000822f3c6f8, num_clauses=7) at doc.cpp:259:9
    frame #35: 0x0000000000882bf9 test-z3`test_doc_cls::test_project(this=0x0000000822f3c6f8, num_rounds=200, num_clauses=7) at doc.cpp:364:13
    frame #36: 0x0000000000880b28 test-z3`tst_doc() at doc.cpp:483:8
    frame #37: 0x00000000009ecabe test-z3`main(argc=2, argv=0x0000000822f3ede8) at main.cpp:163:5
    frame #38: 0x00000000008471d0 test-z3`_start(ap=<unavailable>, cleanup=<unavailable>) at crt1_c.c:73:7

nunoplopes · 2022-05-10T18:53:01Z

That trace doesn't help, sorry.
Maybe edit src/util/memory_manager.h to disable Z3's memory allocator to help with the investigation?
You'll need to debug this yourself. The code that is crashing for you runs perfectly fine on windows and linux. It's exercised all the time, so this is either a bug in freebsd or some unalignment or something similar (bug in Z3), but the information you've provided so far doesn't help us debug.

nunoplopes · 2022-05-12T09:36:39Z

Closing this for now. Please reopen once you've more information. Thank you!

arrowd · 2022-05-13T16:05:27Z

AddressSanitizer didn't help as it hides the problem just as building in the debugging mode.

However, applying the following hack fixed the problem for me:

@@ -258,7 +258,7 @@ static void synchronize_counters(bool allocating) {
 }
 
 void memory::deallocate(void * p) {
-    size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
+    size_t * sz_p  = reinterpret_cast<size_t*>(reinterpret_cast<char*>(p) - 16);
     size_t sz      = *sz_p;
     void * real_p  = reinterpret_cast<void*>(sz_p);
     g_memory_thread_alloc_size -= sz;
@@ -269,7 +269,7 @@ void memory::deallocate(void * p) {
 }
 
 void * memory::allocate(size_t s) {
-    s = s + sizeof(size_t); // we allocate an extra field!
+    s = s + 16; // we allocate an extra field!
     void * r = malloc(s);
     if (r == 0) {
         throw_out_of_memory();
@@ -282,14 +282,14 @@ void * memory::allocate(size_t s) {
         synchronize_counters(true);
     }
 
-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+    return static_cast<char*>(r) + 16; // we return a pointer to the location after the extra field
 }
 
 void* memory::reallocate(void *p, size_t s) {
-    size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
+    size_t *sz_p = reinterpret_cast<size_t*>(reinterpret_cast<char*>(p)-16);
     size_t sz = *sz_p;
     void *real_p = reinterpret_cast<void*>(sz_p);
-    s = s + sizeof(size_t); // we allocate an extra field!
+    s = s + 16; // we allocate an extra field!
 
     g_memory_thread_alloc_size += s - sz;
     g_memory_thread_alloc_count += 1;
@@ -303,7 +303,7 @@ void* memory::reallocate(void *p, size_t s) {
         return nullptr;
     }
     *(static_cast<size_t*>(r)) = s;
-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+    return static_cast<char*>(r) + 16; // we return a pointer to the location after the extra field
 }
 
 #else

Could it be that malloc makes some guarantees about pointer alignment, which gets breaked by z3's memory manager?

nunoplopes · 2022-05-13T18:43:18Z

Oh dear.. It makes sense: your crash is in movaps, which requires a 16-byte aligned address. Z3's malloc only guarantees an 8-byte alignment.
This is annoying, because Z3 has a lot of small allocations, and wasting 16 bytes per allocation is non-trivial. Maybe we should just disable the emission of these aligned moves. I thought compilers were not emitting them anymore..

arrowd · 2022-05-14T11:58:32Z

Why do you need to store the memory buffer's length in the first place?

nunoplopes · 2022-05-14T13:32:26Z

To keep track of memory consumption. That's very important to avoid explosions.

NikolajBjorner · 2022-05-15T00:02:12Z

To keep track of memory consumption. That's very important to avoid explosions.

in reality it is mostly aspirational: one can also query the heap for information and when using std::string and other std:: with the default memory allocator it isn't tracked. We tried using mimalloc for mpz specifically and the savings were not clearly measurable, but with mimalloc could also have the memory module be a throughfare to it. Well-supported allocators should handle alignment compatibility properly.

arrowd · 2022-05-15T10:46:46Z

one can also query the heap for information

Yep, the following change worked for me too:

diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 4fdf20c3a..e23569cd7 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/error_codes.h"
 #include "util/debug.h"
 #include "util/scoped_timer.h"
+#include "malloc_np.h"
 // The following two function are automatically generated by the mk_make.py script.
 // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
 // For example, rational.h contains
@@ -258,52 +259,43 @@ static void synchronize_counters(bool allocating) {
 }
 
 void memory::deallocate(void * p) {
-    size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
-    size_t sz      = *sz_p;
-    void * real_p  = reinterpret_cast<void*>(sz_p);
-    g_memory_thread_alloc_size -= sz;
-    free(real_p);
+    g_memory_thread_alloc_size -= malloc_usable_size(p);
+    if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0;
+    free(p);
     if (g_memory_thread_alloc_size < -SYNCH_THRESHOLD) {
         synchronize_counters(false);
     }
 }

 void * memory::allocate(size_t s) {
-    s = s + sizeof(size_t); // we allocate an extra field!
     void * r = malloc(s);
     if (r == 0) {
         throw_out_of_memory();
         return nullptr;
     }
-    *(static_cast<size_t*>(r)) = s;
     g_memory_thread_alloc_size += s;
     g_memory_thread_alloc_count += 1;
     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
         synchronize_counters(true);
     }
 
-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+    return r; // we return a pointer to the location after the extra field
 }
 
 void* memory::reallocate(void *p, size_t s) {
-    size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
-    size_t sz = *sz_p;
-    void *real_p = reinterpret_cast<void*>(sz_p);
-    s = s + sizeof(size_t); // we allocate an extra field!
-
-    g_memory_thread_alloc_size += s - sz;
+    g_memory_thread_alloc_size += s - malloc_usable_size(p);
+    if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0;
     g_memory_thread_alloc_count += 1;
     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
         synchronize_counters(true);
     }
 
-    void *r = realloc(real_p, s);
+    void *r = realloc(p, s);
     if (r == 0) {
         throw_out_of_memory();
         return nullptr;
     }
-    *(static_cast<size_t*>(r)) = s;
-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+    return r;
 }
 
 #else

The malloc_usable_size() is a jemalloc-specific call that returns allocation size for a given pointer. This looks like a good enough workaround, which I'm going to add as a patch to the FreeBSD package.

Interestingly, adding __attribute__((assume_aligned (16, 8)) or __attribute__((assume_aligned (8)) to the original version of memory::allocate and reallocate doesn't fix the problem.

NikolajBjorner · 2022-05-15T18:57:31Z

which I'm going to add as a patch to the FreeBSD package

Would this be a workaround?
I am trying to understand what can be done uniformly: if there is an environment variable that can be used to extract the pointer alignment of BSD 14 for the used platform. util/machine.h postulates ptr_alignment (to either 4 or 8 bytes).

arrowd · 2022-05-15T19:00:46Z

Would this be a workaround?

Yep, this isn't a proper fix, but the package is broken at the moment, so I need something until you figure out a proper solution.

if there is an environment variable that can be used to extract the pointer alignment of BSD 14 for the used platform

Can't we just compute it at runtime with % 8/%16?

NikolajBjorner · 2022-05-15T19:16:14Z

I don't know what the runtime utility would be (if-defed if it isn't cross-platform), but it is very fine too if there is something that can be used. The hard fix seems to just get rid of this layer and use mimalloc that is better engineered and appears to have utility to query heap allocated memory for allocation size.
https://github.com/microsoft/mimalloc/blob/f2712f4a8f038a7fb4df2790f4c3b7e3ed9e219b/include/mimalloc.h#L358

NikolajBjorner · 2022-05-16T03:10:24Z

alright, we need something like std::alignof to either be queried once or passed by the alloc macro. https://en.cppreference.com/w/cpp/language/alignof; or just use 16 for everything; or use mimalloc.

arrowd · 2022-07-16T19:34:54Z

Any movement on this?

NikolajBjorner · 2022-07-16T23:07:38Z

If you want to make a move, the better option appears to be to port memory_manager to use instead mimalloc.

nunoplopes · 2022-09-05T18:37:07Z

I don't know if your BSD supports malloc_usable_size or similar, but if so, then this PR will help: #6321

arrowd · 2022-09-05T19:22:54Z

@nunoplopes #6015 (comment)

nunoplopes · 2022-09-05T20:07:53Z

@nunoplopes #6015 (comment)

ah, good. So maybe we can have the glibc version and then patch to learn about freebsd as well?

nunoplopes · 2022-10-17T20:30:24Z

fixed, thank you!

Naville · 2023-09-07T10:08:15Z

Ping, is there any workarounds without having to patch Z3 source?

Naville · 2023-09-07T10:19:55Z

Starting a new thread with new info....

nunoplopes closed this as completed May 12, 2022

nunoplopes reopened this May 13, 2022

nunoplopes closed this as completed Oct 17, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SIGBUS due to unaligned access #6015

SIGBUS due to unaligned access #6015

arrowd commented May 2, 2022

NikolajBjorner commented May 3, 2022

arrowd commented May 4, 2022

arrowd commented May 4, 2022

nunoplopes commented May 10, 2022 •

edited

Loading

arrowd commented May 10, 2022

NikolajBjorner commented May 10, 2022 •

edited

Loading

arrowd commented May 10, 2022

nunoplopes commented May 10, 2022 •

edited

Loading

arrowd commented May 10, 2022

arrowd commented May 10, 2022

nunoplopes commented May 10, 2022

nunoplopes commented May 12, 2022

arrowd commented May 13, 2022

nunoplopes commented May 13, 2022

arrowd commented May 14, 2022

nunoplopes commented May 14, 2022

NikolajBjorner commented May 15, 2022

arrowd commented May 15, 2022

NikolajBjorner commented May 15, 2022

arrowd commented May 15, 2022

NikolajBjorner commented May 15, 2022

NikolajBjorner commented May 16, 2022

arrowd commented Jul 16, 2022

NikolajBjorner commented Jul 16, 2022

nunoplopes commented Sep 5, 2022

arrowd commented Sep 5, 2022

nunoplopes commented Sep 5, 2022

nunoplopes commented Oct 17, 2022

Naville commented Sep 7, 2023

Naville commented Sep 7, 2023

SIGBUS due to unaligned access #6015

SIGBUS due to unaligned access #6015

Comments

arrowd commented May 2, 2022

NikolajBjorner commented May 3, 2022

arrowd commented May 4, 2022

arrowd commented May 4, 2022

nunoplopes commented May 10, 2022 • edited Loading

arrowd commented May 10, 2022

NikolajBjorner commented May 10, 2022 • edited Loading

arrowd commented May 10, 2022

nunoplopes commented May 10, 2022 • edited Loading

arrowd commented May 10, 2022

arrowd commented May 10, 2022

nunoplopes commented May 10, 2022

nunoplopes commented May 12, 2022

arrowd commented May 13, 2022

nunoplopes commented May 13, 2022

arrowd commented May 14, 2022

nunoplopes commented May 14, 2022

NikolajBjorner commented May 15, 2022

arrowd commented May 15, 2022

NikolajBjorner commented May 15, 2022

arrowd commented May 15, 2022

NikolajBjorner commented May 15, 2022

NikolajBjorner commented May 16, 2022

arrowd commented Jul 16, 2022

NikolajBjorner commented Jul 16, 2022

nunoplopes commented Sep 5, 2022

arrowd commented Sep 5, 2022

nunoplopes commented Sep 5, 2022

nunoplopes commented Oct 17, 2022

Naville commented Sep 7, 2023

Naville commented Sep 7, 2023

nunoplopes commented May 10, 2022 •

edited

Loading

NikolajBjorner commented May 10, 2022 •

edited

Loading

nunoplopes commented May 10, 2022 •

edited

Loading