Анализ формы (программный анализ)
 | Эта статья включает список общих ссылок , но в ней отсутствуют достаточные соответствующие встроенные цитаты . ( февраль 2018 г. ) |
В анализе программ анализ формы — это метод статического анализа кода , который обнаруживает и проверяет свойства связанных , динамически выделяемых структур данных в (обычно императивных ) компьютерных программах. Обычно он используется во время компиляции для поиска ошибок в программном обеспечении или для проверки свойств корректности программ на высоком уровне. В программах Java его можно использовать для обеспечения правильной сортировки списка методом сортировки. В программах на языке C он может искать места, где блок памяти не освобожден должным образом.
Приложения
[ редактировать ]Анализ формы применялся для решения множества задач:
- Безопасность памяти: поиск утечек памяти , разыменования висячих указателей и обнаружение случаев, когда блок памяти освобождается более одного раза. [1] [2]
- Обнаружение ошибок выхода за пределы массива [ нужна ссылка ]
- Проверка свойств состояния типа (например, проверка того, что файл
open()прежде чем это произойдетread()) [ нужна ссылка ] - Обеспечение того, чтобы метод обращения связанного списка не вводил циклы в список. [2]
- Проверка того, что метод сортировки возвращает результат в отсортированном порядке. [ нужна ссылка ]
Пример
[ редактировать ]Анализ формы — это разновидность анализа указателей , хотя он более точен, чем обычный анализ указателей. Анализ указателя пытается определить набор объектов, на которые может указывать указатель (называемый набором точек указателя). К сожалению, этот анализ обязательно является приблизительным (поскольку совершенно точный статический анализ может решить проблему остановки ). Анализ формы может определить меньшие (более точные) наборы точек.
Рассмотрим следующую простую программу на C++.
Item *items[10];
for (int i = 0; i < 10; ++i) {
items[i] = new Item(...); // line [1]
}
process_items(items); // line [2]
for (int i = 0; i < 10; ++i) {
delete items[i]; // line [3]
}
Эта программа формирует массив объектов, обрабатывает их каким-то произвольным образом, а затем удаляет. Предполагая, что process_items функция не содержит ошибок, видно, что программа безопасна: она никогда не обращается к освобожденной памяти и удаляет все построенные ею объекты.
К сожалению, при большинстве анализов указателей возникают трудности с точным анализом этой программы. Чтобы определить наборы точек на, анализ указателей должен иметь возможность присваивать имена объектам программы. В общем, программы могут размещать неограниченное количество объектов; но для завершения анализа указателя можно использовать только конечный набор имен. Типичным приближением является присвоение всем объектам, расположенным в данной строке программы, одного и того же имени. В приведенном выше примере все объекты, созданные в строке [1], будут иметь одно и то же имя. Поэтому, когда delete оператор анализируется впервые, анализ определяет, что один из объектов с именем [1] удаляется. При втором анализе оператора (поскольку он находится в цикле) анализ предупреждает о возможной ошибке: поскольку он не может различить объекты в массиве, возможно, что второй delete удаляет тот же объект, что и первый delete. Это предупреждение является ложным, и цель анализа формы — избежать таких предупреждений.
Подведение итогов и материализация
[ редактировать ]Анализ формы решает проблемы анализа указателей за счет использования более гибкой системы именования объектов. Вместо того, чтобы давать объекту одно и то же имя во всей программе, объекты могут менять имена в зависимости от действий программы. Иногда несколько отдельных объектов с разными именами могут быть суммированы или объединены так, чтобы у них было одно и то же имя. Затем, когда суммированный объект будет использоваться программой, его можно материализовать , т. е. суммированный объект разбивается на два объекта с разными именами: один представляет один объект, а другой представляет остальные суммированные объекты. Основная эвристика анализа формы заключается в том, что объекты, используемые программой, представляются с помощью уникальных материализованных объектов, а неиспользуемые объекты суммируются.
Массив объектов в приведенном выше примере суммируется по отдельности в строках [1], [2] и [3]. В строке [1] массив построен лишь частично. Элементы массива 0..i-1 содержат построенные объекты. Элемент массива i скоро будет создан, а следующие элементы не инициализированы. Анализ формы может аппроксимировать эту ситуацию, используя сводку для первого набора элементов, материализованную ячейку памяти для элемента i и сводку для остальных неинициализированных ячеек следующим образом:
| 0 .. я-1 | я | я+1 .. 9 |
| указатель на созданный объект (сводка) | неинициализированный | неинициализированный (сводка) |
После завершения цикла в строке [2] нет необходимости сохранять что-либо материализованным. На этом этапе анализ формы определяет, что все элементы массива инициализированы:
| 0 .. 9 |
| указатель на созданный объект (сводка) |
Однако в строке [3] элемент массива i снова используется. Поэтому анализ разбивает массив на три сегмента, как в строке [1]. Однако на этот раз первый сегмент перед i был удален, а оставшиеся элементы все еще действительны (при условии, что delete оператор еще не выполнен).
| 0 .. я-1 | я | я+1 .. 9 |
| бесплатно (сводка) | указатель на созданный объект | указатель на созданный объект (сводка) |
Обратите внимание, что в этом случае анализ распознает, что указатель по индексу i еще не удален. Поэтому он не предупреждает о двойном удалении.
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Ринецкий, Ноам; Сагив, Мули (2001). «Межпроцедурный анализ формы для рекурсивных программ» (PDF) . Конструкция компилятора . Конспекты лекций по информатике. Том. 2027. С. 133–149 . дои : 10.1007/3-540-45306-7_10 . ISBN 978-3-540-41861-0 .
- ^ Jump up to: а б Бердин, Джош; Кальканьо, Криштиану; Кук, Байрон; Дистефано, Дино; о'Хирн, Питер В.; Вис, Томас; Ян, Хонсок (2007). «Анализ формы составных структур данных» (PDF) . Компьютерная проверка . Конспекты лекций по информатике. Том. 4590. стр. 178–192. дои : 10.1007/978-3-540-73368-3_22 . ISBN 978-3-540-73367-6 .
Библиография
[ редактировать ]- Нил Д. Джонс; Стивен С. Мучник (1982). «Гибкий подход к межпроцедурному анализу потоков данных и программам с рекурсивными структурами данных». Материалы 9-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования — POPL '82 . АКМ. стр. 66–74. дои : 10.1145/582153.582161 . ISBN 0897910656 . S2CID 13266723 .
{{cite book}}: CS1 maint: дата и год ( ссылка )
- Мули Сагив ; Томас Репс ; Рейнхард Вильгельм (май 2002 г.). «Параметрический анализ формы с помощью трехзначной логики» (PDF) . Транзакции ACM в языках и системах программирования . 24 (3). АКМ: 217–298. CiteSeerX 10.1.1.147.2132 . дои : 10.1145/292540.292552 . S2CID 101653 .
- Вильгельм, Рейнхард; Сагив, Мули; Репс, Томас (2007). «Глава 12: Анализ формы и приложения». В Шриканте, Ю.Н.; Шанкар, Прити (ред.). Справочник по проектированию компиляторов: оптимизации и генерация машинного кода, второе издание . ЦРК Пресс. стр. 12–1–12–44. ISBN 978-1-4200-4382-2 .