Моделирование доступа к памяти на Z3

Не зная немного больше о вашей конечной цели, помимо моделирования доступа к памяти (например, собираетесь ли вы выполнять проверку, генерацию тестового примера и т. д.?), довольно сложно ответить, так как у вас есть много вариантов. Однако у вас может быть наибольшая гибкость для управления проблемами производительности, если вы полагаетесь на один из 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

Эта наивная реализация позволяет вам либо (а) установить для всех адресов памяти какое-то значение (например, ваш memset), либо (б) изменить один адрес памяти, ограничивая все остальные адреса, чтобы они имели одно и то же значение. Для меня это заняло несколько секунд, чтобы запустить и закодировать около 128 шагов по 128 адресов, поэтому у него было около 20000 выражений битового вектора по 8 бит каждое.

Теперь, в зависимости от того, что вы делаете (например, разрешаете ли вы атомарную запись по нескольким адресам, таким как этот memset, или хотите смоделировать их все как отдельные записи?), вы можете добавить дополнительные функции, например, изменить подмножество адресов на некоторые значения в шаге программы. Это даст вам некоторую гибкость в обмене точностью моделирования на производительность (например, атомарная запись в блоки памяти вместо изменения отдельных адресов за раз, что приведет к проблемам с производительностью). Кроме того, ничто в этой реализации не требует API-интерфейсов, вы также можете закодировать это как файл SMT-LIB, но у вас, вероятно, будет больше гибкости (например, скажем, вы хотите взаимодействовать с моделями, чтобы ограничить будущие проверки спутников), если вы используете один из API.