Конвертер трасс из формата 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 - в первом приближении его можно опустить.