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

Можем ли мы определить наш вход 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, чтобы воспользоваться известными символами?


python z3 z3py
person Neon Flash    schedule 17.12.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

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 Но я думаю, что это ограничивает ввод с чистыми символами ввода программирование. Незначительная экономия производительности, связанная с отсутствием создания символических переменных, вряд ли того стоит.

person alias    schedule 17.12.2018
comment
Спасибо за ваш ответ :) - person Neon Flash; 18.12.2018