您将如何在 z3 中实现指针的取消引用

【问题标题】：How would you implement dereferencing of pointers in z3您将如何在 z3 中实现指针的取消引用
【发布时间】：2017-08-15 10:05:55
【问题描述】：

尝试在python中用z3分析一些C程序，遇到了指针问题。我正在使用以下术语：

float * buffer = (float*)malloc(5*sizeof(float))

我将缓冲区解释为BitVec(32) 值所以*buffer 应该是Real()。应该没问题，但是我应该为

之类的术语写什么断言

*(buffer+3) or *(buffer+i)

如果我像索引一样，应该如何编写断言

*(buffer-1) or *(buffer+10)

【问题讨论】：

如果你用 C 语言编程，那么只使用那个标签。不要使用不相关的标签（语言或其他）发送垃圾邮件。
另外，在 C 语言中，没有必要强制转换 malloc 的返回值 - 它只能屏蔽错误。

标签： c z3 z3py

【解决方案1】：

一种解决方案是将程序堆编码为从位置到值的映射H。在 Z3 中，数组理论可用于对地图进行编码。

指针/地址是整数位置，整数算术编码指针算术；这将允许在您的编码中使用诸如H(buffer + i) > 0 之类的约束。如果要对 OO 语言进行编码，则可以使用对 (receiver, field name) 对地址进行编码。例如。 H(r, f) > 0 将对应于 r.f > 0。请注意，此地图编码自然会考虑混叠，例如如果buffer1 == buffer2 和i == 3 然后H(buffer1 + i) == H(buffer + 3)。

请参阅论文Heaps and Data Structures: A Challenge for Automated Provers，了解基于映射的堆编码的有趣比较。

基于地图的编码通常由基于验证条件的工具使用，例如Frama-C、Dafny 和Boogie。基于符号执行的工具，例如Silicon（它是Viper verification infrastructure 的一部分）和VeriFast 通常使用不同的编码；见，例如Heap-Dependent expressions in separation logic.

【讨论】：