Определение битовых векторов в Z3 с использованием фиксированных символов - PullRequest
Новая
       8

Определение битовых векторов в Z3 с использованием фиксированных символов

0 голосов
/ 17 декабря 2018

Можем ли мы определить наш вход BitVec () в Z3 таким образом, чтобы мы знали часть ввода, а другую часть, которую мы хотим, чтобы Z3 решал?

Например, в приведенном ниже коде яя определяю битовый вектор для представления строки из 10 символов. 

from z3 import *

s = Solver()

input = [BitVec("input%s" % i, 8) for i in range(10)]

s.add(gen(input) == 0xAABBCCDD)

В приведенном выше примере gen () - это функция, которая генерирует DWORD с использованием ввода.

Теперь давайтескажем, я уже знаю первые несколько символов ввода.Например, ввод всегда имеет формат: CHECKXXXXX

, где X - неизвестные символы.

Как теперь определить вход в Z3, чтобы использовать преимущества известных символов?

1 Ответ

0 голосов
/ 17 декабря 2018

Конечно.Так как вы генерируете символьный ввод для каждого символа ввода, просто добавьте соответствующее утверждение для известных вам элементов: 

from z3 import *

s = Solver()

input = [BitVec("input%s" % i, 8) for i in range(10)]

known = "CHECK"
s.add([input[i] == ord(known[i]) for i in range(len(known))])

print s.check()
print s.model()

Это напечатает: 

sat
[input4 = 75,
 input3 = 67,
 input2 = 69,
 input1 = 72,
 input0 = 67]

, что точночто ты хотел.Теперь вы можете вызвать функцию gen и дополнительно ограничить другие части input, чтобы получить полную модель.

В качестве альтернативы, вы можете использовать функцию BitVecVal, чтобы напрямую создавать постоянные битовые векторы, иВо-первых, не стоит создавать символические варианты: https://z3prover.github.io/api/html/namespacez3py.html#a74d306d60d4cc4432907f58306b41686 Но я думаю, что использование чисто символических входов и добавление ограничений более приятное, потому что это упрощает программирование.Мельчайшая экономия производительности, если не создавать символические переменные, вряд ли стоила бы этого.

...