时间戳

首页 > 解决方案 > 将 C99 代码翻译成 Z3，细微的细节

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

问题描述

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

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

标签： pythonz3

解决方案

The problem here is that Bool takes a name and makes a symbolic value out of it. You need to use BoolVal instead. In these cases the sexpr method is your friend for debugging purposes:

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

The above is OK, because the add method is smart to treat values correctly. You could've wrapped it around BoolVal for the same effect:

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

But see what happens if you wrap it around Bool:

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

And that is the essence of your problem. (Looks like z3 is coming up with an internal name k!0 since 1==0 isn't a valid SMTLib name here. Which adds to the confusion.)

Note that z3py has similar functions for Int/IntVal, BitVec/BitVecVal, Real/RealVal etc. that you have to be careful with similarly.

This is one of the weakest points of z3py unfortunately: Due to Python's untyped nature, different functions try to interpret all sorts of inputs you can provide and they are sometimes inconsistent and it can be very hard to detect and debug such issues. If you suspect something is off printing s.sexpr() is your best friend. (A similar recent bug was reported here and subsequently fixed, for instance.)

推荐阅读