From a4a96bce618cffa8cceabc2cb93a5b3d3992128a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 5 Mar 2024 15:57:48 -0800 Subject: [PATCH] Add full calling example --- .gitignore | 1 + Cargo.lock | 49 +++++++++++++++++++++++++++++++++ Cargo.toml | 4 ++- README.md | 1 + build.rs | 66 ++++++++++++++++++++++++++++++++++++++++++++- flake.nix | 2 ++ rust-toolchain.toml | 2 ++ src/main.rs | 40 +++++++++++++++++++++++---- 8 files changed, 158 insertions(+), 7 deletions(-) create mode 100644 rust-toolchain.toml diff --git a/.gitignore b/.gitignore index 9ea0f13..01fc188 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .* +*.olean !.gitignore diff --git a/Cargo.lock b/Cargo.lock index d33082b..6a1a17f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -11,12 +11,23 @@ dependencies = [ "memchr", ] +[[package]] +name = "annotate-snippets" +version = "0.9.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ccaf7e9dfbb6ab22c82e473cd1a8a7bd313c19a5b7e40970f3d89ef5a5c9e81e" +dependencies = [ + "unicode-width", + "yansi-term", +] + [[package]] name = "bindgen" version = "0.69.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a00dc851838a2120612785d195287475a3ac45514741da670b735818822129a0" dependencies = [ + "annotate-snippets", "bitflags", "cexpr", "clang-sys", @@ -242,6 +253,7 @@ name = "rustcalllean" version = "0.1.0" dependencies = [ "bindgen", + "libc", ] [[package]] @@ -280,6 +292,12 @@ version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" +[[package]] +name = "unicode-width" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e51733f11c9c4f72aa0c160008246859e340b00807569a0da0e7a1079b27ba85" + [[package]] name = "which" version = "4.4.2" @@ -292,6 +310,28 @@ dependencies = [ "rustix", ] +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" + +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" + [[package]] name = "windows-sys" version = "0.52.0" @@ -357,3 +397,12 @@ name = "windows_x86_64_msvc" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8" + +[[package]] +name = "yansi-term" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fe5c30ade05e61656247b2e334a031dfd0cc466fadef865bdcdea8d537951bf1" +dependencies = [ + "winapi", +] diff --git a/Cargo.toml b/Cargo.toml index 9de7b0a..c6d3a93 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,6 +9,8 @@ edition = "2021" rust-version = "1.73" [dependencies] +libc = "0.2.153" [build-dependencies] -bindgen = "0.69.4" +# the experimental flag must be enabled +bindgen = { version = "0.69.4", features = ["experimental"] } diff --git a/README.md b/README.md index fc2fa99..476bb27 100644 --- a/README.md +++ b/README.md @@ -7,3 +7,4 @@ This is based on: * [Lean4 FFI](https://lean-lang.org/lean4/doc/dev/ffi.html#initialization) * [Rustonomicon FFI](https://doc.rust-lang.org/nomicon/ffi.html) * [Rust Bindgen](https://rust-lang.github.io/rust-bindgen/introduction.html) +* [Rust Bindgen Static Functions](https://github.com/rust-lang/rust-bindgen/discussions/2405) diff --git a/build.rs b/build.rs index da9e4a2..573fa3b 100644 --- a/build.rs +++ b/build.rs @@ -7,6 +7,7 @@ fn main() { let callee_root = env::var("CALLEE_PATH").expect("Callee path variable must be available"); let lean_root = env::var("LEAN_ROOT").expect("Lean root must exist"); + let input = format!("{lean_root}/include/lean/lean.h"); println!("cargo:rustc-link-search={callee_root}"); println!("cargo:rustc-link-search={lean_root}/lib/lean"); println!("cargo:rustc-link-lib={CALLEE_NAME}"); @@ -19,18 +20,81 @@ fn main() let bindings = bindgen::Builder::default() // The input header we would like to generate // bindings for. - .header(format!("{lean_root}/include/lean/lean.h")) + .header(&input) // Tell cargo to invalidate the built crate whenever any of the // included header files changed. .parse_callbacks(Box::new(bindgen::CargoCallbacks::new())) + // The following is specific to `lean.h`: There are a lot of static + // function + .wrap_static_fns(true) + // but some functions use `_Atomic(int)` types that bindgen cannot handle, + // so they are blocklisted. The types which use `_Atomic` are treated as + // opaque. + .blocklist_function("lean_get_rc_mt_addr") + .opaque_type("lean_thunk_object") + .opaque_type("lean_task_object") // Finish the builder and generate the bindings. .generate() // Unwrap the Result and panic on failure. .expect("Unable to generate bindings"); + let extern_src_path = std::env::temp_dir().join("bindgen").join("extern.c"); + let extern_obj_path = std::env::temp_dir().join("bindgen").join("extern.o"); + let output_path = PathBuf::from(std::env::var("OUT_DIR").unwrap()); // Write the bindings to the $OUT_DIR/bindings.rs file. let out_path = PathBuf::from(env::var("OUT_DIR").unwrap()); bindings .write_to_file(out_path.join("lean.rs")) .expect("Couldn't write bindings!"); + + // This is the path to the object file. + let obj_path = output_path.join("extern.o"); + // This is the path to the static library file. + let lib_path = output_path.join("libextern.a"); + + // Compile the generated wrappers into an object file. + let clang_output = std::process::Command::new("clang") + .arg("-O") + .arg("-c") + .arg("-o") + .arg(extern_obj_path) + .arg(extern_src_path) + .arg("-include") + .arg(&input) + .output() + .unwrap(); + if !clang_output.status.success() { + panic!( + "Could not compile object file:\n{}", + String::from_utf8_lossy(&clang_output.stderr) + ); + } + + // Turn the object file into a static library + #[cfg(not(target_os = "windows"))] + let lib_output = std::process::Command::new("ar") + .arg("rcs") + .arg(output_path.join(&lib_path)) + .arg(obj_path) + .output() + .unwrap(); + #[cfg(target_os = "windows")] + let lib_output = std::process::Command::new("LIB") + .arg(obj_path) + .arg(format!( + "/OUT:{}", + out_dir_path.join("libextern.lib").display() + )) + .output() + .unwrap(); + if !lib_output.status.success() { + panic!( + "Could not emit library file:\n{}", + String::from_utf8_lossy(&lib_output.stderr) + ); + } + + // Statically link against the generated lib + println!("cargo:rustc-link-search={}", output_path.display()); + println!("cargo:rustc-link-lib=static=extern"); } diff --git a/flake.nix b/flake.nix index 6ee59d4..bc67e74 100644 --- a/flake.nix +++ b/flake.nix @@ -41,6 +41,8 @@ LEAN_ROOT = leanPkgs.lean-all; buildInputs = common ++ [ pkgs.rustc + # This is not needed for compilation. It is here for diagnostic purposes + pkgs.rust-bindgen ]; }; }; diff --git a/rust-toolchain.toml b/rust-toolchain.toml new file mode 100644 index 0000000..5d56faf --- /dev/null +++ b/rust-toolchain.toml @@ -0,0 +1,2 @@ +[toolchain] +channel = "nightly" diff --git a/src/main.rs b/src/main.rs index ef3c08f..79a52c5 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,21 +1,51 @@ #[allow(non_upper_case_globals)] #[allow(non_camel_case_types)] #[allow(non_snake_case)] -mod lean { +#[allow(dead_code)] +mod lean +{ include!(concat!(env!("OUT_DIR"), "/lean.rs")); - #[link(name="lean")] - extern { + #[link(name = "lean")] + extern "C" { pub fn lean_initialize_runtime_module(); pub fn lean_initialize(); // lean_io_mark_end_initialization is already defined. } + #[link(name = "Callee")] + extern "C" { + pub fn initialize_Callee(builtin: u8, world: *mut lean_object) -> *mut lean_object; + pub fn my_function(s: lean_obj_arg) -> lean_obj_arg; + } } -fn main() { +fn main() +{ unsafe { lean::lean_initialize_runtime_module(); lean::lean_initialize(); + let builtin: u8 = 1; + let res = lean::initialize_Callee(builtin, lean::lean_io_mk_world()); + if lean::lean_io_result_is_ok(res) { + lean::lean_dec_ref(res); + } else { + lean::lean_io_result_show_error(res); + lean::lean_dec(res); + panic!("Failed to load callee"); + } lean::lean_io_mark_end_initialization(); } - println!("Lean initialization complete!"); + println!("Lean initialization complete!"); + + let c_str = std::ffi::CString::new("hello ").unwrap(); + let result = unsafe { + let native_str = lean::lean_mk_string(c_str.as_ptr()); + let result_obj = lean::my_function(native_str); + let result_c_str = std::ffi::CStr::from_ptr(lean::lean_string_cstr(result_obj)); + let str = result_c_str.to_str().unwrap().to_string(); + // Clean up the resultant objects + lean::lean_dec(result_obj); + str + }; + + println!("result: {result}"); }