Issue with String marshalling between Lean and Rust FFI

Stream: lean4

[Daneshvar Amrollahi]

Hello everyone,

I'm working on a project that uses Lean to call into a Rust library via FFI. I'm having trouble with passing file paths from Lean to Rust.

My setup:

In Lean

(FFI.Lean):

namespace SMTParser

@[extern "test_ffi"] opaque testFFI : UInt32 → UInt32

@[extern "parse_smt_file"]
opaque parseSMTFile (path : @& String) : UInt32

end SMTParser

(Main.Lean):

def main (args : List String) : IO UInt32 := do
  match args with
  | [] => do
    IO.println "Please provide an SMT file path"
    return 1
  | filename :: _ => do
    IO.println s!"Processing SMT file: {filename}"
    SMTParser.processSMTFile filename

In Rust
(lib.rs):

#[unsafe(no_mangle)]
pub extern "C" fn parse_smt_file(_path: *const c_char) -> u32 {
    if _path.is_null() {
        eprintln!("Received null pointer for path");
        return 0;
    }

    // Convert C string to Rust string
    let path_str = unsafe {
        match CStr::from_ptr(_path).to_str() {
            Ok(s) => s,
            Err(e) => {
                eprintln!("Error converting path: {}", e);
                return 0;
            },
        }
    };

    eprintln!("Reading file: '{}'", path_str);

    // Read the file
    let contents = match fs::read_to_string(path_str) {
        Ok(s) => s,
        Err(e) => {
            eprintln!("Error reading file: {}", e);
            return 1;
        }
    };

    // Rest of the code...
}

When I pass a file path from Lean to Rust, the string doesn't seem to be properly marshalled. The Rust side can't correctly interpret the string pointer that Lean is passing.

A simple numeric FFI test works fine (test_ffi function that doubles an integer), but string passing is failing.

Does anyone know how can we properly pass a Lean String as a C-compatible string through Rust's FFI?

[Arthur Paulino]

This is how Lean strings are stored in memory:

// from lean.h
typedef struct {
    lean_object m_header;
    size_t      m_size;     /* byte length including '\0' terminator */
    size_t      m_capacity;
    size_t      m_length;   /* UTF8 length */
    char        m_data[];
} lean_string_object;

So you either have to intercept the call in C and pass ptr->m_data to Rust or you need to mimic that precise memory layout in Rust in order to access the m_data attribute

[Arthur Paulino]

Or, if you're feeling brave, add 32 to your pointer and read from there. It's the size of a lean_object (8 bytes) and three size_ts (8 bytes each on a 64bit machine).

[Arthur Paulino]

If you choose to mimic the memory layout in Rust, make sure to tag your LeanStringObject struct with #[repr(C)]!

[Daneshvar Amrollahi]

Thanks Arthur. I managed to do it by mimicing the struct in my Rust code.
But it seems like a very fragile solution. For instance if the String object for Lean changes for some reason in the future updates, this would break. Is there a more clean solution for this?

[Arthur Paulino]

These basic structs from lean.h are pretty stable already. But passing ptr->m_data (or, even better, lean_string_cstr(ptr)) from C to Rust is more stable because in the worst case you'd get a compilation error from your C code. The price of this solution is that your build becomes a bit messier, mixing up C and Rust.

[Arthur Paulino]

But keep in mind that FFI is fundamentally unsafe, so it's always gonna feel a bit itchy.