Paths

ExecutionManager 类似于函数 foo 中的 路径 迭代器。每条路径都是可能导致函数返回某些值的控制流决策的可能序列（例如，在每次 if 语句中我们选择哪个方向）。在这个示例中，函数 foo 有两条路径，一条是“true”分支，另一条是“false”分支。

让我们检查通过函数的第一条路径

let result = em.next().expect("Expected at least one path");

在常见情况下，result 包含此路径上的函数返回值，作为 Boolector BV（位向量）封装在 ReturnValue 枚举中。由于我们知道 foo 不是一个空类型函数（并且不会抛出异常或中止），我们可以简单地解包 ReturnValue 以获取 BV

let retval = match result {
    Ok(ReturnValue::Return(r)) => r,
    Ok(ReturnValue::ReturnVoid) => panic!("Function shouldn't return void"),
    Ok(ReturnValue::Throw(_)) => panic!("Function shouldn't throw an exception"),
    Ok(ReturnValue::Abort) => panic!("Function shouldn't panic or exit()"),
    ...

result 也可以是一个 Err，描述了在处理路径时遇到的 Error。在这种情况下，我们可以忽略错误并继续调用 next() 来尝试找到没有错误的路径。或者，我们可以这样获取有关错误的信息：

    ...
    Err(e) => panic!("{}", em.state().full_error_message_with_context(e)),
};

这将从程序 State 中获取错误信息，我们将在下一节讨论。但在本教程的其余部分，我们将假设我们得到了 Ok 的结果，此时 retval 是表示第一个路径上函数返回值的 BV。

状态

对于每条路径，ExecutionManager 不仅提供路径的最终结果（要么是 ReturnValue，要么是 Error），还提供该路径末尾的最终程序 State。我们可以使用 state() 获取对 State 的不可变访问，或者使用 mut_state() 获取可变访问。

let state = em.mut_state();  // the final program state along this path

要测试在这个 State 中 retval 是否可以等于 0，我们可以使用 state.bvs_can_be_equal()

let zero = state.zero(32);  // The 32-bit constant 0
if state.bvs_can_be_equal(&retval, &zero)? {
    println!("retval can be 0!");
}

获取变量的解

如果 retval 可以等于 0，让我们找出哪些函数参数的值会导致这种情况。首先，我们将向 State 添加一个约束，要求返回值必须是 0

retval._eq(&zero).assert();

然后我们将根据这个约束请求每个参数的解

// Get a possible solution for the first parameter.
// In this case, from looking at the text-format LLVM IR, we know the variable
// we're looking for is variable #0 in the function "foo".
let a = state.get_a_solution_for_irname(&String::from("foo"), Name::from(0))?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

// Likewise the second parameter, which is variable #1 in "foo"
let b = state.get_a_solution_for_irname(&String::from("foo"), Name::from(1))?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

println!("Parameter values for which foo returns 0: a = {}, b = {}", a, b);

或者，我们也可以像这样从 ExecutionManager 获取参数的 BV：

let a_bv = em.param_bvs()[0].clone();
let b_bv = em.param_bvs()[1].clone();

let a = em.state().get_a_solution_for_bv(&a_bv)?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

let b = em.state().get_a_solution_for_bv(&b_bv)?
    .expect("Expected there to be a solution")
    .as_u64()
    .expect("Expected solution to fit in 64 bits");

println!("Parameter values for which foo returns 0: a = {}, b = {}", a, b);

文档

有关 haybale 的完整文档可以在 docs.rs 上找到，或者当然，您可以使用 cargo doc --open 生成本地文档。

兼容性

目前，haybale 的官方 crates.io 版本（0.7.0 及以后）依赖于 Boolector 3.2.1 和 LLVM 9、10、11、12、13 或 14，通过功能标志 llvm-9 到 llvm-14 选择。截至本文写作时，选择 LLVM 版本对 haybale 的功能或接口几乎没有影响；唯一的区别是能够分析使用较新 LLVM 生成的基本代码。（并且 LLVM 10+ 版本可以处理 AtomicRMW 指令；参见 #12。）