WikiDer > Анализ формы (программный анализ)

Эта статья включает в себя список общих Рекомендации, но он остается в основном непроверенным, потому что ему не хватает соответствующих встроенные цитаты. Пожалуйста, помогите улучшать эта статья введение более точные цитаты. (Февраль 2018 г.) (Узнайте, как и когда удалить этот шаблон сообщения)

В программный анализ, анализ формы это статический анализ кода метод, который обнаруживает и проверяет свойства связаны, динамически распределяется структуры данных в (обычно императив) компьютерные программы. Обычно он используется во время компиляции для поиска ошибок программного обеспечения или для проверки свойств корректности программ на высоком уровне. В Ява программы, его можно использовать для проверки правильности сортировки списка методом сортировки. Для программ 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 и сводку для остальных неинициализированных местоположений, как показано ниже:

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

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

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

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

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

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

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

• Нил Д. Джонс; Стивен С. Мучник (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.