Modeling nested tuples / sequences in z3

Question

我目前正在为Python的一小部分构建一个符号执行引擎。该子集支持的最复杂的数据结构是任意嵌套的元组，即，您可以编写类似x = (1, 2, (3, 4), 5)的内容。在我的SE引擎中，所有值都表示为z3对象。昨天，我很难在z3中对这些嵌套元组进行建模。

我尝试过的：

• 数组。问题：数组是数组，也就是说，它们跨越一个矩形空间，这不适合我的元组
• 序列。我喜欢序列数据类型；但是，它不支持嵌套。例如，不能写入z3.Concat(z3.Unit(z3.IntVal(1)), z3.Unit(z3.Concat(z3.Unit(z3.IntVal(2)), z3.Unit(z3.IntVal(3)))))，这会引发z3.z3types.Z3Exception: b"Sort of function 'seq.++' does not match the declared type. Given domain: (Seq Int) (Seq (Seq Int))"
• 列表。但是，Lists只有一个类型T，我只能将其实例化为List或，例如Int。据我所知，z3中没有类似并集类型或一般超排序的东西
• 意外功能。我认为应该可以引入一个具有排序Tuple的函数tuple，甚至可以为不同的参数长度和排序重载它。然而，我不知道如何提取tuple(1, 2, 3)的元素，因为该表达式不是递归定义的

如果这里有z3/SMT专家的帮助，我将不胜感激！

提前感谢！

元组数据类型："；摘要"；索引&元组

我还尝试了@alias提出的想法，为元组定义一个数据类型。这工作得很好，但有一个问题：如果元组或索引都不是具体的，即(表达式包含)变量，我如何对元组元素的访问建模？

例如，我可以将int的2元组定义为：

Tup_II = z3.Datatype('Tuple_II')
Tup_II.declare('tuple', ('fst', z3.IntSort()), ('snd', z3.IntSort()))
Tup_II = Tup_II.create()
a_tuple = Tup_II.tuple(z3.IntVal(1), z3.IntVal(2))
print(a_tuple)  # tuple(1, 2)
tuple_concrete_access = z3.simplify(Tup_II.fst(a_tuple))
print(tuple_concrete_access)  # 1

没关系。我还可以通过嵌入Tup_II数据类型在顶部定义嵌套元组：

Tup_IT = z3.Datatype('Tuple_IT')
Tup_IT.declare('tuple', ('fst', z3.IntSort()), ('snd', Tup_II))
Tup_IT = Tup_IT.create()
another_tuple = Tup_IT.tuple(z3.IntVal(0), a_tuple)
print(another_tuple)  # tuple(0, tuple(1, 2))

但是要访问元素，我需要知道索引是0还是1才能选择正确的访问器(fst，snd)。

我试图从序列类型的行为中获得灵感：

int_seq = z3.Concat(z3.Unit(z3.IntVal(1)), z3.Unit(z3.IntVal(2)))
print(int_seq)  # Concat(Unit(1), Unit(2))
concrete_access = z3.simplify(int_seq[z3.IntVal(0)])
print(concrete_access)  # 1
concrete_access_2 = z3.simplify(int_seq[z3.IntVal(2)])
x = z3.Int("x")
abstract_access = z3.simplify(int_seq[x])
print(abstract_access)
# If(And(x >= 0, Not(2 <= x)),
#    seq.nth_i(Concat(Unit(1), Unit(2)), x),
#    seq.nth_u(Concat(Unit(1), Unit(2)), x))

因此，一个想法是定义一个Tuple_II.nth函数。然而，如果我们有一个类似Tup_IT的元组，由不同类型的元素组成，我该如何定义该函数的目标域？例如，

target_sort = # ???
tup_IT_nth = z3.Function("Tuple_IT.nth", z3.IntSort(), Tup_II, target_sort)

因此，我需要某种超级类型的int和Tup_II：与列表的问题相同。

有什么想法吗？：)

我想要的是：用于创建元组类型的实用函数

只是假设我可以解决getter函数的排序问题；然后我写了一个很好的实用函数，创建了在存在抽象索引的情况下处理元组所需的所有东西：

def create_tuple_type(*sorts: z3.SortRef) -> 
Tuple[z3.Datatype, Dict[int, z3.FuncDeclRef], z3.FuncDeclRef, z3.BoolRef]:
"""
DOES NOT YET WORK WITH NESTED TUPLES!
Example:
>>> tuple_II, accessors, getter, axioms = create_tuple_type(z3.IntSort(), z3.IntSort())
>>>
>>> a_tuple = tuple_II.tuple(z3.IntVal(1), z3.IntVal(2))
>>>
>>> print(z3.simplify(accessors[0](a_tuple)))  # 1
>>> print(z3.simplify(getter(a_tuple, z3.IntVal(0))))  # Tuple_II.nth(tuple(1, 2), 0)
>>>
>>> s = z3.Solver()
>>> s.set("timeout", 1000)
>>> s.add(z3.Not(z3.Implies(axioms, z3.IntVal(1) == getter(a_tuple, z3.IntVal(0)))))
>>> assert s.check() == z3.unsat  # proved!
>>>
>>> s = z3.Solver()
>>> s.set("timeout", 1000)
>>> s.add(z3.Not(z3.Implies(axioms, z3.IntVal(0) == getter(a_tuple, z3.IntVal(0)))))
>>> assert s.check() == z3.unknown  # not proved!
:param sorts: The argument sorts for the tuple type
:return: The new tuple type along with
accessor functions,
a generic accessor function,
and axioms for the generic accessor
"""
dt_name = "Tuple_" + "".join([str(sort)[0] for sort in sorts])
datatype = z3.Datatype(dt_name)
datatype.declare('tuple', *{f"get_{i}": sort for i, sort in enumerate(sorts)}.items())
datatype = datatype.create()
accessors = {i: getattr(datatype, f"get_{i}") for i in range(len(sorts))}
target_sort = z3.IntSort()  # ??? <-- What to do here?
get = z3.Function(f"{dt_name}.nth", datatype, z3.IntSort(), target_sort)
get_in_range = z3.Function(f"{dt_name}.nth_i", datatype, z3.IntSort(), target_sort)
get_not_in_range = z3.Function(f"{dt_name}.nth_u", datatype, z3.IntSort(), target_sort)
x = z3.Int("x")
t = z3.Const("t", datatype)
axiom_1 = z3.ForAll(
[t, x],
get(t, x) == z3.If(
z3.And(x >= z3.IntVal(0), x < z3.IntVal(len(sorts))),
get_in_range(t, x),
get_not_in_range(t, x)
)
)
axiom_2 = None
for idx in range(len(sorts)):
axiom = get_in_range(t, z3.IntVal(idx)) == accessors[idx](t)
if axiom_2 is None:
axiom_2 = axiom
continue
axiom_2 = z3.And(axiom_2, axiom)
axiom_2 = z3.ForAll([t], axiom_2)
return datatype, accessors, get, z3.And(axiom_1, axiom_2)

问题是使用# ??? <-- What to do here?注释声明target_sort。

Answer 1

为什么不使用元组来建模元组？您可以声明一个泛型元组类型，然后将其实例化多次以处理嵌套的元组类型。

这里有一个例子：https://rise4fun.com/z3/tutorialcontent/guide#h27并且同样可以在z3py中进行编码。看见https://ericpony.github.io/z3py-tutorial/advanced-examples.htm以及用于进一步的实例。参见第4.2.3节http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf以获取对SMTLib中数据类型支持的官方描述。

注意，对于您将拥有的每种元组类型，都必须声明一个新的元组类型。SMT并不是以这种方式多态的。这个过程通常被称为单形态化。如果最终你正在建模的语言有变量；改变"；形状(即，一个简单的2元组在赋值后变成3元组)，您必须将其视为一个新变量并对其进行建模。(但这与变量被分配一个int，然后是一个boolean没有什么不同。SMTLib是"简单类型化的"，即所有变量总是有一个声明的类型。)

尝试一下这个想法，如果遇到问题，可以发布代码示例。

处理类型

如果您有一个类型为IntxBool的元组(即，第一个组件是Int，第二个是Bool)，那么投影函数将是fst : IntxBool -> Int和snd : IntxBool -> Bool。如果你想使用的投影函数不是具体的，那么你就有问题了。结果是Int还是Bool？

然而，这与象征性的执行几乎没有关系。想一想如何"；类型检查"；这样的功能。在类似Haskell的表示法中：

index :: (Int, Bool) -> Int -> XX
index (a, _) 0 = a
index (_, b) 1 = b

在XX中放入什么？在简单类型的lambda演算中无法键入此定义。这就是你所处的情况：SMTLib本质上是一个简单类型的微积分，所有这些类型都必须在"；编译"；时间

那么，你是如何处理的呢？最简单的答案是而不允许使用符号值进行索引。这就是Haskell、ML等语言的立场。但在具有动态类型的语言(如Lisp/Scheme/Python)中，情况并非如此。因此，问题变成了，如何在SMTLib这样的简单类型系统中为这样一种动态类型的语言建模。

到目前为止，您采用的方法是将Python子集浅嵌入到SMTLib中，这是最自然的方法。您正在使用SMTLib函数/类型为您的语言建模。这是一种典型的方法，它没有错。它更简单，利用了底层语言的类型系统和特性的所有特性。如果可能的话，应该优先考虑。

这种方法的不足之处在于，当您的对象语言和元语言功能不匹配时：您的对象语本质上是动态类型的(我假设您遵循Python的约定)，其中asSMTLib是静态且简单类型的。这种不匹配意味着您不能再直接使用浅嵌入方法。

另一种选择是使用表示对象语言中所有术语的通用类型。这也被称为深度嵌入，你的语言术语本质上成为句法元素。对象语言表达式的类型成为元语言本身的数据类型。显然，这是一项更多的工作，但如果您想在SMTLib中进行编码，则几乎需要这样做。但请记住，如果你用Haskell/ML等高级类型语言为这一子集编写解释器，你也会遇到同样的问题：一旦类型策略中的不匹配开始出现，浅嵌入就会中断。

我的建议是简单地不允许符号索引到元组中。仅支持具体索引。当你找出这个系统的怪癖时，你无疑会发现进一步的差异。在这一点上，您可以切换到深度嵌入。

这是一篇很好的论文(在Haskell上下文中)，讨论了如何使用浅层和嵌入式风格对特定领域的语言进行建模。在您的情况下，细节会有所不同，因为您也想支持符号结构，但基本思想适用：http://www.cse.chalmers.se/~josefs/publications/TFP12.pdf