Конвертер трасс из формата graphML в формат Sarif
Необходимо написать на питоне конвертер трасс вместе с логикой полностью из witness формата GraphML, используемого в SV-COMP, в формат трасс SARIF. Нас интересует ивзуализация формата SARIF на Github.
В результирующем формате SARIF должна быть представленна трасса ошибки и исходный ему соответствующий.
Подробности см. для каждого элемента.
Ссылки:
1. Witness формат GraphML https://github.com/sosy-lab/sv-witnesses/blob/main/README-GraphML.md
2. Формат SARIF https://docs.oasis-open.org/sarif/sarif/v2.1.0/sarif-v2.1.0.html
3. Визуализация SARIF на Github https://docs.github.com/en/code-security/code-scanning/integrating-with-code-scanning/sarif-support-for-code-scanning#reportingdescriptor-object
Должен поддерживать все основные типы узлов witness формата:
- Entry - представляет собой начальную вершину, с нее должна начинаться трасса.
- Violation - конечная вершина трассы показывает, где детектирована ошибка.
- Sink - в SARIF может отсутствовать
- Invariant - в SARIF может отсутствовать
Должен поддерживать все основные типы дуг witness формата:
- Function calls - ключи enterFunction, returnFromFunction. В формате SARIF трасса по вызовам функций должна полностью прослеживаться. То есть для каждого вызова в трассе witness формата должен быть вызов в SARIF формате, и должна быть возможность установить порядок вызова. В визуализаторе формата SARIF обязательно должна быть отсылка к исходному коду (определяется ключами startline, endline, startoffset, endoffset).
- Conditions - ключ control - позволяет отследить, какая была выбрана ветвь. Для этого эелемента в формате SARIF должно быть понятно, как он располагается относительно вызова функций. В первом приближении его можно опустить.
- Assumptions - ключ assumption, позволяет отследить, какие были сделаны предположения об переменных состояния. Для этого эелемента в формате SARIF должно быть понятно, как он располагается относительно вызова функций. Обязательно должны поддерживаться выражения типа имя переменной = значение.
- Thread specifics - ключ threadId - предоставляет информацию о том, в каком потоке происходит выполнение. В визуализаторе формата SARIF требуется визуально отличать трассу функций в одном потоке от трассы функций другого потока. Ключ createThread - показывает точку создания потока.
- Loop heads, ключ enterLoopHead - в первом приближении его можно опустить.
