Перевод кода C99 в Z3, тонкие детали - PullRequest
Новая
       29

Перевод кода C99 в Z3, тонкие детали

1 голос
/ 09 июля 2020

Я сталкиваюсь с некоторыми тонкими деталями, которые я не очень хорошо понимаю. Я разрабатываю инструмент для удаления мертвого кода, предполагая следующий пример: 

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

1 Ответ

1 голос
/ 09 июля 2020

Проблема здесь в том, что Bool берет имя и делает из него значение symboli c. Вместо этого вам нужно использовать 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 и c. с которыми вы должны быть осторожны.

К сожалению, это одно из самых слабых мест z3py: из-за нетипизированной природы Python различные функции пытаются интерпретировать все виды вводимых вами данных, и они иногда бывают непоследовательными, и обнаружить и отладить такие проблемы может быть очень сложно. Если вы подозреваете, что что-то не так, напечатайте s.sexpr() - ваш лучший друг. (Об аналогичной недавней ошибке сообщалось здесь и впоследствии было исправлено, например.)

...