ord() 函数或字符串的 ASCII 字符代码与 Z3 求解器

Question

如何将 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 中有什么东西可以吗？

Answer 1

2022 年更新

以下答案，写于 2018 年，不再适用；由于 SMTLib 中的字符串收到了重大更新，因此给出的代码已过时。将它保存在这里用于存档目的，以防万一您碰巧有一个非常旧的 z3，由于某种原因您无法升级。请参阅另一个答案，了解适用于 SMTLib 中新 unicode 字符串的变体：

2018 年的旧答案

您将 Python 字符串和 Z3 字符串混为一谈；不幸的是，这两者是完全不同的类型。

在 Z3py 中，String 只是一个 8 位值的序列。 Z3 能做的实际上非常有限；例如，您不能像在 add_ascii_values 函数中那样遍历字符。请参阅此页面以了解允许的函数是什么：https://rise4fun.com/z3/tutorialcontent/sequences（此页面列出了 SMTLib 术语中的函数；但等效函数可从 z3py 界面获得。）

在使用 Z3 序列和字符串时，您需要牢记一些重要的 restrictions/things：

你必须非常明确地说明长度；特别是，您不能 sum 处理任意符号长度的字符串。在不明确指定长度的情况下，您可以做一些事情，但这些事情是有限的。（如正则表达式匹配、子字符串提取等）
您不能从字符串中提取字符。我认为这是一个疏忽，但 SMTLib 暂时没有办法这样做。相反，您会得到一个长度为 1 的列表。这会在编程中引起很多麻烦，但有一些解决方法。见下文。
任何时候你在 string/sequence 上循环时，你都必须达到一个固定的界限。有一些编程方法可以覆盖“所有长度为 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的字符串；但为什么 ord 的总和不等于 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 本身的对象完全不同。请注意，sequence/string 逻辑甚至还没有被 SMTLib 人员标准化，因此情况可能会发生变化。（特别是，我希望他们能添加在索引处提取元素的功能！）。

说了这么多，复习一下 https://rise4fun.com/z3/tutorialcontent/sequences 将是熟悉它们的良好开端，并随时提出更多问题。

Answer 2

接受的答案可以追溯到 2018 年，同时情况发生了变化，这使得建议的解决方案不再适用于 z3。特别是：

字符串现在由 SMTLib 规范化。（参见 https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml）
与以前的版本（字符串只是位向量序列）不同，字符串现在是 unicode 字符序列。因此，先前答案中使用的编码不再适用。

基于此，假设密码长度为 3，下面是如何对这个问题进行编码：

from z3 import *

s = Solver()

# Ord of character at position i
def OrdAt(inp, i):
    return StrToCode(SubString(inp, i, 1))

# Adding ascii values for a string of a given length
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 = 3
password = String("password")
s.add(Length(password) == length)
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])

注意由于 https://github.com/Z3Prover/z3/issues/5773，为了能够运行以上内容，您需要在 2022 年 1 月 12 日下载的 z3 版本或之后！截至目前，none 的 z3 发布版本包含此答案中使用的功能。

当运行时，上面打印：

sat
" #!"

您可以检查它是否满足给定的约束条件，即字符的顺序加起来为 100：

>>> sum(ord(c) for c in " #!")
100

请注意，我们不再需要担心模运算，因为 OrdAt returns 是一个实际的整数，而不是位向量。

ord() 函数或字符串的 ASCII 字符代码与 Z3 求解器

ord() Function or ASCII Character Code of String with Z3 Solver

z3

z3py

python-3.4

2022 年更新

2018 年的旧答案