将 C99 代码翻译成 Z3，细微的细节

Question

我遇到了一些我不太了解的微妙细节。我正在开发一个工具来删除死代码，假设以下示例：

int main(){
    if(1==0){
        neverexecutes();
    }
}

我将其转换为 AST (pycparser)，当我遇到 if 条件时 1==0 我使用以下方法将其转换为 Z3：

def evaluate_ast(self, node: c_ast.Node):
        """Translates a c_ast.Node to a z3 predicate."""
        typ = type(node) 
        if typ == c_ast.BinaryOp:
            leftnode = self.evaluate_ast(node.left)
            rightnode = self.evaluate_ast(node.right) 
            
            if node.op == '&&':
                return And(leftnode, rightnode)
            elif node.op == '||':
                return Or(leftnode, rightnode)
            elif node.op == '==':
                return leftnode == rightnode 
            elif node.op == '<':
                return leftnode < rightnode
            elif node.op == '<=':
                return leftnode <= rightnode
            elif node.op == '>':
                return leftnode > rightnode
            elif node.op == '>=':
                return leftnode >= rightnode
            elif node.op == '!=':
                return leftnode != rightnode
            elif node.op == '/':
                return leftnode / rightnode
            elif node.op == '+':
                return leftnode + rightnode

        elif typ == c_ast.Assignment and node.op == '=':
            leftnode = self.evaluate_ast(node.lvalue)
            rightnode = self.evaluate_ast(node.rvalue) 
            
            return leftnode == rightnode
        (...)

1==0 被翻译成 k!0，求解器回答 sat，这是不正确的。

如果我这样改变 C99 平等的处理方式：

elif node.op == '==':
     return And(leftnode == rightnode)

它有效，我假设我对所有二元运算符都有同样的问题。我在这里错过了什么？只有 False 的系统不应该是 unsat 吗？我认为 k!0 只是对 Z3 中某些错误值的翻译。

我觉得这也图形好一点我的问题：

>>> from z3 import * 
>>> s = Solver()
>>> s.add(False)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(1==0)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(Bool(1==0))
>>> s.check()
sat

False、1==0和Bool(1==0)有什么区别？

Answer 1

这里的问题是 Bool 取了一个名字并从中产生了一个符号值。您需要改用 BoolVal。在这些情况下，sexpr 方法是您用于调试目的的朋友：

>>> from z3 import *
>>> s = Solver()
>>> s.add(1==0)
>>> print(s.sexpr())
(assert false)

以上没问题，因为 add 方法很聪明，可以正确处理值。您可以将它包裹在 BoolVal 周围以获得相同的效果：

>>> from z3 import *
>>> s = Solver()
>>> s.add(BoolVal(1==0))
>>> print(s.sexpr())
(assert false)

但是如果你把它包裹起来看看会发生什么 Bool:

>>> from z3 import *
>>> s = Solver()
>>> s.add(Bool(1==0))
>>> print(s.sexpr())
(declare-fun k!0 () Bool)
(assert k!0)

这就是你问题的本质。（看起来 z3 提出了一个内部名称 k!0，因为 1==0 在这里不是有效的 SMTLib 名称。这增加了混乱。）

请注意，z3py 对 Int/IntVal、BitVec/BitVecVal、Real/RealVal 等具有类似的功能。你必须要小心。

不幸的是，这是 z3py 的最弱点之一：由于 Python 的非类型化性质，不同的函数会尝试解释您可以提供的各种输入，它们有时不一致，而且可能非常很难检测和调试此类问题。如果您怀疑打印有问题，s.sexpr() 是您最好的朋友。（例如，最近报告了一个类似的错误并随后得到修复。）

将 C99 代码翻译成 Z3，细微的细节

Translation C99 code to Z3, subtle details

python

z3