4

我正在阅读一篇关于C 程序的高效上下文敏感指针分析的论文的强更新部分，但我无法准确理解它的含义。有人可以提供一个例子，特别是对于链接中的这一行：

这极大地提高了我们执行强更新的能力。由于堆块代表在特定上下文中分配的所有存储，我们假设本地分配的堆块永远不会唯一。

4

1 回答 1

5

强更新，弱更新

在静态分析的上下文中，人们试图一次推断程序的所有可能行为，强更新是一种更新（分配）操作，其中被更新的地址是精确已知的。相比之下，写入地址不准确的赋值称为弱更新。

在处理弱更新时，不仅新值可以写入多个位置并且不知道是哪个位置，而且必须考虑每个位置保持其旧值的可能性（因为更新可能发生在其他地方）。

例子

考虑Frama-C 的 value analysis，这是一种高效的上下文敏感指针分析，用于在大多数 Linux 发行版中作为包提供的 C 程序。假设我们正在分析以下程序：

int a, b, c, d, *p, t[5];

int main(int argc, char **argv){
  a = 1; // strong
  p = &b;
  *p = 2; // strong
  if (c & 1) 
    p = &c;
  else
    p = &d;
  *p = 3; // weak

  t[2] = 4; // strong
  t[c & 2] = 5; // weak
}

当用 Frama-C 的价值分析来分析这个例子时，可以得到：

$ frama-c -val t.c
[value] Values at end of function main:
  a ∈ {1}
  b ∈ {2}
  c ∈ {0; 3}
  d ∈ {0; 3}
  p ∈ {{ &c ; &d }}
  t[0] ∈ {0; 5}
   [1] ∈ {0}
   [2] ∈ {4; 5}
   [3..4] ∈ {0}
  __retres ∈ {0}

位置c、d和已成为弱更新的目标t[0]。t[2]它们每个都可以包含一个新值（可能已经写在那里）或一个旧值（当时在那里并且可以保留）。

遭到反对，a并被b强烈更新的对象。众所周知，赋值正在准确地写入这些变量中的每一个，因此无需考虑它们可能保留其旧值的可能性。

在文章的上下文中

关于您引用的确切段落：

关键是要认识到表示唯一指针初始值的扩展参数可以是唯一块，即使该指针在调用上下文中有许多可能的值。由于指针在任何时候只能包含其中一种可能性，因此扩展参数是过程范围内的唯一块。只有当多个位置指向扩展参数并且该参数的实际值不是单个唯一位置时，我们才必须将该参数标记为非唯一。这极大地提高了我们执行强更新的能力。

研究人员的目标是尽可能频繁地使用强更新，因为它更精确。在本段中，他们指出，尽管指针p可能指向几个可能的位置，但如果您为“位置p指向”命名，那么您可以强烈更新该位置。我想这就是他们所说的。

在我的示例程序中，这将允许从*p程序末尾读取并发现它完全包含3，尽管p指向c可能包含0or3或指向d可能包含0or的点3。旧版本的 Frama-C 价值分析使用类似于所描述的技术（如果我理解正确的话）推断此信息，但它太昂贵并且被删除。

于 2012-11-03T08:51:26.393 回答