在 z3 中建模嵌套元组/序列
Modeling nested tuples / sequences in z3
我目前正在为 Python 的一小部分构建一个符号执行引擎。这个子集支持的最复杂的数据结构是任意嵌套的元组，也就是说，你可以写成x = (1, 2, (3, 4), 5)这样的东西。在我的 SE 引擎中，所有值都表示为 z3 对象。昨天，我很难尝试在 z3 中对这些嵌套元组进行建模。
我尝试了什么：
- 数组。问题：数组就是数组，也就是说，它们跨越一个矩形 space，这不适合我的元组。
- 序列。我喜欢序列数据类型；但是，它不支持嵌套。例如，您不能写
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))"
- 列表。但是，列表只有一个类型
T，我只能将其实例化为 List 或 ，例如 Int。据我所知，z3 中没有联合类型或通用超级排序之类的东西。
- 未解释的函数。我认为应该可以引入一个带有排序
Tuple 的函数 tuple，甚至可以针对不同的参数长度和排序重载它。但是，我不知道如何提取 tuple(1, 2, 3) 的元素，因为该表达式不是递归定义的。
非常感谢 z3/SMT 专家的任何帮助！
非常感谢！
元组数据类型：“抽象”索引和元组存在问题
我也尝试了@alias 提出的想法，为元组定义了一个数据类型。这工作得很好，但有一个问题：如果元组或索引不是具体的，即（包含表达式的）变量，我如何建模对元组元素的访问？
例如，我可以将整数的二元组定义为：
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)
问题是 target_sort 的声明带有 # ??? <-- What to do here? 注释。
为什么不直接使用元组来建模元组？您可以声明一个通用元组类型，然后将其实例化多次以处理嵌套。
这里有一个例子：https://rise4fun.com/z3/tutorialcontent/guide#h27 and the same can be coded in z3py as well. See https://ericpony.github.io/z3py-tutorial/advanced-examples.htm as well for further examples. See section 4.2.3 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf SMTLib 中对数据类型支持的官方描述。
请注意，对于您将拥有的每种元组类型，您都必须声明一个新的元组类型。 SMT 在这方面不是多态的。这个过程通常称为单态化。如果最终你正在建模的语言具有可以“改变”形状的变量（即，一个简单的二元组在赋值后变成三元组），你将不得不考虑一个新变量并将其建模为这样的。 （但这与为变量分配一个 int，然后分配一个 boolean 没有什么不同。SMTLib 是“简单类型的”，即所有变量始终具有单一声明类型。）
试试这个想法，如果你 运行 遇到问题 post 代码示例。
处理类型
如果你有一个类型为 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 本质上是一种简单类型的演算，其中所有这些类型都必须在“编译”时解决。
那么，你是如何处理这个问题的？最简单的答案是 not 允许使用符号值进行索引。这就是 Haskell、ML 等语言所采取的立场。但是在 Lisp/Scheme/Python 等具有动态类型的语言中，情况并非如此。所以问题就变成了，如何在简单类型的系统（例如 SMTLib）中为这样的动态类型语言建模。
您目前采用的方法是将 Python 子集浅嵌入到 SMTLib 中，这是最自然的方法。您正在使用 SMTLib functions/types 为您的语言建模。这是典型的做法，并没有错。它更简单，利用了底层语言的类型系统和特性的所有特性。如果可能的话应该是首选。
当您的对象语言和元语言功能不匹配时，这种方法的不足之处是：您的对象语言本质上是动态类型的（我假设您遵循 Python 的约定），其中 SMTLib 是静态和简单类型的。这种不匹配意味着您不能再直接使用浅嵌入方法。
另一种方法是使用通用类型来表示目标语言中的所有术语。这也称为深度嵌入，您的语言术语本质上成为句法元素。您的对象语言表达式的类型成为您的元语言本身的数据类型。显然，这是更多的工作，但如果您想在 SMTLib 中编码，则非常需要这样做。但请记住，如果您使用 Haskell/ML 等高级类型化语言为该子集编写解释器，这与您遇到的问题相同：一旦类型化策略不匹配，浅嵌入就会中断开始出现。
我的建议是简单地不允许对元组进行符号索引。只支持具体索引。当你找出这个系统的怪癖时，你无疑会发现更多的差异。那时你可以切换到深度嵌入。
这是一篇值得阅读的好论文（在 Haskell 上下文中），讨论了如何使用浅层和嵌入式样式对特定领域的语言进行建模。您的情况的细节会有所不同，因为您还希望支持符号构造，但基本思想适用：http://www.cse.chalmers.se/~josefs/publications/TFP12.pdf
我目前正在为 Python 的一小部分构建一个符号执行引擎。这个子集支持的最复杂的数据结构是任意嵌套的元组，也就是说，你可以写成x = (1, 2, (3, 4), 5)这样的东西。在我的 SE 引擎中，所有值都表示为 z3 对象。昨天，我很难尝试在 z3 中对这些嵌套元组进行建模。
我尝试了什么：
- 数组。问题：数组就是数组，也就是说，它们跨越一个矩形 space，这不适合我的元组。
- 序列。我喜欢序列数据类型；但是，它不支持嵌套。例如，您不能写
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))" - 列表。但是，列表只有一个类型
T，我只能将其实例化为List或 ，例如Int。据我所知，z3 中没有联合类型或通用超级排序之类的东西。 - 未解释的函数。我认为应该可以引入一个带有排序
Tuple的函数tuple，甚至可以针对不同的参数长度和排序重载它。但是，我不知道如何提取tuple(1, 2, 3)的元素，因为该表达式不是递归定义的。
非常感谢 z3/SMT 专家的任何帮助！
非常感谢！
元组数据类型：“抽象”索引和元组存在问题
我也尝试了@alias 提出的想法，为元组定义了一个数据类型。这工作得很好，但有一个问题：如果元组或索引不是具体的，即（包含表达式的）变量，我如何建模对元组元素的访问？
例如，我可以将整数的二元组定义为：
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)
问题是 target_sort 的声明带有 # ??? <-- What to do here? 注释。
为什么不直接使用元组来建模元组？您可以声明一个通用元组类型，然后将其实例化多次以处理嵌套。
这里有一个例子：https://rise4fun.com/z3/tutorialcontent/guide#h27 and the same can be coded in z3py as well. See https://ericpony.github.io/z3py-tutorial/advanced-examples.htm as well for further examples. See section 4.2.3 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf SMTLib 中对数据类型支持的官方描述。
请注意，对于您将拥有的每种元组类型，您都必须声明一个新的元组类型。 SMT 在这方面不是多态的。这个过程通常称为单态化。如果最终你正在建模的语言具有可以“改变”形状的变量（即，一个简单的二元组在赋值后变成三元组），你将不得不考虑一个新变量并将其建模为这样的。 （但这与为变量分配一个 int，然后分配一个 boolean 没有什么不同。SMTLib 是“简单类型的”，即所有变量始终具有单一声明类型。）
试试这个想法，如果你 运行 遇到问题 post 代码示例。
处理类型
如果你有一个类型为 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 本质上是一种简单类型的演算，其中所有这些类型都必须在“编译”时解决。
那么，你是如何处理这个问题的？最简单的答案是 not 允许使用符号值进行索引。这就是 Haskell、ML 等语言所采取的立场。但是在 Lisp/Scheme/Python 等具有动态类型的语言中，情况并非如此。所以问题就变成了，如何在简单类型的系统（例如 SMTLib）中为这样的动态类型语言建模。
您目前采用的方法是将 Python 子集浅嵌入到 SMTLib 中，这是最自然的方法。您正在使用 SMTLib functions/types 为您的语言建模。这是典型的做法，并没有错。它更简单，利用了底层语言的类型系统和特性的所有特性。如果可能的话应该是首选。
当您的对象语言和元语言功能不匹配时，这种方法的不足之处是：您的对象语言本质上是动态类型的（我假设您遵循 Python 的约定），其中 SMTLib 是静态和简单类型的。这种不匹配意味着您不能再直接使用浅嵌入方法。
另一种方法是使用通用类型来表示目标语言中的所有术语。这也称为深度嵌入，您的语言术语本质上成为句法元素。您的对象语言表达式的类型成为您的元语言本身的数据类型。显然，这是更多的工作，但如果您想在 SMTLib 中编码，则非常需要这样做。但请记住，如果您使用 Haskell/ML 等高级类型化语言为该子集编写解释器，这与您遇到的问题相同：一旦类型化策略不匹配，浅嵌入就会中断开始出现。
我的建议是简单地不允许对元组进行符号索引。只支持具体索引。当你找出这个系统的怪癖时，你无疑会发现更多的差异。那时你可以切换到深度嵌入。
这是一篇值得阅读的好论文（在 Haskell 上下文中），讨论了如何使用浅层和嵌入式样式对特定领域的语言进行建模。您的情况的细节会有所不同，因为您还希望支持符号构造，但基本思想适用：http://www.cse.chalmers.se/~josefs/publications/TFP12.pdf