Анализ формы (программный анализ) - Shape analysis (program analysis)

В программный анализ, анализ формы это статический анализ кода метод, который обнаруживает и проверяет свойства связаны, динамически распределяется структуры данных в (обычно императив ) компьютерные программы. Обычно он используется во время компиляции для поиска ошибок программного обеспечения или для проверки свойств корректности программ на высоком уровне. В Ява программы, его можно использовать для проверки правильности сортировки списка методом сортировки. Для программ C он может искать места, где блок памяти не освобожден должным образом.

Приложения

Анализ формы применялся к множеству задач:

• Безопасность памяти: находка утечки памяти, разыменования висячие указатели и обнаружение случаев, когда блок памяти освобождается более одного раза.^[1][2]
• Обнаружение ошибок выхода за пределы массива^{[нужна цитата ]}
• Проверка свойства типа-состояния (например, убедитесь, что файл открыто() прежде чем это читать())^{[нужна цитата ]}
• Обеспечение того, чтобы метод обратного связанный список не вводит циклы в список^[2]
• Проверка того, что метод сортировки возвращает результат в отсортированном порядке^{[нужна цитата ]}

Пример

Анализ формы - это форма анализ указателя, хотя он более точен, чем обычный анализ указателя. Анализ указателя пытается определить набор объектов, на которые может указывать указатель (называемый набором точек указателя). К сожалению, этот анализ обязательно является приблизительным (поскольку совершенно точный статический анализ может решить проблема остановки ). Анализ формы может определять меньшие (более точные) наборы точек.

Рассмотрим следующую простую программу на C ++.

Элемент *Предметы[10];за (int я = 0; я < 10; ++я) {    Предметы[я] = новый Элемент(...); // строка 1]}process_items(Предметы); // строка [2]за (int я = 0; я < 10; ++я) {    Удалить Предметы[я]; // строка [3]}

Эта программа создает массив объектов, обрабатывает их произвольным образом, а затем удаляет их. Предполагая, что process_items Функция не содержит ошибок, ясно, что программа безопасна: она никогда не ссылается на освобожденную память и удаляет все созданные ею объекты.

К сожалению, большинство анализов указателей затрудняют точный анализ этой программы. Чтобы определить наборы точек, анализ указателя должен иметь возможность имя объекты программы. Как правило, программы могут размещать неограниченное количество объектов; но для завершения анализ указателя может использовать только конечный набор имен. Типичное приближение - дать всем объектам, размещенным в данной строке программы, одно и то же имя. В приведенном выше примере все объекты, построенные в строке [1], будут иметь одинаковое имя. Поэтому, когда Удалить Если оператор анализируется впервые, анализ определяет, что один из объектов с именем [1] удаляется. При втором анализе оператора (поскольку он находится в цикле) анализ предупреждает о возможной ошибке: поскольку он не может различить объекты в массиве, возможно, что второй Удалить удаляет тот же объект, что и первый Удалить. Это предупреждение является ложным, и цель анализа формы - избежать таких предупреждений.

Обобщение и материализация

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

Массив объектов в приведенном выше примере суммирован по отдельности в строках [1], [2] и [3]. В строке [1] массив построен только частично. Элементы массива 0..i-1 содержат сконструированные объекты. Элемент массива i собирается быть построен, а следующие элементы не инициализированы. Анализ формы может аппроксимировать эту ситуацию, используя сводку для первого набора элементов, материализованную ячейку памяти для элемента i и сводку для остальных неинициализированных местоположений, как показано ниже:

0 .. i-1	я	я + 1 .. 9
указатель на построенный объект (сводка)	неинициализированный	неинициализированный (сводка)

После завершения цикла в строке [2] нет необходимости сохранять что-либо материализованным. На этом этапе анализ формы определяет, что все элементы массива были инициализированы:

0 .. 9

указатель на построенный объект (сводка)

Однако в строке [3] элемент массива я снова используется. Следовательно, анализ разбивает массив на три сегмента, как в строке [1]. Но на этот раз первый сегмент перед я был удален, а остальные элементы все еще действительны (при условии, что Удалить оператор еще не выполнен).

0 .. i-1	я	я + 1 .. 9
бесплатно (резюме)	указатель на построенный объект	указатель на построенный объект (сводка)

Обратите внимание, что в этом случае анализ распознает, что указатель на index я еще не удален. Таким образом, он не предупреждает о двойном удалении.

Смотрите также

• Анализ псевдонимов
• Анализ побега

Рекомендации

1. Ринецки, Ноам; Сагив, Мули (2001). «Межпроцедурный анализ формы для рекурсивных программ» (PDF). Конструкция компилятора. Конспект лекций по информатике. 2027. стр.133–149. Дои:10.1007/3-540-45306-7_10. ISBN  978-3-540-41861-0.
2. Бердин, Джош; Кальканьо, Криштиану; Повар, Байрон; Дистефано, Дино; о'Хирн, Питер В .; Виз, Томас; Ян, Хонгсок (2007). «Анализ формы для составных структур данных» (PDF). Компьютерная проверка. Конспект лекций по информатике. 4590. С. 178–192. Дои:10.1007/978-3-540-73368-3_22. ISBN  978-3-540-73367-6.

Библиография

• Нил Д. Джонс; Стивен С. Мучник (1982). «Гибкий подход к межпроцедурному анализу потоков данных и программ с рекурсивными структурами данных». POPL '82 Материалы 9-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования. ACM: 66–74. Дои:10.1145/582153.582161. ISBN  0897910656.

• Мули Сагив; Томас Репс; Райнхард Вильгельм (Май 2002 г.). «Параметрический анализ формы с помощью трехзначной логики» (PDF). Транзакции ACM по языкам и системам программирования. ACM. 24 (3): 217–298. CiteSeerX  10.1.1.147.2132. Дои:10.1145/292540.292552.

• Вильгельм, Рейнхард; Сагив, Мули; Репс, Томас (2007). «Глава 12: Анализ формы и приложения». В Srikant, Y. N .; Шанкар, Прити (ред.). Справочник по проектированию компиляторов: Оптимизация и генерация машинного кода, второе издание. CRC Press. С. 12–1–12–44. ISBN  978-1-4200-4382-2.