ord() 函数或带有 Z3 求解器的字符串的 ASCII 字符代码 [英] ord() Function or ASCII Character Code of String with Z3 Solver

问题描述

如何将 z3.String 转换为 ASCII 值序列?

例如，下面是一些我认为可以检查字符串中所有字符的 ASCII 值加起来是否为 100 的代码:

导入z3def add_ascii_values(密码):return sum(ord(character) for character in password)密码 = z3.String("密码")求解器 = z3.Solver()ascii_sum = add_ascii_values(密码)solver.add(ascii_sum == 100)打印(求解器.检查())打印(求解器.模型())

不幸的是，我收到此错误:

TypeError: ord() 预期长度为 1 的字符串，但 SeqRef 找到

很明显ord 不适用于z3.String.Z3 中是否有这样的功能?

解决方案

您将 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 = 求解器()# 解决 z3 无法在索引处为我们提供元素的事实.叹.ordHelperCounter = 0def OrdAt(inp, i):全局 ordHelperCounterv = BitVec("OrdAtHelper_%d_%d" % (i, ordHelperCounter), 8)ordHelperCounter += 1s.add(Unit(v) == SubString(inp, i, 1))返回 v# 你原来的函数，但要注意len参数的添加和Sum的使用def add_ascii_values(密码，len):return Sum([OrdAt(password, i) for i in range(len)])# 我们必须强制一个恒定的长度长度 = 10密码 = String("密码")s.add(长度(密码) == 10)ascii_sum = add_ascii_values(密码，长度)s.add(ascii_sum == 100)# 还要求字符是可打印的，以便我们可以查看它们:对于范围(长度)中的 i:v = OrdAt(密码，我)s.add(v >= 0x20)s.add(v <= 0x7E)打印(s.check())打印(s.model()[密码])

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}@@@") % 256100

为了避免溢出，您可以使用更大的位向量，或者更简单地使用 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 将是熟悉它们的良好开端，并随时提出进一步的问题.

How can I convert a z3.String to a sequence of ASCII values?

For example, here is some code that I thought would check whether the ASCII values of all the characters in the string add up to 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())

Unfortunately, I get this error:

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

It's apparent that ord doesn't work with z3.String. Is there something in Z3 that does?

解决方案

You're conflating Python strings and Z3 Strings; and unfortunately the two are quite different types.

In Z3py, a String is simply a sequence of 8-bit values. And what you can do with a Z3 is actually quite limited; for instance you cannot iterate over the characters like you did in your add_ascii_values function. See this page for what the allowed functions are: https://rise4fun.com/z3/tutorialcontent/sequences (This page lists the functions in SMTLib parlance; but the equivalent ones are available from the z3py interface.)

There are a few important restrictions/things that you need to keep in mind when working with Z3 sequences and strings:

• You have to be very explicit about the lengths; In particular, you cannot sum over strings of arbitrary symbolic length. There are a few things you can do without specifying the length explicitly, but these are limited. (Like regex matches, substring extraction etc.)

• You cannot extract a character out of a string. This is an oversight in my opinion, but SMTLib just has no way of doing so for the time being. Instead, you get a list of length 1. This causes a lot of headaches in programming, but there are workarounds. See below.

• Anytime you loop over a string/sequence, you have to go up to a fixed bound. There are ways to program so you can cover "all strings upto length N" for some constant "N", but they do get hairy.

Keeping all this in mind, I'd go about coding your example like the following; restricting password to be precisely 10 characters long:

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])

The OrdAt function works around the problem of not being able to extract characters. Also note how we use Sum instead of sum, and how all "loops" are of fixed iteration count. I also added constraints to make all the ascii codes printable for convenience.

When you run this, you get:

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

Let's check it's indeed good:

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

So, we did get a length 10 string; but how come the ord's don't sum up to 100? Now, you have to remember sequences are composed of 8-bit values, and thus the arithmetic is done modulo 256. So, the sum actually is:

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

To avoid the overflows, you can either use larger bit-vectors, or more simply use Z3's unbounded Integer type Int. To do so, use the BV2Int function, by simply changing add_ascii_values to:

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

Now we'd get:

unsat

That's because each of our characters has at least value 0x20 and we wanted 10 characters; so there's no way to make them all sum up to 100. And z3 is precisely telling us that. If you increase your sum goal to something more reasonable, you'd start getting proper values.

Programming with z3py is different than regular programming with Python, and z3 String objects are quite different than those of Python itself. Note that the sequence/string logic isn't even standardized yet by the SMTLib folks, so things can change. (In particular, I'm hoping they'll add functionality for extracting elements at an index!).

Having said all this, going over the https://rise4fun.com/z3/tutorialcontent/sequences would be a good start to get familiar with them, and feel free to ask further questions.

这篇关于ord() 函数或带有 Z3 求解器的字符串的 ASCII 字符代码的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！