Libcprover-rust

方便与CProver工具交互的Rust接口。

构建说明

要构建Rust项目，您需要安装Rust语言工具链（您可以从 rustup.rs 安装）。

安装后，您可以在当前目录（src/libcprover-rust）下执行 cargo build 命令。

为此，您需要向项目提供两个环境变量

• CBMC_LIB_DIR，用于选择libcprover-x.y.z.a的位置（例如，如果您已下载包含静态库的预包装版本），
• CBMC_INCLUDE_DIR，用于选择cprover/api.h的位置，以及
• CBMC_VERSION，用于选择要链接的库版本（如果您在同一位置有多个版本的库，并且您想控制编译时使用哪个版本，这很有用）。

以下是通过cargo构建API的示例命令序列（假设您是从CBMC项目的根目录执行这些命令的）。

$ cd src/libcprover-rust
$ cargo clean
$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build

要构建项目和运行其关联的测试，命令序列如下所示

$ cd src/libcprover-rust
$ cargo clean
$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture

基本用法

此文件将引导您通过API进行一次示例交互，在基本场景下：加载文件并验证其中的模型。

首先，我们将假设您在/tmp/api_example.c下有一个文件，内容如下

int main(int argc, char *argv[])
{
  int arr[] = {0, 1, 2, 3};
  __CPROVER_assert(arr[3] != 3, "expected failure: arr[3] == 3");
}

要开始与API进行任何交互，我们首先需要使用函数new_api_session创建一个新的api_sessiont句柄。

let client = cprover_api::new_api_session();

然后，我们需要将文件添加到包含文件名的向量中，这些文件名指示了验证引擎要加载哪些模型。

let vec: Vec<String> = vec!["/tmp/api_example.c".to_owned()];

let vect = ffi_util::translate_rust_vector_to_cpp(vec);

在上面的代码示例中，我们创建了一个Rust语言的字符串向量（vec）。在下一行中，我们调用模块ffi_util中的一个实用函数，将Rust的Vec<String>转换为C++的等效向量std::vector<std::string> - 这一步是至关重要的，因为我们需要将类型转换为C++端理解的形式。

这些操作是显式的：我们选择在FFI级别强制用户在类型之间进行转换，以减少“魔法”并使心理模型更符合语言边界（FFI）工作的本质。如果我们不这样做，并假设在API级别透明地转换这些类型的工作量，我们可能会因我们的端或用户的端出错而使调试工作受阻。

在这个阶段，我们有一个包含我们想要CProver验证引擎加载的文件名的C++向量的句柄。为此，我们将使用以下代码片段

// Invoke load_model_from_files and see if the model has been loaded.
if let Err(_) = client.load_model_from_files(vect) {
    eprintln!("Failed to load model from files: {:?}", vect);
    process::exit(1);
}

上面的例子是Rust中的一种称为if let的惯用语 - 它实际上是一个只有一个模式的模式匹配 - 我们不匹配任何其他情况。

我们上面做的事情有两方面

• 我们调用函数load_model_from_files，传递我们之前准备好的C++向量（vect）。值得注意的是，这个函数是通过client.调用的 - 这意味着它将我们在开头初始化的api_session句柄作为第一个参数传递给C++ API端的load_model_from_files。
• 我们处理了从C++端加载模型失败的情况，通过在Rust端捕获错误并打印适当的错误消息然后优雅地退出过程。

插曲：错误处理

cxx.rs（我们用于构建Rust API的FFI桥）允许一种机制，其中C++程序的异常可以转换成Rust Result<>类型，前提是已经建立了适当的基础设施。

if let Err(_) = client.verify_model() {
    eprintln!("Failed to verify model from files: {:?}", vect);
    process::exit(1);
}

let msgs_cpp = cprover_api::get_messages();
let msgs_rust = ffi_util::translate_cpp_vector_to_rust(msgs_cpp);
ffi_util::print_response(msgs_rust);