Способ верификации программного обеспечения по естественной семантике идентификаторов исходного кода программы при статическом анализе Российский патент 2018 года по МПК G06F8/00 G06F17/27 

Изобретение относится информатике, а именно к способам верификации программного обеспечения (ПО), разрабатываемого на языках программирования высокого уровня, и может быть использовано в инструментальных средствах статического анализа компьютерных программ, в которых идентификаторы ИК интерпретируют физические величины.

Статический анализ, являясь одним из методов проведения верификации, позволяет снизить затраты на ее проведение ПО за счет обнаружения дефектов на более ранних (по сравнению с тестированием) стадиях разработки ПО и точной локализации искажений в программном коде. Инструментальные средства статического анализа представляют собой реализацию первой стадии работы компилятора (анализа) с усложненными семантическими правилами. Процесс проведения статического анализа делится на фазы, каждая из которых преобразует одно из представлений исходной программы в другое. На первой фазе выполняется лексический анализ, во время которого происходит чтение входной последовательности символов программы, выделяются лексемы языка программирования и формируются токены. Токен представляет собой структуру, состоящую из имени токена и ссылки на таблицу символов, в которой аккумулируется информация об обнаруженных лексемах в процессе анализа. Вторая фаза - синтаксический анализ, который дополняет информацией таблицу символов и преобразует поток токенов от лексического анализатора в древовидную структуру в соответствии с грамматикой языка программирования. Типичным представлением исходной программы, получаемым после проведения синтаксического анализа, является абстрактное синтаксическое дерево (АСД), в котором «родительские» узлы соответствуют операциям, а «дочерние» - их аргументам. АСД и информация из таблицы символов используется на третьей фазе - семантическом анализе, для проверки исходной программы на семантическую согласованность с определением конкретного языка программирования и поиска дефектов. Статический анализ способен обнаруживать лексические, синтаксические и семантические дефекты, вызванные нарушением требований спецификации языка программирования или рекомендаций отраслевых стандартов.

Для снижения затрат на проведение верификации ПО целесообразно повысить эффективность статического анализа за счет дефектов, относящихся к нарушениям логики вычислений в программе. Для реализации данной возможности предлагается способ верификации ПО, основанный на проверке естественной семантики (ЕС) идентификаторов исходного кода (ИК) программы. Под семантикой понимается размерность физической величины, интерпретируемой в идентификаторе ИК.

Известен способ (Патент №2373570, «Способ верификации программного обеспечения распределительных вычислительных комплексов и система для его реализации»), позволяющий определять точки и участки уязвимости ИК ПО распределенных вычислительных комплексов (например, переполнение буфера) путем автоматического составления и решения соответствующих систем уравнений на основе внутреннего представления ИК ПО, хранящегося в виде баз данных и баз знаний.

Известен способ (Патент №2515684, «Способ синтаксического анализа языка программирования с расширяемой грамматикой»), решающий задачу динамической модификации таблиц компиляции LR синтаксического анализатора за счет заданных отдельно для каждого уровня иерархии вложенности грамматических правил языка программирования директив расширения грамматики, предназначенных для введения новых грамматических конструкций. Использование данного способа направлено на создание инструмента, позволяющего для решения любых специфических задач использовать универсальный язык программирования с расширяемой грамматикой.

Известен способ (Патент №2103728, «Способ преобразования входной программы транслятора и устройство для его осуществления»), позволяющий решать задачу быстрого доступа к актуальным значениям идентификаторов в дереве трансляции за счет запоминания указателей таблицы идентификаторов для синтаксического дерева вместо запоминания имен в синтаксическом дереве.

Известен способ (Патент №2115158, «Способ и устройство для достоверной оценки сематических признаков в синтаксическом анализе при проходе вперед слева направо»), осуществляющий определенный вид семантического анализа (проверку семантических признаков) во время работы синтаксического анализатора за счет модификации формата узлов в дереве разбора и усовершенствования действий, связанных с грамматическими правилами вывода. Данный способ синтаксического анализа позволяет осуществить проверку сематических признаков, связанных с требованиями спецификации языка программирования, а также проконтролировать синтаксическую корректность конструкций в ИК, за один проход одновременно с построением дерева разбора, что снижает время, требуемое для компиляции программы.

Наиболее близким технически решением, принятым за прототип, является известный способ построения синтаксических деревьев (Ахо Альфред В., Лам, Моника С., Сети Рави, Ульман Джеффри Д. Компиляторы: принципы, технологии и инструментарий, 2-е изд.: Пер. с англ. - М.: ООО «И.Д. Вильяме», 2008. - 1184 с.: ил. - Парал. тит. англ., разд. 5.3.1.), позволяющий с помощью синтаксически управляемого определения формировать внутреннее представление программы в виде АСД. Для чего каждой продукции исходной грамматики назначается семантическое правило создания объекта узла АСД с соответствующим количеством полей.

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

Указанный технический результат достигается за счет того, что в синтаксическом управляемом определении (СУО) способа, основанного на способе построения синтаксических деревьев, семантические правила дополняются полем для операций с ЕС идентификаторов, позволяющие при проведении синтаксического анализа строить модифицированное АСД, в процессе восходящего обхода которого осуществляется контроль неизменности ЕС идентификаторов, хранящейся в дополненной таблице символов в виде одномерно целочисленного массива из девяти элементов.

Для построения модифицированного АСД продукциям контекстно-свободной грамматики языка программирования в СУО ставятся в соответствие программные конструкции (например, в объектно-ориентированном стиле), описывающие создание узлов АСД. Структура внутреннего узла дополняется полем для операции с ЕС идентификаторов ИК (op_NS), которое заполняется автоматически в зависимости от операции с идентификаторами в данном узле (op_I) и на основе размерной однородности физических уравнений, таблица соответствия которых представлена на фиг. 1.

Конструктор для создания объекта дополненного внутреннего узла АСД имеет вид: Node (op_I, op_NS, c₁, …, c_k), где op_I - метка узла и операция с идентификаторами; op_NS - операция с ЕС идентификаторов; с₁, …,c_k - k дополнительных полей для ссылок на «дочерние» объекты.

Конструктор для создания узла, являющегося листом: Leaf (op, val), где op - метка узла; val - лексическое значение, представленное либо ссылкой на таблицу символов для идентификаторов, либо константу.

При применении продукций СУО в процессе синтаксического разбора создаются объекты узлов модифицированного АСД, согласно конструкторам описанным выше.

ЕС идентификаторов ИК (размерность физической величины) не может быть получена путем анализа исходной программы и должна назначаться вручную. Предлагается после проведения лексического и синтаксического анализа инициализировать таблицу символов значениями ЕС для обнаруженных идентификаторов. Для чего таблица символов должна быть расширена полем для хранения одномерного целочисленного массива из девяти элементов (int natSem[9]), который позволит описать размерность любой физической величины, интерпретируемой в идентификаторе ИК. Формула размерности произвольной физической величины (А) имеет вид: , где e_j - степень j-го сомножителя формулы размерности физической величины. Элементами массива являются степени сомножителей в формуле размерности физической величины natSem[j - 1] = e_j, распределение которых по сопоставляющим формулы размерности представлено на фиг. 2. Идентификаторам, не обладающим ЕС, соответствует массив из нулевых элементов.

Для непосредственного проведения верификации ПО необходимо осуществить восходящий обход модифицированного АСД, то есть обход, который вычисляет значения ЕС «родительского» узла после вычисления значений в «дочерних». Значения ЕС листьев АСД хранятся в таблице символов, получение которых возможно осуществить при помощи функции доступа к значениям поля в таблице символов по ссылке val объекта листа (getNaturalSemantics(val)). При выполнении обхода АСД в зависимости от операции в узле op_NS возможны два варианта действий: расчет результирующего значения ЕС и контроль выполнения условия корректности выражения ИК (фиг. 1).

Расчет значения ЕС «родительского» узла АСД производится путем сложения или вычитания (op_NS) значений ЕС «дочерних» узлов, помеченных идентификаторами ИК. Сложение и вычитание значений ЕС идентификаторов с числами (num) не производится, результирующее значение ЕС равняется значению ЕС идентификатора «дочернего» узла. Так как ЕС представлена в виде массива, то необходимая операция (op_NS) с операндами выражения выполняется поэлементно и результатом является массив той же размерности.

Контроль выполнения условия корректности выражений ИК выполняется с целью выявления нарушений принципа размерной однородности физических уравнений, представленных в конструкциях ИК, исходя из значений ЕС идентификаторов в таблице символов. Невыполнение условия корректности выражения ИК свидетельствует о логическом дефекте в программе.

В качестве доказательства возможности осуществления заявленного изобретения с достижением вышеуказанного технического результата рассматривается программная конструкция для выражения для расчета координат при равноускоренном движении: 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.

Шаги обхода АСД для расчета ЕС и контроля условий корректности выражений ИК:

sem₁ = getNaturalSemantics(t); /* {0,0,1,0,0,0,0,0,0} */

sem₂ = num. val;

sem₃ = sem₁, /* {0,0,1,0,0,0,0,0,0} */

sem₄ = getNaturalSemantics{t); /* {0,0,1,0,0,0,0,0,0} */

sem₅ = sem₄ + sem₃; /* {0,0,2,0,0,0,0,0,0} */

sem₆ = getNaturalSemantics(a); /* {1,0,-2,0,0,0,0,0,0} */

sem₇ = sem₆ + sem₅; /* {1,0,0,0,0,0,0,0,0} */

sem₈ = getNaturalSemantics(v), /* {1,0,-1,0,0,0,0,0,0} */

sem₉ = getNaturalSemantics(t)\ /* {0,0,1,0,0,0,0,0,0} */

sem₁₀ = sem₉ + sem₈; /* {1,0,0,0,0,0,0,0,0} */

sem₁₁ = sem₁₀; /* {1,0,0,0,0,0,0,0,0}, T_ПО = 0*/

sem₁₂ = getNaturalSemantics(x0), /* {1,0,0,0,0,0,0,0,0} */

sem₁₃ = sem₁₂; /* {1,0,0,0,0,0,0,0,0}, T_ПО = 0 */

sem₁₄ = getNaturalSemantics(x); /* {1,0,0,0,0,0,0,0,0} */

sem₁₅ = sem₁₄; /* {1,0,0,0,0,0,0,0,0}, T_ПО = 0 */.

Результирующее значения EC выражения равно sem₁₅, условия корректности выполнены (T_ПО = 0).

Если в данном примере заменить идентификатор а на v, то выражение примет вид: x = x0+v*t+v*t*t/2. Шаги обхода модифицированного АСД, с изменившимися значениями, следующие:

sem₆ = getNaturalSemantics(v); /* {1,0,-1,0,0,0,0,0,0} */

sem₇ = sem₆+sem₅; /* {1,0,1,0,0,0,0,0,0} */

sem₁₁ = sem₁₀; /* {1,0,0,0,0,0,0,0,0}, T_ПО ≠ 0 */.

Условие корректности на шаге 11 не выполнено (Т_ПО ≠ 0), следовательно существует дефект ЕС в проверяемом на данном узле, либо в его «дочерних» узлах.

Таким образом, в настоящем изобретении доказана возможность обнаружения нового для статического анализа типа дефектов - дефектов ЕС идентификаторов ИК программы, что позволит повысить эффективность статического анализа и снизить суммарные затраты на проведение верификации ПО.

Изобретение относится к способу верификации программного обеспечения. Технический результат заключается в автоматизации верификации программного обеспечения. В способе семантические правила для создания узлов абстрактного синтаксического дерева синтаксически управляемого определения, исходя из размерной однородности физических уравнений, реализованных в выражениях исходного кода программы, дополняют полем для операции с естественной семантикой идентификаторов, представленной в виде размерности физической величины, интерпретируемой в идентификаторе и описанной одномерным целочисленным массивом, хранящимся в таблице символов, инициализируемой значениями естественной семантики идентификаторов после проведения лексического и синтаксического анализов, при этом указанное поле заполняется автоматически в зависимости от операции с идентификаторами в данном узле, при выполнении восходящего обхода модифицированного абстрактного синтаксического дерева вычисляют значения естественной семантики во внутренних узлах и контролируют выполнение условий корректности выражений исходного кода программы, исходя из значений естественной семантики идентификаторов в таблице символов. 4 ил.

Способ верификации программного обеспечения, заключающийся в статическом анализе исходного кода программы, отличающийся тем, что семантические правила для создания узлов абстрактного синтаксического дерева синтаксически управляемого определения, исходя из размерной однородности физических уравнений, реализованных в выражениях исходного кода программы, дополняют полем для операции с естественной семантикой идентификаторов, представленной в виде размерности физической величины, интерпретируемой в идентификаторе, и описанной одномерным целочисленным массивом из девяти элементов, хранящимся в таблице символов, инициализируемой значениями естественной семантики идентификаторов после проведения лексического и синтаксического анализов, при этом указанное поле заполняется автоматически в зависимости от операции с идентификаторами в данном узле и на основе размерной однородности физических уравнений, при выполнении восходящего обхода модифицированного абстрактного синтаксического дерева вычисляют значения естественной семантики во внутренних узлах и контролируют выполнение условий корректности выражений исходного кода программы, исходя из значений естественной семантики идентификаторов в таблице символов.