Способ верификации программного обеспечения по естественной семантике идентификаторов исходного кода программы при статическом анализе
METHOD OF THE SOFTWARE VERIFICATION BY THE SOFTWARE SOURCE CODE IDENTIFIERS NATURAL SEMANTICS IN STATIC ANALYSIS

Изобретение относится информатике, а именно к способам верификации программного обеспечения (ПО), разрабатываемого на языках программирования высокого уровня, и может быть использовано в инструментальных средствах статического анализа компьютерных программ, в которых идентификаторы ИК интерпретируют физические величины.
Статический анализ, являясь одним из методов проведения верификации, позволяет снизить затраты на ее проведение ПО за счет обнаружения дефектов на более ранних (по сравнению с тестированием) стадиях разработки ПО и точной локализации искажений в программном коде. Инструментальные средства статического анализа представляют собой реализацию первой стадии работы компилятора (анализа) с усложненными семантическими правилами. Процесс проведения статического анализа делится на фазы, каждая из которых преобразует одно из представлений исходной программы в другое. На первой фазе выполняется лексический анализ, во время которого происходит чтение входной последовательности символов программы, выделяются лексемы языка программирования и формируются токены. Токен представляет собой структуру, состоящую из имени токена и ссылки на таблицу символов, в которой аккумулируется информация об обнаруженных лексемах в процессе анализа. Вторая фаза - синтаксический анализ, который дополняет информацией таблицу символов и преобразует поток токенов от лексического анализатора в древовидную структуру в соответствии с грамматикой языка программирования. Типичным представлением исходной программы, получаемым после проведения синтаксического анализа, является абстрактное синтаксическое дерево (АСД), в котором «родительские» узлы соответствуют операциям, а «дочерние» - их аргументам. АСД и информация из таблицы символов используется на третьей фазе - семантическом анализе, для проверки исходной программы на семантическую согласованность с определением конкретного языка программирования и поиска дефектов. Статический анализ способен обнаруживать лексические, синтаксические и семантические дефекты, вызванные нарушением требований спецификации языка программирования или рекомендаций отраслевых стандартов.
Для снижения затрат на проведение верификации ПО целесообразно повысить эффективность статического анализа за счет дефектов, относящихся к нарушениям логики вычислений в программе. Для реализации данной возможности предлагается способ верификации ПО, основанный на проверке естественной семантики (ЕС) идентификаторов исходного кода (ИК) программы. Под семантикой понимается размерность физической величины, интерпретируемой в идентификаторе ИК.
Известен способ (Патент №2373570, «Способ верификации программного обеспечения распределительных вычислительных комплексов и система для его реализации»), позволяющий определять точки и участки уязвимости ИК ПО распределенных вычислительных комплексов (например, переполнение буфера) путем автоматического составления и решения соответствующих систем уравнений на основе внутреннего представления ИК ПО, хранящегося в виде баз данных и баз знаний.
Известен способ (Патент №2515684, «Способ синтаксического анализа языка программирования с расширяемой грамматикой»), решающий задачу динамической модификации таблиц компиляции LR синтаксического анализатора за счет заданных отдельно для каждого уровня иерархии вложенности грамматических правил языка программирования директив расширения грамматики, предназначенных для введения новых грамматических конструкций. Использование данного способа направлено на создание инструмента, позволяющего для решения любых специфических задач использовать универсальный язык программирования с расширяемой грамматикой.
Известен способ (Патент №2103728, «Способ преобразования входной программы транслятора и устройство для его осуществления»), позволяющий решать задачу быстрого доступа к актуальным значениям идентификаторов в дереве трансляции за счет запоминания указателей таблицы идентификаторов для синтаксического дерева вместо запоминания имен в синтаксическом дереве.
Известен способ (Патент №2115158, «Способ и устройство для достоверной оценки сематических признаков в синтаксическом анализе при проходе вперед слева направо»), осуществляющий определенный вид семантического анализа (проверку семантических признаков) во время работы синтаксического анализатора за счет модификации формата узлов в дереве разбора и усовершенствования действий, связанных с грамматическими правилами вывода. Данный способ синтаксического анализа позволяет осуществить проверку сематических признаков, связанных с требованиями спецификации языка программирования, а также проконтролировать синтаксическую корректность конструкций в ИК, за один проход одновременно с построением дерева разбора, что снижает время, требуемое для компиляции программы.
Наиболее близким технически решением, принятым за прототип, является известный способ построения синтаксических деревьев (Ахо Альфред В., Лам, Моника С., Сети Рави, Ульман Джеффри Д. Компиляторы: принципы, технологии и инструментарий, 2-е изд.: Пер. с англ. - М.: ООО «И.Д. Вильяме», 2008. - 1184 с.: ил. - Парал. тит. англ., разд. 5.3.1.), позволяющий с помощью синтаксически управляемого определения формировать внутреннее представление программы в виде АСД. Для чего каждой продукции исходной грамматики назначается семантическое правило создания объекта узла АСД с соответствующим количеством полей.
Целью настоящего изобретения является повышение эффективности статического анализа, за счет расширения множества типов обнаруживаемых дефектов, для снижения суммарных затрат на проведение верификации ПО.
Указанный технический результат достигается за счет того, что в синтаксическом управляемом определении (СУО) способа, основанного на способе построения синтаксических деревьев, семантические правила дополняются полем для операций с ЕС идентификаторов, позволяющие при проведении синтаксического анализа строить модифицированное АСД, в процессе восходящего обхода которого осуществляется контроль неизменности ЕС идентификаторов, хранящейся в дополненной таблице символов в виде одномерно целочисленного массива из девяти элементов.
NS
I
Для построения модифицированного АСД продукциям контекстно-свободной грамматики языка программирования в СУО ставятся в соответствие программные конструкции (например, в объектно-ориентированном стиле), описывающие создание узлов АСД. Структура внутреннего узла дополняется полем для операции с ЕС идентификаторов ИК (op), которое заполняется автоматически в зависимости от операции с идентификаторами в данном узле (op) и на основе размерной однородности физических уравнений, таблица соответствия которых представлена на фиг. 1.
I
NS
1
k
I
NS
1
k
Конструктор для создания объекта дополненного внутреннего узла АСД имеет вид: Node (op, op, c, …, c), где op - метка узла и операция с идентификаторами; op - операция с ЕС идентификаторов; с, …,c - k дополнительных полей для ссылок на «дочерние» объекты.
Конструктор для создания узла, являющегося листом: Leaf (op, val), где op - метка узла; val - лексическое значение, представленное либо ссылкой на таблицу символов для идентификаторов, либо константу.
При применении продукций СУО в процессе синтаксического разбора создаются объекты узлов модифицированного АСД, согласно конструкторам описанным выше.
j
j
ЕС идентификаторов ИК (размерность физической величины) не может быть получена путем анализа исходной программы и должна назначаться вручную. Предлагается после проведения лексического и синтаксического анализа инициализировать таблицу символов значениями ЕС для обнаруженных идентификаторов. Для чего таблица символов должна быть расширена полем для хранения одномерного целочисленного массива из девяти элементов (int natSem[9]), который позволит описать размерность любой физической величины, интерпретируемой в идентификаторе ИК. Формула размерности произвольной физической величины (А) имеет вид: , где e - степень j-го сомножителя формулы размерности физической величины. Элементами массива являются степени сомножителей в формуле размерности физической величины natSem[j - 1] = e, распределение которых по сопоставляющим формулы размерности представлено на фиг. 2. Идентификаторам, не обладающим ЕС, соответствует массив из нулевых элементов.
NS
Для непосредственного проведения верификации ПО необходимо осуществить восходящий обход модифицированного АСД, то есть обход, который вычисляет значения ЕС «родительского» узла после вычисления значений в «дочерних». Значения ЕС листьев АСД хранятся в таблице символов, получение которых возможно осуществить при помощи функции доступа к значениям поля в таблице символов по ссылке val объекта листа (getNaturalSemantics(val)). При выполнении обхода АСД в зависимости от операции в узле op возможны два варианта действий: расчет результирующего значения ЕС и контроль выполнения условия корректности выражения ИК (фиг. 1).
NS
NS
Расчет значения ЕС «родительского» узла АСД производится путем сложения или вычитания (op) значений ЕС «дочерних» узлов, помеченных идентификаторами ИК. Сложение и вычитание значений ЕС идентификаторов с числами (num) не производится, результирующее значение ЕС равняется значению ЕС идентификатора «дочернего» узла. Так как ЕС представлена в виде массива, то необходимая операция (op) с операндами выражения выполняется поэлементно и результатом является массив той же размерности.
Контроль выполнения условия корректности выражений ИК выполняется с целью выявления нарушений принципа размерной однородности физических уравнений, представленных в конструкциях ИК, исходя из значений ЕС идентификаторов в таблице символов. Невыполнение условия корректности выражения ИК свидетельствует о логическом дефекте в программе.
В качестве доказательства возможности осуществления заявленного изобретения с достижением вышеуказанного технического результата рассматривается программная конструкция для выражения для расчета координат при равноускоренном движении: x = x0+v*t+a*t*t/2.
а
Значения элементов массивов natSem, хранящихся в таблице символов, для идентификаторов выражения имеют вид: х - {1,0,0,0,0,0,0,0,0}; х0 - {1,0,0,0,0,0,0,0,0}; v - {1,0,-1,0,0,0,0,0,0}; t - {0,0,1,0,0,0,0,0,0}; -{1,0,-2,0,0,0,0,0,0}.
СУО для разбора ИК и построения модифицированного АСД данного выражения представлена на фиг. 3, где Е, Т, F - нетерминальные символы грамматики, num, id - терминалы грамматики, представляющие числа и идентификаторы соответственно. АСД для рассматриваемого выражения изображено на фиг. 4.
Шаги обхода АСД для расчета ЕС и контроля условий корректности выражений ИК:
1
sem = getNaturalSemantics(t); /* {0,0,1,0,0,0,0,0,0} */
2
sem = num. val;
3
1
sem = sem, /* {0,0,1,0,0,0,0,0,0} */
4
sem = getNaturalSemantics{t); /* {0,0,1,0,0,0,0,0,0} */
5
4
3
sem = sem + sem; /* {0,0,2,0,0,0,0,0,0} */
6
a
sem = getNaturalSemantics(); /* {1,0,-2,0,0,0,0,0,0} */
7
6
5
sem = sem + sem; /* {1,0,0,0,0,0,0,0,0} */
8
sem = getNaturalSemantics(v), /* {1,0,-1,0,0,0,0,0,0} */
9
sem = getNaturalSemantics(t)\ /* {0,0,1,0,0,0,0,0,0} */
10
9
8
sem = sem + sem; /* {1,0,0,0,0,0,0,0,0} */
11
10
ПО
sem = sem; /* {1,0,0,0,0,0,0,0,0}, T = 0*/
12
sem = getNaturalSemantics(x0), /* {1,0,0,0,0,0,0,0,0} */
13
12
ПО
sem = sem; /* {1,0,0,0,0,0,0,0,0}, T = 0 */
14
sem = getNaturalSemantics(x); /* {1,0,0,0,0,0,0,0,0} */
15
14
ПО
sem = sem; /* {1,0,0,0,0,0,0,0,0}, T = 0 */.
15
ПО
Результирующее значения EC выражения равно sem, условия корректности выполнены (T = 0).
а
Если в данном примере заменить идентификатор  на v, то выражение примет вид: x = x0+v*t+v*t*t/2. Шаги обхода модифицированного АСД, с изменившимися значениями, следующие:
6
sem = getNaturalSemantics(v); /* {1,0,-1,0,0,0,0,0,0} */
7
6
5
sem = sem+sem; /* {1,0,1,0,0,0,0,0,0} */
11
10
ПО
sem = sem; /* {1,0,0,0,0,0,0,0,0}, T ≠ 0 */.
ПО
Условие корректности на шаге 11 не выполнено (Т ≠ 0), следовательно существует дефект ЕС в проверяемом на данном узле, либо в его «дочерних» узлах.
Таким образом, в настоящем изобретении доказана возможность обнаружения нового для статического анализа типа дефектов - дефектов ЕС идентификаторов ИК программы, что позволит повысить эффективность статического анализа и снизить суммарные затраты на проведение верификации ПО.