2

假设我们有以下 C 代码：

int my_main(int x){
    if (x > 5){
        x++;
        if (x > 8){
            x++;
            if (x < 15){
                //@(x >= 9 && x <= 14);
            }
        }   
    }
    return 0;
}

我想在初始化时使用静态分析计算变量 x 的边界，从而得到满足的谓词。在这个例子中，main 开头的 x 的间隔应该是 [8, 12]。

TL;DR：给定代码中某处的断言，计算这些范围的最佳方法是什么？

到目前为止我尝试了什么：

我认为解决这个问题的最佳方法是使用最弱的前提条件计算器。我尝试过使用 frama-c 的 wp 插件，但由于它是为验证目的而构建的，我不确定它在这个用例中有多有用。在以下代码上应用插件时：

int main(void){
    int n = 0;
    int x;

    if (x > 5){
        x++;
        if (x > 8){
            x++;
            if (x < 15){
                n = x;
            }
        }   
    }
    //@ assert p: n >= 9 && n <= 14;
    return 0;
}

我收到以下谓词发送到 alt-ergo 求解器：

  goal main_assert_p:
    forall i_1,i : int.
    is_sint32(i) ->
    is_sint32(i_1) ->
    (((i < 6) -> (0 = i_1)) and
     (**(6 <= i)** ->
      (((i < 8) -> (0 = i_1)) and
       (**(8 <= i)** ->
        (((12 < i) -> (0 = i_1)) and (**(i <= 12)** -> (i_1 = (2 + i)))))))) ->
    ((9 <= i_1) and (i_1 <= 14))

如果您仔细观察，可以通过遵循变量 i 上不会导致 (i_1 = 0) 的边界来识别输入所需的间隔。我已经标记了这些界限。这不是很健壮，例如，如果断言更改为&& n <= 13，则隐含谓词的“左侧”保持不变，因为没有任何条件改变。另外我不确定这在其他情况下有多大用处，例如在调用函数时将我的断言更改为 requires 语句，我无法理解生成的谓词：

if (x < 15){
      sum(x);
}

并向函数添加 requires 语句：

//@requires (n >= 6 && n <= 11);
int sum(int n){

我得到：

    goal main_call_sum_pre:
  forall i : int.
  (6 <= i) ->
  (8 <= i) ->
  (i <= 12) ->
  is_sint32(i) ->
  is_sint32(1 + i) ->
  is_sint32(2 + i) ->
  ((4 <= i) and (i <= 9))
4

2 回答 2

3

你是对的，基于“最弱前提”范式的 WP（或 Jessie）是在这里使用的正确工具。然而，他们所做的是构建含义：

规范给出的前提条件 ==> 计算出的最弱前提条件

然后外部证明者尝试证明上述含义，（在一般情况下）仅提供真/假/超时答案。

您可以通过反复试验来做到这一点，使用“LOWER_BOUND ≤ x ≤ UPPER_BOUND”作为user_input(*) 的后置条件，并查看其含义是否得到证明。使用您作为黑匣子所拥有的工具，您将通过几个步骤通过二分法到达区间。您永远不会知道您是否有最佳间隔，或者证明者是否只是不再能够证明仍然持有的财产，但这就是生活。

或者你可以让证明者为你做简化工作，但这需要一种更复杂的交互，而不仅仅是“这个属性是真的吗？”。一些证明者会让您比其他人更容易访问该信息。这一切都在证明者手中，真的，在 WP 完成工作之后，你的问题实际上是关于“一个将逻辑公式简化为x使公式为真的界限的证明者”，而不是关于 Frama-C。

这项研究在某些地方涉及“给我最好的间隔”的问题。它是关于浮点的，但由于浮点比整数更难推理，因此那里使用的工具和技术也可能适用于您的问题。特别是，“Gappa”证明器，其专长是浮点，可以在本地处理区间，而 IIRC 是在该研究中在必要时提供“最佳”区间的证明器（第 11 页，“例如，我们如何在我们的说明性示例中确定界限 1/16？”）

(*) 请注意，在添加调用以user_input()澄清含义之后，您要查找的实际上是该函数的后置条件，而不是主函数的前置条件。

于 2016-02-09T10:40:42.750 回答
-1

assert接受一个布尔表达式和 if FALSE，用一条消息中止应用程序。assert通常是一个宏，在程序的非调试版本中，对这些宏的调用在预处理过程中会被删除。

您的布尔表达式包含常量。如果你用变量替换它们，那么你就有了灵活的断言。

于 2016-02-09T10:29:15.343 回答