在 Z3 上建模内存访问

Question

我正在使用 Z3 对程序的内存访问进行建模，但我对想要分享的性能存有疑问。

我想以一种紧凑的方式进行建模，例如：

memset(dst, 0, 1000);

我的第一次尝试是使用数组理论，但这意味着要么创建一千个类似 (assert (and (= (select mem 0) 0) (= (select mem 1) 0) ... 的术语，要么创建一千个类似的商店或一个量化公式：

(forall (x Int) (implies (and (>= x 0) (< x 1000)) (= (select mem x) 0))

但有人告诉我在使用数组时要避免使用量词。

下一个想法是定义一个 UF：

 (define-fun newmemfun ((idx Int)) Int (
   ite (and (>= idx 0) (< idx 1000)) 0 (prevmemfun idx)
 ))

但这意味着我需要为每个内存写入操作定义一个新函数（即使是单独的存储操作，而不仅仅是像 memset 或 memcpy 这样的多个存储）。这最终会创建一个非常嵌套的 ITE 结构，甚至可以为同一索引保存“旧”值。即：

mem[0] = 1;
mem[0] = 2;

would be:
(ite (= idx 0) 2 (ite (= idx 0) 1 ...

这在功能上是正确的，但表达式的大小（我猜为它生成的 AST）往往会快速累积，我不确定 Z3 是否经过优化以检测和处理这种情况。

所以，问题是：编码内存操作的最佳性能方式是什么，可以同时处理像上面的示例这样的大型多个存储和单个存储。

谢谢， 巴勃罗。

PS：非封闭且不匹配的括号旨在：P。

Answer 1

如果不了解您的最终目标，除了对内存访问进行建模（例如，您是否要进行验证、测试用例生成等？），这有点难以回答，因为您有很多选择。但是，如果您依赖其中一个 API，您可能最灵活地控制性能问题。例如，您可以如下定义自己的内存访问（z3py 脚本链接：http://rise4fun.com/Z3Py/gO6i）：

address_bits = 7
data_bits = 8

s = Solver()

# mem is a list of length program step, of a list of length 2^address_bits of bitvectors of size 2^data_bits
mem =[]

# modify a single address addr to value at program step step
def modifyAddr(addr, value, step):
  mem.append([]) # add new step
  for i in range(0,2**address_bits):
    mem[step+1].append( BitVec('m' + str(step + 1) + '_' + str(i), data_bits) )

    if i != addr:
      s.add(mem[step+1][i] == mem[step][i])
    else:
      s.add(mem[step+1][i] == value)

# set all memory addresses to a specified value at program step step
def memSet(value, step):
  mem.append([])
  for i in range(0,2**address_bits):
    mem[step+1].append( BitVec('m' + str(step + 1) + '_' + str(i), data_bits) )
    s.add(mem[step+1][i] == value)

modaddr = 23 # example address
step = -1
# initialize all addresses to 0
memSet(0, step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]] # print all step values for modaddr

modifyAddr(modaddr,3,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

modifyAddr(modaddr,4,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

modifyAddr(modaddr,2**6,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

memSet(1,step)
step += 1
print s.check()
for i in range(0,step+1): print s.model()[mem[i][modaddr]]

for a in range(0,2**address_bits): # set all address values to their address number
  modifyAddr(a,a,step)
  step += 1

print s.check()
print "values for modaddr at all steps"
for i in range(0,step+1): print s.model()[mem[i][modaddr]] # print all values at each step for modaddr

print "values at final step"
for i in range(0,2**address_bits): print s.model()[mem[step][i]] # print all memory addresses at final step

这种简单的实现允许您 (a) 将所有内存地址设置为某个值（如您的 memset），或 (b) 修改单个内存地址，将所有其他地址限制为具有相同的值。对我来说，运行和编码大约 128 个步骤的 128 个地址需要几秒钟，所以它有大约 20000 个 8 位的位向量表达式。

现在，根据您正在做的事情（例如，您是否允许像这个 memset 一样对多个地址进行原子写入，还是要将它们全部建模为单独的写入？），您可以添加更多功能，例如修改子集程序步骤中某些值的地址。这将使您能够灵活地权衡建模准确性与性能（例如，原子写入内存块与一次修改单个地址，这将遇到性能问题）。此外，此实现不需要 API，您也可以将其编码为 SMT-LIB 文件，但如果您使用，您可能会有更大的灵活性（例如，假设您想与模型交互以约束未来的 sat 检查） API 之一。