ord () Функция или ASCII символьный код строки с помощью Z3 Solver - PullRequest
Новая
       22

ord () Функция или ASCII символьный код строки с помощью Z3 Solver

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

Как я могу преобразовать z3.String в последовательность значений ASCII?

Например, вот некоторый код, который, как я думал, проверит, складываются ли значения ASCII всех символов в строке до100: 

import z3

def add_ascii_values(password):
    return sum(ord(character) for character in password)

password = z3.String("password")
solver = z3.Solver()
ascii_sum = add_ascii_values(password)
solver.add(ascii_sum == 100)

print(solver.check())
print(solver.model())

К сожалению, я получаю эту ошибку: 

TypeError: ord() expected string of length 1, but SeqRef found

Очевидно, что ord не работает с z3.String.Есть ли что-то в Z3, что делает?

1 Ответ

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

Вы объединяете строки Python и строки Z3;и, к сожалению, эти два типа совершенно разные.

В Z3py String - это просто последовательность 8-битных значений.А то, что вы можете сделать с Z3, на самом деле весьма ограничено;например, вы не можете перебирать символы, как в своей функции add_ascii_values.На этой странице приведены допустимые функции: https://rise4fun.com/z3/tutorialcontent/sequences (на этой странице перечислены функции на языке SMTLib; но эквивалентные функции доступны через интерфейс z3py.)

Есть несколько важных ограничений/ вещи, которые вы должны иметь в виду при работе с последовательностями и строками Z3:

  • Вы должны очень четко указывать длину;В частности, вы не можете sum для строк произвольной символьной длины.Есть несколько вещей, которые вы можете сделать без указания длины явно, но они ограничены.(Подобно совпадениям с регулярным выражением, извлечению подстроки и т. Д.)

  • Вы не можете извлечь символ из строки.На мой взгляд, это упущение, но пока у SMTLib просто нет возможности сделать это.Вместо этого вы получите список длины 1. Это вызывает много головной боли в программировании, но есть обходные пути.См. Ниже.

  • Каждый раз, когда вы перебираете строку / последовательность, вы должны подняться до фиксированной границы.Есть способы программирования, так что вы можете покрыть «все строки до длины N» для некоторой константы «N», но они становятся волосатыми.

Имея все это в виду, я быперейдите к кодированию вашего примера, как показано ниже;ограничение password длиной до 10 символов: 

from z3 import *

s = Solver()

# Work around the fact that z3 has no way of giving us an element at an index. Sigh.
ordHelperCounter = 0
def OrdAt(inp, i):
    global ordHelperCounter
    v = BitVec("OrdAtHelper_%d_%d" % (i, ordHelperCounter), 8)
    ordHelperCounter += 1
    s.add(Unit(v) == SubString(inp, i, 1))
    return v

# Your original function, but note the addition of len parameter and use of Sum
def add_ascii_values(password, len):
    return Sum([OrdAt(password, i) for i in range(len)])

# We'll have to force a constant length
length = 10
password = String("password")
s.add(Length(password) == 10)
ascii_sum = add_ascii_values(password, length)
s.add(ascii_sum == 100)

# Also require characters to be printable so we can view them:
for i in range(length):
  v = OrdAt(password, i)
  s.add(v >= 0x20)
  s.add(v <= 0x7E)

print(s.check())
print(s.model()[password])

Функция OrdAt решает проблему невозможности извлечения символов.Также обратите внимание, как мы используем Sum вместо sum и как все «циклы» имеют фиксированный счетчик итераций.Я также добавил ограничения для удобства печати всех кодов ascii.

Когда вы запустите это, вы получите: 

sat
":X|@`y}@@@"

Давайте проверим, что это действительно хорошо: 

>>> len(":X|@`y}@@@")
10
>>> sum(ord(character) for character in ":X|@`y}@@@")
868

Итак, мы получили строку длиной 10;но как получается, что орды не составляют до 100?Теперь вы должны помнить, что последовательности состоят из 8-битных значений, и, следовательно, арифметика выполняется по модулю 256. Таким образом, сумма на самом деле: 

>>> sum(ord(character) for character in ":X|@`y}@@@") % 256
100

Чтобы избежать переполнений, вы можете использовать большеебитовые векторы или, проще говоря, использовать неограниченный тип целого числа Z3 Int.Для этого используйте функцию BV2Int, просто изменив add_ascii_values на: 

def add_ascii_values(password, len):
    return Sum([BV2Int(OrdAt(password, i)) for i in range(len)])

Теперь мы получим: 

unsat

Это потому, что каждый из наших персонажей имеетпо крайней мере, значение 0x20, и мы хотели 10 символов;таким образом, нет никакого способа сделать их всех до 100. И z3 точно говорит нам об этом.Если вы увеличите целевую сумму до чего-то более разумного, вы начнете получать правильные значения.

Программирование с использованием z3py отличается от обычного программирования с использованием Python, а объекты z3 String сильно отличаются от объектов самого Python.,Обратите внимание, что последовательность / строковая логика еще даже не стандартизирована людьми SMTLib, поэтому все может измениться.(В частности, я надеюсь, что они добавят функциональность для извлечения элементов по индексу!).

Сказав все это, переход на https://rise4fun.com/z3/tutorialcontent/sequences будет хорошим началом для ознакомления с ними и не стесняйтесь задавать дополнительные вопросы.

...