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

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

 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

sem2 = num. val;

sem3 = sem1, /* {0,0,1,0,0,0,0,0,0} */

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

sem5 = sem4 + sem3; /* {0,0,2,0,0,0,0,0,0} */

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

sem7 = sem6 + sem5; /* {1,0,0,0,0,0,0,0,0} */

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

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

sem10 = sem9 + sem8; /* {1,0,0,0,0,0,0,0,0} */

sem11 = sem10; /* {1,0,0,0,0,0,0,0,0}, TПО = 0*/

sem12 = getNaturalSemantics(x0), /* {1,0,0,0,0,0,0,0,0} */

sem13 = sem12; /* {1,0,0,0,0,0,0,0,0}, TПО = 0 */

sem14 = getNaturalSemantics(x); /* {1,0,0,0,0,0,0,0,0} */

sem15 = sem14; /* {1,0,0,0,0,0,0,0,0}, TПО = 0 */.

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

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

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

sem7 = sem6+sem5; /* {1,0,1,0,0,0,0,0,0} */

sem11 = sem10; /* {1,0,0,0,0,0,0,0,0}, TПО ≠ 0 */.

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

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

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



 

Похожие патенты:

Изобретение относится к устройствам мобильной связи, а именно к обеспечению доверия работы изолированных операционных систем. Технический результат – повышение безопасности изменения рабочего состояния устройства.

Изобретение относится к системе и способу защиты финансовых устройств. Технический результат заключается в повышении безопасности финансовых устройств.

Изобретение относится к вычислительной технике. Технический результат заключается в повышении быстродействия при работе в базах данных с использованием систем управления базами данных.

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

Изобретение относится к области вычислительной техники. Техническим результатом является возможность управления обновлениями программного обеспечения в системах с каскадной структурой.

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

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

Изобретение относится к области аутентификации пользователей. Технический результат – повышение эффективности аутентификации.

Изобретение относится к технологиям сетевой связи. Технический результат заключается в повышении безопасности передачи данных.

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

Изобретение относится к способам и серверам для автоматического создания тезауруса. Техническим результатом является расширение арсенала технических средств автоматического создания цифрового тезауруса.

Изобретение относится к способам и серверам для автоматического создания тезауруса. Техническим результатом является расширение арсенала технических средств автоматического создания цифрового тезауруса.

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

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

Изобретение относится к области обработки текста. Технический результат – повышение точности при выборе текстовой области.

Изобретение относится к области обработки текста. Технический результат – повышение точности при выборе текстовой области.

Изобретение относится к переговорной диалоговой системе. Техническим результатом является расширение арсенала технических средств.

Изобретение относится к переговорной диалоговой системе. Техническим результатом является расширение арсенала технических средств.

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

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

Изобретение относится к способу и системе обработки данных. Технический результат заключается в обеспечении возможности поставщику разгрузки использовать большие маркеры. Способ содержит этапы, на которых принимают, посредством вычислительного устройства, два или более подмаркеров, каждый фиксированного размера, причем подмаркеры вместе представляют больший маркер, размер которого превосходит этот фиксированный размер, при этом больший маркер представляет данные, которые являются неизменными, пока больший маркер является действительным; получают, посредством вычислительного устройства из одного или более из упомянутых подмаркеров, криптографически стойкий ключ и информацию, которая идентифицирует источник, из которого можно получать данные, представляемые большим маркером; и предоставляют, посредством вычислительного устройства поставщику разгрузки, который содержит по меньшей мере одно другое вычислительное устройство, являющееся отдельным от упомянутого вычислительного устройства, подтверждение упомянутого ключа, чтобы получить часть данных, представляемых большим маркером, без прохождения этой части данных через инициатор, который предоставил упомянутые подмаркеры. 3 н. и 14 з.п. ф-лы, 9 ил.

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

Наверх