Как аннотировать программу для обнаружения мертвого кода с помощью z3-solver?

Question

вступление

Учитывая простую функцию, написанную на C++, как показано ниже:

      int func(int x, int y)
{
    if (x < 3)
    {
        y = 4;
        if (x < 4)
        {
            y = y + 2;
        }
        else
        {
            x = x + 4;
        }
    }
    else
    {
        x = x + 1;
    }

    return x + y;
};

Проблема

Как аннотировать программу, чтобы сделать следующее в ?

1. Обнаружение мертвых кодов. (х = х + 4)
2. Создание тестовых случаев (покрытие кода).
3. Анализ инвариантов.
4. и проверки кода.

Что я сделал?

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

      PATH 1 for (y = 4) => (x < 3)
PATH 2 for (y = y + 2) => (x < 3) ^ (x < 4)
PATH 3 for (x = x + 4) => (x < 3) ^ (x >= 4)
PATH 4 for (x = x + 1) => (x >= 3)

Затем, если я использую Z3, я могу проверить, есть ли какие-либо из этих путей. unsatчто предполагает, что блок кода, связанный с ними, будет Dead code.

Какая помощь мне нужна?

• Для обнаружения мертвого кода:

Я действительно не знаю, как показать выше в . Должен ли я использовать разные решатели для каждого пути? как это:

      from z3 import *

x = Int('x')
y = Int('y)
s1 = Solver()
s2 = Solver()
s3 = Solver()
s4 = Solver()

s1.add(x < 3)
s2.add(x < 3, x < 4)
s3.add(x < 3, x >= 4)
s4.add(x >= 3)

s1.check() // sat
s2.check() // sat
s3.check() // unsat
s4.check() // sat

Я думаю, что это неэффективный способ обнаружения мертвых кодов. Что, если было сто разных путей? Так что должен быть лучший способ сделать это.

• Для анализа инвариантов:

Опять же, должен ли я использовать разные решатели для каждого блока кода? Например:

      from z3 import *

s1 = Solver()
s2 = Solver()
s3 = Solver()
s4 = Solver()
x0 = Int('x0')
y0 = Int('y0)
x1 = Int('x1')
y1 = Int('y1')

// Path 1
s1.add(x0 < 3)
s1.add(y0 == 4)
s1.add(y1 == y0 + 2)
s1.check()
s1.model()

// Path 2
s2.add(x0 < 3)
s2.add(y0 == 4)
s2.add(x1 == x0 + 4);
s2.check()
s2.model()

// Path 3
s3.add(x0 < 3)
s3.add(y0 == 4)
s3.add(x1 == x0 + 4);
s3.check()
s3.model()

// Path 4
s3.add(x0 >= 3)
s3.add(x1 == x0 + 1);
s3.check()
s3.model()

• И я понятия не имею, как Generate test casesи делать Pre& Postпроверка кода

Наконец, мой вопрос на самом деле заключается в том, как анализировать программу с z3 для различных сценариев, таких как Dead Code Detection, Invariant analysis, Test-case generationи т. д. Чтобы быть более конкретным, я ищу лучшие практики в этом отношении. Пример кода в z3-solverочень поможет. Более желательно, я хотел бы увидеть, как улучшить образец z3коды, которые я привел выше.

Спасибо за вашу помощь

Answer 1

Переполнение стека работает лучше всего, если вы сосредоточитесь только на одном вопросе. Все это выполнимо с помощью z3, но важный вопрос, который следует задать, заключается в том, интересует ли вас только эта конкретная программа или вы заинтересованы в создании чего-то, что работает для произвольных программ на C?

Если вы заинтересованы в последнем, то это гораздо более сложная задача, и вам действительно следует взглянуть на документы по символическому исполнению/анализу. Если вас интересует только эта программа, вам следует провести анализ пути: для мертвого кода вы хотите знать, есть ли какой-либо путь кода, который недостижим, т. е. не принимает ли конкретный оператор if никогда это thenили же elseответвляться. Обратите внимание, что вы должны использовать только один решатель, а не разные для каждого пути. Вы можете использовать решатель постепенно, так как вы выполняете поиск в глубину потока управления.

Методы, которые вам нужны, обычно рассматриваются как часть исследования DART, которое также охватывает создание тестовых случаев. Начните с прочтения этой статьи: https://web.eecs.umich.edu/~weimerw/2014-6610/reading/p213-godefroid.pdf

Опять же, переполнение стека работает лучше всего, если вы задаете очень конкретный и очень сфокусированный вопрос по одному конкретному аспекту. После того, как вы просмотрите приведенную выше статью, я уверен, что у вас появятся вопросы получше!