在 z3 中建模嵌套元组/序列

如何解决在 z3 中建模嵌套元组/序列

我目前正在为一小部分 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))"
• 列表。但是，列表只有一个类型 T，我只能将其实例化为 List 或，例如 Int。据我所知，z3 中没有联合类型或通用超级排序之类的东西。
• 未解释的函数。我认为应该可以引入带有 sort tuple 的函数 Tuple，甚至可以针对不同的参数长度和排序重载它。但是，我不知道如何提取 tuple(1,3) 的元素，因为该表达式不是递归定义的。

非常感谢 z3 / SMT 专家的任何帮助！

非常感谢！

元组数据类型：“抽象”索引和元组的问题

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

例如，我可以将一个 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',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、{{ 1}}).

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

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),x)) 函数。但是，如果我们有一个像 Tup_IT 这样由不同类型元素组成的元组，我该如何定义这个函数的目标域？例如，

Tuple_II.nth

为此，我需要某种超级类型的 target_sort = # ??? tup_IT_nth = z3.Function("Tuple_IT.nth",z3.IntSort(),Tup_II,target_sort) 和 int：与列表相同的问题。

有什么想法吗？ :)

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

只要假设我可以解决getter函数的排序问题；然后我编写了一个很好的实用程序函数来创建处理存在抽象索引的元组所需的所有内容：

Tup_II

问题在于带有 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",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,target_sort) get_in_range = z3.Function(f"{dt_name}.nth_i",target_sort) get_not_in_range = z3.Function(f"{dt_name}.nth_u",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,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,get,z3.And(axiom_1,axiom_2) 注释的 target_sort 声明。

解决方法

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

这里有一个例子：https://rise4fun.com/z3/tutorialcontent/guide#h27 并且同样可以在 z3py 中编码。有关更多示例，请参见 https://ericpony.github.io/z3py-tutorial/advanced-examples.htm。有关 SMTLib 中数据类型支持的官方说明，请参阅 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf 的第 4.2.3 节。

请注意，对于您将拥有的每个元组类型，您必须声明一个新的元组类型。 SMT 不是那种多态的。这个过程通常称为单晶化。如果最终您建模的语言具有可以“改变”形状的变量（即，一个简单的 2 元组在赋值后变成了 3 元组），您将不得不考虑一个新变量并将其建模为这样的。 （但这与给变量分配一个 int 和一个布尔值没有什么不同。SMTLib 是“简单类型的”，即所有变量总是有一个声明的类型。）

试试这个想法，如果您遇到问题，请发布代码示例。

处理类型

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

然而，这与符号执行几乎没有关系。想一想如何对这样的函数进行“类型检查”。在 Haskell 中类似符号：

Bool

要在 index :: (Int,Bool) -> Int -> XX index (a,_) 0 = a index (_,b) 1 = b 中放入什么？没有办法在简单类型的 lambda 演算中输入这个定义。这就是您所处的情况：SMTLib 本质上是一个简单类型的演算，所有这些类型都必须在“编译”时解析。

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

您目前采用的方法是最自然的方法，它是将 Python 子集浅嵌入到 SMTLib 中。您正在使用 SMTLib 函数/类型对您的语言进行建模。这是典型的方法，没有任何问题。它更简单，利用了底层语言的类型系统和特性的所有特性。如果可能，应该首选。

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

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

我的建议是简单地不允许对元组进行符号索引。只支持具体索引。当您弄清楚这个系统的怪癖时，您无疑会发现更多的差异。此时，您可以切换到深度嵌入。

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