Strange memory error from FFI

Stream: general

[Schrodinger ZHU Yifan]

Help needed!

I was still working on a hashset/hashmap binding to lean: https://github.com/SchrodingerZhu/hashbrown4lean

The idea was to check and ensure the exclusivity of an lean_external_object whenever a mutation happens. However, I run into segfault with this approach. I have reduced the code to an example that does nothing but check and ensure the exclusivity:

In Rust,

#[no_mangle]
pub unsafe extern "C" fn lean_hashbrown_test(
    obj: lean_obj_arg,
    _hash: u64,
    _target: lean_obj_arg,
    _eq_closure: lean_obj_arg,
    _hash_closure: lean_obj_arg,
) -> lean_obj_res {
    println!("test invoked");
    let obj = exlusive_hashset(obj);
    obj
}
unsafe fn exlusive_hashset(set: lean_obj_arg) -> lean_obj_res {
    if lean_is_exclusive(set) {
        println!("target is exclusive: {:?}", set);
        set
    } else {
        println!("target is not exclusive: {:?}", set);
        let inner: *mut HashSet = get_data_from_external(set);
        let cloned = Box::into_raw(Box::new((*inner).clone()));
        let new_set = lean_alloc_external(HASHSET_CLASS, cloned as *mut c_void);
        println!("new set: {:?}", new_set);
        for i in (*inner).iter() {
            lean_inc(*i.as_ref());
        }
        lean_dec_ref(set);
        new_set
    }
}

In lean:

opaque HashSetPointed : (α : Type) → NonemptyType
def HashSet (α : Type) : Type := (HashSetPointed α).type
instance : Nonempty (HashSet α) := (HashSetPointed α).property

@[extern "lean_hashbrown_hashset_len"]
opaque HashSet.len : {α : Type} → @& HashSet α → USize

@[extern "lean_hashbrown_hashset_create"]
opaque HashSet.mk : {α : Type} → HashSet α

@[extern "lean_hashbrown_test"]
private opaque HashSet.test : {α : Type}
  → HashSet α → UInt64 → α → @&(α → Bool) → @&(α → UInt64) → HashSet α

@[extern "lean_hashbrown_register_hashset_class"]
private opaque registerHashSetClass : IO PUnit

@[extern "lean_hashbrown_register_hashset_iter_class"]
private opaque registerHashSetIterClass : IO PUnit

@[init]
private def initModule : IO Unit := do
 registerHashSetClass
 registerHashSetIterClass

def main : IO Unit := do
  let set : HashSet Nat := HashSet.mk
  let hash := 1
  let target := 1
  let check := λ x => x == 1
  let hashFn := λ x => 1
  let set := set.test hash target check hashFn
  IO.println s!"Hello, {set.len}!"

Yet, it still crashes:

❯  ./build/bin/swisstable
lean_set_st_header(0x7fe686cd6f38, 0, 2)
   0: lean_hashbrown::ffi::lean_set_st_header
             at ./src/ffi.rs:128:71
   1: lean_hashbrown::ffi::lean_alloc_ctor
             at ./src/ffi.rs:145:5
   2: lean_hashbrown::ffi::lean_io_result_mk_ok
             at ./src/ffi.rs:151:13
   3: lean_hashbrown_register_hashset_class
             at ./src/set.rs:103:5
   4: l___private_Main_0__initModule
   5: initialize_Main
   6: main
   7: __libc_start_call_main
             at /usr/src/debug/glibc/glibc/csu/../sysdeps/nptl/libc_start_call_main.h:58:16
   8: __libc_start_main_impl
             at /usr/src/debug/glibc/glibc/csu/../csu/libc-start.c:360:3
   9: _start

lean_set_st_header(0x7fe686cd6f38, 0, 2)
   0: lean_hashbrown::ffi::lean_set_st_header
             at ./src/ffi.rs:128:71
   1: lean_hashbrown::ffi::lean_alloc_ctor
             at ./src/ffi.rs:145:5
   2: lean_hashbrown::ffi::lean_io_result_mk_ok
             at ./src/ffi.rs:151:13
   3: lean_hashbrown_register_hashset_iter_class
             at ./src/set.rs:110:5
   4: initialize_Main
   5: main
   6: __libc_start_call_main
             at /usr/src/debug/glibc/glibc/csu/../sysdeps/nptl/libc_start_call_main.h:58:16
   7: __libc_start_main_impl
             at /usr/src/debug/glibc/glibc/csu/../csu/libc-start.c:360:3
   8: _start

lean_alloc_small_object(sz: 24)
   0: lean_hashbrown::ffi::lean_alloc_small_object
             at ./src/ffi.rs:163:13
   1: lean_hashbrown::ffi::lean_alloc_external
             at ./src/ffi.rs:177:15
   2: lean_hashbrown_hashset_create
             at ./src/set.rs:52:15
   3: initialize_Main
   4: main
   5: __libc_start_call_main
             at /usr/src/debug/glibc/glibc/csu/../sysdeps/nptl/libc_start_call_main.h:58:16
   6: __libc_start_main_impl
             at /usr/src/debug/glibc/glibc/csu/../csu/libc-start.c:360:3
   7: _start

lean_set_st_header(0x7fe686cd6f38, 254, 0)
   0: lean_hashbrown::ffi::lean_set_st_header
             at ./src/ffi.rs:128:71
   1: lean_hashbrown::ffi::lean_alloc_external
             at ./src/ffi.rs:178:5
   2: lean_hashbrown_hashset_create
             at ./src/set.rs:52:15
   3: initialize_Main
   4: main
   5: __libc_start_call_main
             at /usr/src/debug/glibc/glibc/csu/../sysdeps/nptl/libc_start_call_main.h:58:16
   6: __libc_start_main_impl
             at /usr/src/debug/glibc/glibc/csu/../csu/libc-start.c:360:3
   7: _start

hashset_foreach(0x5576de6423d0, 0x7fe686cd6f20)
   0: lean_hashbrown::set::hashset_foreach
             at ./src/set.rs:65:53
   1: lean_mark_persistent
   2: initialize_Main
   3: main
   4: __libc_start_call_main
             at /usr/src/debug/glibc/glibc/csu/../sysdeps/nptl/libc_start_call_main.h:58:16
   5: __libc_start_main_impl
             at /usr/src/debug/glibc/glibc/csu/../csu/libc-start.c:360:3
   6: _start

lean_dec_ref(0x7fe686cd6f20), m_rc = 1
test invoked
target is not exclusive: 0x7fe686cd6f38
lean_alloc_small_object(sz: 24)
   0: lean_hashbrown::ffi::lean_alloc_small_object
             at ./src/ffi.rs:163:13
   1: lean_hashbrown::ffi::lean_alloc_external
             at ./src/ffi.rs:177:15
   2: lean_hashbrown::set::exlusive_hashset
             at ./src/set.rs:139:23
   3: lean_hashbrown_test
             at ./src/set.rs:281:15
   4: _lean_main
   5: main
   6: __libc_start_call_main
             at /usr/src/debug/glibc/glibc/csu/../sysdeps/nptl/libc_start_call_main.h:58:16
   7: __libc_start_main_impl
             at /usr/src/debug/glibc/glibc/csu/../csu/libc-start.c:360:3
   8: _start

lean_set_st_header(0x7fe686cd6f09, 254, 0)
   0: lean_hashbrown::ffi::lean_set_st_header
             at ./src/ffi.rs:128:71
   1: lean_hashbrown::ffi::lean_alloc_external
             at ./src/ffi.rs:178:5
   2: lean_hashbrown::set::exlusive_hashset
             at ./src/set.rs:139:23
   3: lean_hashbrown_test
             at ./src/set.rs:281:15
   4: _lean_main
   5: main
   6: __libc_start_call_main
             at /usr/src/debug/glibc/glibc/csu/../sysdeps/nptl/libc_start_call_main.h:58:16
   7: __libc_start_main_impl
             at /usr/src/debug/glibc/glibc/csu/../csu/libc-start.c:360:3
   8: _start

thread '<unnamed>' panicked at 'misaligned pointer dereference: address must be a multiple of 0x4 but is 0x7fe686cd6f09', src/ffi.rs:129:5
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread caused non-unwinding panic. aborting.

Details are committed to the repo.

[Schrodinger ZHU Yifan]

Ok, I found the problem!

                    object * fn = lean_alloc_closure((void*)mark_persistent_fn, 1, 0);
                    lean_to_external(o)->m_class->m_foreach(lean_to_external(o)->m_data, fn);
                    lean_dec(fn);
                    break;

it is assumed that foreach accepts @& Fn. I did not notice that and corrupted the heap.