int ct(int x, int y, int option) {
    volatile int z[3] = { 0, 2, 300 };
    z[2] = y;
    if (option > 3) {
        return z[1];
    } else {
        return z[x % 3];
    }
}

如果我们使用上面给出的注释来分析这个函数，pitchfork会（正确地）报告一个常数时间违规，因为z[x % 3]使用了一个依赖于秘密数据的数组索引。

但是，让我们假设我们只对分析option值为5的情况感兴趣。我们可以用AbstractData来这样表达

println!("{}", check_for_ct_violation(
    "ct",
    &project,
    Some(vec![
        AbstractData::secret(),
        AbstractData::secret(),
        AbstractData::pub_i32(AbstractValue::ExactValue(5)),
    ]),
    &StructDescriptions::new(),
    Config::default(),
    &PitchforkConfig::default(),
));

这里我们使用AbstractData::pub_i32()来指定一个公共32位整数，并使用AbstractValue::ExactValue(5)来赋予这个整数确切的值5。这意味着分析只会考虑该参数值为5的情况，结果会报告该函数没有常数时间违规。

ExactValue在函数参数指定像输入数组长度这样的东西时也很有用，而你只想在分析中考虑特定的数组长度。有关指定参数值的其他方法，请参阅AbstractValue的文档。

作为一个旁注，请注意，您不能指定标记为秘密的东西的值。这是因为标记为秘密的任何东西的值对于符号分析来说并不重要。事实上，如果标记为秘密的某物的值对于分析很重要（例如，确定哪些路径是有效的，或者哪个内存地址被加载），那么这已经是一个常数时间违规，因为这意味着秘密值已经影响了分支条件或内存地址。

指向秘密数据数组的指针

假设我们有一个C函数，它接受一个指向32个秘密整数的数组的指针，并将1加到数组的每个元素上

uint32_t secret_array(uint32_t* arr) {
    for (int i = 0; i < 32; i++) {
        arr[i] += 1;
    }
    return arr[0];
}

为arr使用AbstractData::secret()可能不会按预期工作

println!("{}", check_for_ct_violation(
    "secret_array",
    &project,
    Some(vec![AbstractData::secret()]),
    &StructDescriptions::new(),
    Config::default(),
    &PitchforkConfig::default(),
));

这个函数看起来没有问题，但pitchfork会报告一个常数时间违规！这是因为它将secret应用于参数本身，在这个例子中是一个指针。由于指针值arr是秘密的，因此访问arr[i]的结果是一个依赖于指针arr的秘密值的地址。

相反，我们可以告诉pitchfork，arr本身（指针）是公开的，但它指向一个秘密数据的数组

AbstractData::pub_pointer_to(AbstractData::array_of(AbstractData::secret(), 32))

我们还需要提高“循环界限”，默认值为10（截至本文撰写时）。（有关更多详细信息，请参阅有关Config.loop_bound的文档。）

let mut config = Config::default();
config.loop_bound = 100;
// then pass this `config` to `check_for_ct_violation()`

现在，pitchfork应该验证函数是否是常数时间的。

有关数组的更多约束

以下C函数接收两个数组的指针：包含公共值的数组 public_arr，其长度为 public_arr_len，以及包含秘密值的数组 secret_arr，长度为32。假设 public_arr_len 和 i 也是公开的 - 唯一的秘密值在 secret_arr 中。

uint32_t secret_array_var_length(uint32_t* public_arr, uint32_t public_arr_len, uint32_t* secret_arr, uint32_t i) {
    uint32_t x = public_arr[i];
    for (int j = 0; j < 32; j++) {
        secret_arr[j] += x;
    }
    if (x > 10) {
        return public_arr[0] + secret_arr[0];
    } else {
        return public_arr[1] + secret_arr[1];
    }
}

如果我们像这样检查该函数的常量时间违规行为...

println!("{}", check_for_ct_violation(
    "secret_array_var_length",
    &project,
    Some(vec![
        AbstractData::default(),
        AbstractData::default(),
        AbstractData::pub_pointer_to(AbstractData::array_of(AbstractData::secret(), 32)),
        AbstractData::default(),
    ]),
    &StructDescriptions::new(),
    config,  // with loop_bound set to 100 as above
    &PitchforkConfig::default(),
));

...我们会发现 pitchfork 报告了一个常量时间违规。具体来说，如果 i 太大，public_arr[i] 实际上会从 secret_arr（在 public_arr 的末尾）加载秘密数据，然后用于分支条件。

在这种情况下，只要调用者传递一个在范围内 i，函数实际上是安全的。为了仅分析 i 在范围内的情况，我们可以为 public_arr 指定一个最大长度（在这个例子中，让我们假设72个元素），并将 public_arr_len 和 i 都约束在这个最大长度内

println!("{}", check_for_ct_violation(
    "secret_array_var_length",
    &project,
    Some(vec![
        AbstractData::pub_pointer_to(AbstractData::array_of(AbstractData::default(), 72)),
        AbstractData::pub_i32(AbstractValue::Range(0, 72)),
        AbstractData::pub_pointer_to(AbstractData::array_of(AbstractData::secret(), 32)),
        AbstractData::pub_i32(AbstractValue::Range(0, 71)),
    ]),
    &StructDescriptions::new(),
    config,  // with loop_bound set to 100 as above
    &PitchforkConfig::default(),
));

有了这些注释，pitchfork 将验证在给定这些假设的情况下函数是常量的。

注意关于此函数的两个额外事项：首先，我们可以在不知道其实际长度的情况下选择一个较大的 public_arr 最大长度。假设数组的大小并不会真的造成伤害：pitchfork 将为该数组“分配”额外的内存，但该内存将不会被使用，并且（很可能）不会影响分析。其次，上述分析仍将考虑 i > public_arr_len 的输入；只是上面的函数在这些情况下仍然是常量的，因为我们假设 i 在 public_arr 实际分配的大小内（72，尽管 public_arr_len 可能更小）。如果我们想考虑那些同时满足 i < public_arr_len 的案例，我们可以用这个用于 public_arr_len

AbstractData::pub_i32(AbstractValue::named("public_arr_len", AbstractValue::Range(0, 72)))

和这个用于 i

AbstractData::pub_i32(AbstractValue::UnsignedLessThan("public_arr_len".into()))

您可能会想知道当我们使用 AbstractData::default() 时，pitchfork 首先对 public_arr 做了什么假设。答案是它假设了一个长度为 AbstractData::DEFAULT_ARRAY_LENGTH 的数组（截至本文写作时为1024）。有关 default() 的精确行为的更多详细信息，请参阅有关 AbstractData::default() 的文档。

包含秘密数据的结构体

让我们考虑这个C函数

uint32_t uses_a_struct(Context* ctx, uint32_t* public_input, uint32_t* public_output) {
    for (int i = 0; i < 32; i++) {
        public_output[i] = public_input[i] ^ ctx->secret_key;
    }
    if (ctx->public_option) {
        return public_output[0];
    } else {
        return public_output[1];
    }
}

其中，Context 结构体定义为

typedef struct {
    uint32_t public_option;
    uint32_t another_thing;
    uint32_t secret_key;
} Context;

我们希望指定 ctx 参数指向一个包含一些秘密数据（secret_key）和一些公共数据（public_option）的结构体。我们可以使用 AbstractData::_struct 来实现这一点

println!("{}", check_for_ct_violation(
    "uses_a_struct",
    &project,
    Some(vec![
        AbstractData::pub_pointer_to(AbstractData::_struct("Context", vec![
            AbstractData::default(),  // public_option
            AbstractData::default(),  // another_thing
            AbstractData::secret(),   // secret_key
        ])),
        AbstractData::default(),  // public_input
        AbstractData::default(),  // public_output
    ]),
    &StructDescriptions::new(),
    config,  // with loop_bound set to 100 as above
    &PitchforkConfig::default(),
));

有了这个描述，pitchfork 应该能够正确报告该函数是常量的。

另一种实现相同功能的方法——如果存在多个Context结构体或者有其他结构体包含指向Context结构体的指针等，这种方法将更有用——是通过StructDescriptions。我们可以向pitchfork提供一个Context结构体的描述。

let sd: StructDescriptions = vec![
    ("struct.Context".into(), AbstractData::_struct("Context", vec![
        AbstractData::default(),  // public_option
        AbstractData::default(),  // another_thing
        AbstractData::secret(),   // secret_key
    ])),
].into_iter().collect();

然后，当我们使用AbstractData::default()时，它将自动考虑我们在StructDescriptions参数中给出的Context结构体的描述。

println!("{}", check_for_ct_violation(
    "uses_a_struct",
    &project,
    Some(vec![
        AbstractData::default(),  // ctx
        AbstractData::default(),  // public_input
        AbstractData::default(),  // public_output
    ]),
    &sd,
    config,  // with loop_bound set to 100 as above
    &PitchforkConfig::default(),
));

此外，它遇到的任何其他作为相同或不同参数的Context结构体也将使用这个描述。

使用Pitchfork的main_func

Pitchfork还提供了一个带有众多命令行选项的main_func()，用于对您选择的库进行恒时检查。您只需提供您的Project、StructDescriptions、Config等，然后在您的main()中调用main_func()即可。