4

我正在使用 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 结构，甚至可以为同一索引保存“旧”值。IE：

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

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

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

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

谢谢，巴勃罗。

PS：非封闭和不匹配的括号意为：P。

4

1 回答 1

2

在不了解您的最终目标的情况下，除了对内存访问进行建模（例如，您是否要进行验证、测试用例生成等？），这有点难以回答，因为您有很多选择。但是，如果您依赖其中一个 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 文件，但如果使用API 之一。

于 2012-11-26T20:46:08.933 回答