FFI to Rust/C++

Stream: lean4

[Tage Johansson]

I tried to build the Rust FFI template in this repo. It basicly compiles the Rust functions to a static c++ library and then uses functions from that in the lean code. But for some strange reason lake build fails on my machine. I get the following strange error:

Compiling shim.cpp
Creating libffi.a
Linking libffi.so
Building FFI
error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=/home/tage/.elan/toolchains/leanprover--lean4---nightly-2022-12-08/lib:./build/lib:./build/src /home/tage/.elan/toolchains/leanprover--lean4---nightly-2022-12-08/bin/lean ./lean/./FFI.lean -R ./lean/. -o ./build/lib/FFI.olean -i ./build/lib/FFI.ilean -c ./build/ir/FFI.c --load-dynlib=libffi.so
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ./build/src/libffi.so: undefined symbol: _ZNSt8ios_base4InitD1Ev
error: external command `/home/tage/.elan/toolchains/leanprover--lean4---nightly-2022-12-08/bin/lean` exited with code 134

I think the point here is the undefined symbol _ZNSt8ios_base4InitD1Ev. After some googling it seems that it has something to do with the linking of libc++.so.

So does anyone have any experience of linking c++ libraries and what might cause the error?

[Arthur Paulino]

Yeah, this is something we've been trying to do for a while. So far, the setup is flaky and doesn't work on all machines. There is a nix branch that seems to work though (I haven't tested it yet). This is highly experimental at this point, as you can see

[Henrik Böving]

Is there a reason you are going over C++ instead of just using the C FFI that we already have in Lean? In theory we could auto generate all of the Lean <-> C FFI <-> Rust glue code automatically just from the types that are in Lean without dealing with C++ at all.

[Henrik Böving]

Basically like https://github.com/rust-lang/rust-bindgen but for Lean instead (of course the tool would be written in Lean instead of Rust in order to access the Environment.

[Arthur Paulino]

Do you mean parsing Rust code in Lean?

[Henrik Böving]

No. When you compile lean code and you tag a declaration with @[export] you can know the symbol name in advance, furthermore you can also deduce the C type of the function in advance based on our FFI. Since you can do this you can also automatically decude a Rust representation of any Lean type automatically (based on #[repr(C)], however many lean types will end up being lean_object*. For that you can define type aliases + wrapper functions to allocate and pattern match on stuff). So in theory I believe it should be possible to automatically generate a .rs file using a Lean program that reads some other Lean file and exposes all of the functions tagged with export in that Lean file to Rust + at least working representation of all Lean types defined in that file in Rust. I don't think that representation and the way you interact with it will necessarily end up being safe but it should in general be possible.

[Henrik Böving]

So basically writing a bindgen that generates a Rust C FFI layer for some arbitrary Lean file automatically should be perfectly possible.

[Arthur Paulino]

Sorry, I still don't understand it. Suppose we have some huge Rust lib whose behavior we want to access from Lean. How would an automatically generated .rs file help us bridge the gap between Lean and Rust?

[Arthur Paulino]

We want to use access Rust programs from Lean, not the other way around

[Henrik Böving]

Arthur Paulino said:

We want to use access Rust programs from Lean, not the other way around

But surely you are passing Lean objects into those rust programs so you will still need the information about Lean exposed in Rust no? Exposing the Rust types to Lean is also possible via C FFI if you want to.

[Henrik Böving]

What I am confused about is, why are you taking the indirection over the C++ FFI with cxx when both Rust and Lean support C FII.

[Arthur Paulino]

In my mind, it's the flow of data. Lean can use code that's written in C. So does Rust. But we are trying to use code that's written in Rust from Lean

[Arthur Paulino]

The Lean objects that we want to pass are extremely simple, like unboxed unsigned integers and such. Writing the bindings is the easy part - we do it by hand.

[Reid Barton]

But then why is C++ (rather than C) involved?

[Arthur Paulino]

Because that's what https://cxx.rs/ provides

[Reid Barton]

... is there https://c.rs/ ?

[Reid Barton]

Unlucky.

[Reid Barton]

Avoiding C++ should make everything easier.

[Reid Barton]

The C ABI is in general the normal way to do FFI; I imagine it must be supported natively by Rust

[Henrik Böving]

It is, CXX does still use the C ABI under the hood it just hides stuff behind a C++ facade.

[Arthur Paulino]

@Tage Johansson Okay it works now (thanks everyone!!)
The misconception I had was that I didn't think we could call Rust code from C. I thought it was like Lean, which allows us to call C code from it.

Here's the PR with the changes: https://github.com/yatima-inc/FFI.lean/pull/1
You might as well just fetch the c branch

[Anders Christiansen Sørby]

@Arthur Paulino I tried that approach, but I still get the undefined symbol error above. The --load-dynlib doesn't include all the rust library dependencies. Also how this is added to the lean runtime command is rather undocumented. I also need some way of providing the libraries in topological order which is not the default case. How can I add more runtime dynlibs to the lean command invocation by lake?

[Notification Bot]

Anders Christiansen Sørby has marked this topic as unresolved.

[Anders Christiansen Sørby]

I'm trying to link lean with an advanced rust application and using lean as the main entrypoint and executable.

[Anders Christiansen Sørby]

@Mac Is it possible to disable the load dynlib feature in Lake? I don't think I will need this in the interpreter

[Arthur Paulino]

@Anders Christiansen Sørby the repo had to undergo yet another change in order to work when used as a dependency. This is the template: https://github.com/yatima-inc/RustFFI.lean

[Anders Christiansen Sørby]

I based it on that repo, but it is a rust lib with no dependencies so not very representative. With dependencies you need to have all the dynlib dependencies topologically sorted or disable the --load-dynlib

[Anders Christiansen Sørby]

I guess I could do something similar to copy out all those libraries too

[Mac Malone]

Anders Christiansen Sørby said:

Mac Is it possible to disable the load dynlib feature in Lake? I don't think I will need this in the interpreter

Just turn off precompileModules? Oh, I guess you mean turning off loading external shared libraries during interpretation. Sadly, no that is not currently an option. It would be pretty easier to add though.

[Mac Malone]

One important design decision question, though, would be what should happen if a dependent package wants its dependencies dynlibs loaded but the dependency itself does not.

[Sebastian Ullrich]

@Anders Christiansen Sørby
Why does the external shared library not properly declare its dependencies? At least on Unix, loading a correctly linked dynlib should automatically load its dependencies.

[Sebastian Ullrich]

I suppose a simple workaround for avoiding the --load-dynlib though would be not to tell Lake about the library but add it manually to the linker flags

[Anders Christiansen Sørby]

@Mac Yeah, that could be a nice feature.

[Anders Christiansen Sørby]

@Sebastian Ullrich So that would mean using just target instead of externLib?
The library declares some of it's dependencies which is shown by ldd, but not all apparently(?). I don't know why. It is built with rust and cargo to a static lib. Copied over to the build dir. How this interpreter dynamic loading is enabled is mysterious and it would be nice to have an option.
Would love for some more work on the FFI. Maybe someone will make a full rust FFI ABI interface?

[Anders Christiansen Sørby]

@Sebastian Ullrich I've tried handcrafting the link args, but I run into other problems:
Using roughly /home/anderscs/.elan/toolchains/leanprover--lean4---nightly-2023-02-06/bin/leanc -o ./build/bin/remodel ./build/ir/Main.o ./build/ir/Remodel.o -Lbuild/lib/ -Lrust/target/release/deps -lc -lc++ -lc++abi -lffi -lremodel_rust_ffi

Which leads to some undefined references

/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::_M_replace(unsigned long, unsigned long, char const*, unsigned long)'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__future_base::_Result_base::_Result_base()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__throw_bad_cast()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::~basic_string()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::thread::detach()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::thread::join()'

Why are these rust symbols not linked? I suppose these are from the rust std lib and intended to be loaded at runtime?

[Anders Christiansen Sørby]

Ok, the answer is that I didn't link with stdc++and Idk why that is needed in a rust binary.

[Reid Barton]

Reading between the lines, it seems like your Rust library has Rust dependencies, and maybe some parts of those are implemented in C++?

[Anders Christiansen Sørby]

Ok, it works now. leanc -o ./build/bin/remodel ./build/ir/Main.o ./build/ir/Remodel.o -Lbuild/lib/ -lssl -lstdc++ -lffi -lremodel_rust_ffi
I think I can remove the -lstdc++ too if I don't include the cxx rust dependency.

[Anders Christiansen Sørby]

Rust shouldn't need stdc++ normally

[Anders Christiansen Sørby]

@Mac Follow up question: How do I add the targets to extraDepTargets without causing unknown identifier '_package.name'

[Anders Christiansen Sørby]

Oh, it was just adding strings not symbols

[Anders Christiansen Sørby]

What would be best practice for working with strings in a Rust to Lean and Lean to Rust context? Is it passing strings to lean_mk_string_from_bytes(str, str_len) based on the string in Rust? Just using lean_mk_string(str) on a null terminated C string borrowed from rust seems to cause segmentation fault.

[Anders Christiansen Sørby]

This causes a segmentation fault. Do I perhaps need to run lean_inc(ns)? @Sebastian Ullrich ?

extern void rust_test(const char* name) {
  //char* namec = malloc();
  lean_obj_res ns = lean_mk_string(name);
  char* name_l = lean_string_cstr(ns);
}

[Sebastian Ullrich]

I don't see how that could fail if the string is indeed null-terminated. But really there's no reason not to use lean_mk_string_from_bytes if you want to avoid the extra conversion

[Anders Christiansen Sørby]

Both of them cause segmentation fault apparently. Does lean_mk_string_from_bytes copy the string? Need to do more debugging next week.

[Sebastian Ullrich]

It does

[Anders Christiansen Sørby]

It causes a segmentation fault and idk why.
Given this rust code calling from inside a tokio runtime:

let name = CString::new(name).expect("CString::new failed");
 unsafe {
        let name_raw = name.into_raw();
        let result = rust_test(name_raw, name_len);
        // Take back ownership and drop
        drop(CString::from_raw(name_raw));
}

This causes a Segmentation fault in 0x000000000447258b in lean::utf8_strlen(char const*, unsigned long) ()

extern char* rust_test(const char* name, size_t name_len) {
  lean_obj_res ns = lean_mk_string_from_bytes(name, name_len);
//...

I've also tried to use the rust as_bytes approach

let name = name.as_bytes();
 unsafe {
        let result = rust_test(name.as_ptr().cast(), name.len());

}

But this also leads to segmentation fault. Can this be due to the pointer being freed before it is passed to C? I'm pretty stuck

[Anders Christiansen Sørby]

@Sebastian Ullrich Do you have some hints?

[Sebastian Ullrich]

There is some way to find out the address of a segfault in gdb, you could check what the correlation to the pointer address in Rust is. Otherwise I can't say anything on these snippets.

[Anders Christiansen Sørby]

gdb reports the segfault in lean::utf8_strlen(char const*, unsigned long), but it seems to happen even when I set the size to 0 and the pointer should never be accessed.

[Anders Christiansen Sørby]

I guess my next step would be to break the error down into even smaller pieces.