表达式的反向分析

Question

假设我在 C 中有以下代码段。

i = j = k = 1;

j = (i++) + (++k);

result = i + j + k; //POI
//Expected result = 7

这里，我想通过反向分析找到result的值。当我进行反向分析时，我将按顺序遍历以下表达式。

j = (i++) + (++k);
++k;
i++;
i = j = k = 1;
j = k = 1;
k = 1;

在反向分析过程中，只要适用，我将用相应的表达式替换每个变量。但是我很困惑如何处理 increment/decrement 操作。

我目前的策略会产生以下结果

result = i + j + k

//after j = i++ + ++k
result = (i+(i+(k+1)))+k

//after ++k
result = (i+(i+((k+1)+1)))+(k+1)

//after i++
result = ((i+1)+((i+1)+((k+1)+1)))+(k+1)

//after i = j = k = 1
result = ((1+1)+((1+1)+((k+1)+1)))+(k+1)

//after k = 1
result = (((1+1)+((1+1)+((1+1)+1)))+(1+1))

//Simplifying
result = 9

这当然不是真的。

谁能帮我解决这个问题？

Answer 1

这里要注意的是 i++ 在评估之后增加，而不是之前。

i=j=k=1
++k  //happens before expression
//k=2,i=j=1
j = k + i 
//k=2,i=1,j=3
i++ //happens after expression
//k=2,i=2,j=3
result = i+ j + k
//result = 7

你的错误是在计算 j 之前增加 i，然后得到 j=4，而不是 j=3

如果你想向后分析，可以参考

result = i + j + k
i = i+1 = 1 + 1
//result = (1+1) + j + k
j = i + k 
k = k+1 = 1+1
//j = 1 + (1+1) 
//result = (1+1) + (1+(1+1)) + (1+1)

Answer 2

我觉得应该更像这样

result = i + j + k

//after j = X + Y      // You didn't analyse ++k and i++ yet 
result = i+(X+Y)+k    

//after Y = ++k
result = (i+(X+(k+1))+(k+1)

//after X = i++
result = ((i+1)+(i+(k+1))+(k+1)

//after i = j = k = 1
result = ((1+1)+(1+(k+1))+(k+1)

//after k = 1
result = ((1+1)+(1+(1+1))+(1+1)

//Simplifying
result = 7

Answer 3

我建议您首先像编译器那样将语句分解为基本语句。例如，使用 Frama-C 分解语句会给出如下内容：

k = 1;
j = k;
i = j;
tmp = i;
i ++;
k ++;
j = tmp + k;
result = (i + j) + k;

这样分析起来就容易多了。考虑从底部开始的顺序：

  // 1 + 1 + 1 + 1 + 1 + 1 + 1
k = 1;
  // k + 1 + k + k + 1 + k + 1
j = k;
  // j + 1 + j + k + 1 + k + 1
i = j;
  // i + 1 + i + k + 1 + k + 1
tmp = i;
  // i + 1 + tmp + k + 1 + k + 1
i ++;
  // i + tmp + k + 1 + k + 1
k ++;
  // i + tmp + k + k
j = tmp + k;
  // i + j + k
result = (i + j) + k;
  // result ?

这给了你预期的 7。

表达式的反向分析

Backward Analysis of Expression

c

algorithm

static-analysis