Методика статического анализа для поиска дефектов естественной семантики программных объектов и ее программная реализация на базе инфраструктуры компилятора LLVM и фронтенда Clang

Abstract

В статье описывается методика статического анализа для поиска функциональных дефектов программ, разработка которой обусловлена необходимостью создания качественного отечественного программного обеспечения автоматизированных систем военного назначения в условиях временных и финансовых ограничений процесса разработки. Использование статического анализа позволит автоматизировать процесс выявления дефектов и упростит их локализацию в рамках мероприятий процесса верификации, при этом приоритетным объектом проверок должно быть специальное программное обеспечение вновь создаваемых автоматизированных систем ввиду своей эксклюзивности, масштабности и логической сложности. Предлагается подход, основанный на контроле выполнения принципа размерной однородности физических уравнений, представленных в программе, для чего идентификаторам программных объектов назначается неизменный признак в виде вектора физической размерности интерпретируемой величины. Совокупность всех векторов образует семантический домен, используемый при проверке соотношений между программными объектами по аналогии с анализом зависимостей при абстрактной интерпретации. Для проверки используется внутреннее представление программы, по которому происходят вычисления производных векторов на основании операций с исходными программными объектами. Программная реализация предлагаемой методики основывается на компиляторе LLVM и фронтенде Clang для трансляции кода на языках C, C++, Objective-C. Получаемое с помощью API Clang абстрактное синтаксическое дерево модифицируется для хранения данных о векторах программных объектов

The article proposes a static analysis technique for searching functional software defects. Development is caused by the need to create high quality domestic military automated system software in conditions of temporary and financial constraints. The use of static analysis makes it possible to automate the process of error detection and it allows to localizing defects simply. The priority object of inspections should be special software for newly created automated systems because it is exclusively, scale and logical complexity. An approach based on controlling the implementation of principle of dimensional homogeneity of the physical equations presented in the software. For this purpose, program objects identifiers are assigned an invariable attribute in the form of a physical dimension vector of interpreted value. The set of all vectors forms a semantic domain used in verifying the relationships between program objects by analogy with the analysis of dependencies in the abstract interpretation. The technique uses a program internal representation for calculations of derivate vectors on the basis of operations with initial program objects. The software implementations uses the LLVM compiler and Clang frontend to translate code in C, C++, Objective-C. Clang API internal representation in the form of abstract syntax tree is modified to store data about program objects vectors