Анализ формы (программный анализ) - Shape analysis (program analysis)
 | Эта статья включает в себя список общих Рекомендации, но он остается в основном непроверенным, потому что ему не хватает соответствующих встроенные цитаты. (Февраль 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 и сводку для остальных неинициализированных местоположений, как показано ниже:
| 0 .. i-1 | я | я + 1 .. 9 |
| указатель на построенный объект (сводка) | неинициализированный | неинициализированный (сводка) |
После завершения цикла в строке [2] нет необходимости сохранять что-либо материализованным. На этом этапе анализ формы определяет, что все элементы массива были инициализированы:
| 0 .. 9 |
| указатель на построенный объект (сводка) |
Однако в строке [3] элемент массива я снова используется. Следовательно, анализ разбивает массив на три сегмента, как в строке [1]. Но на этот раз первый сегмент перед я был удален, а остальные элементы все еще действительны (при условии, что Удалить оператор еще не выполнен).
| 0 .. i-1 | я | я + 1 .. 9 |
| бесплатно (резюме) | указатель на построенный объект | указатель на построенный объект (сводка) |
Обратите внимание, что в этом случае анализ распознает, что указатель на index я еще не удален. Таким образом, он не предупреждает о двойном удалении.
Смотрите также
Рекомендации
- ^ Ринецки, Ноам; Сагив, Мули (2001). «Межпроцедурный анализ формы для рекурсивных программ» (PDF). Конструкция компилятора. Конспект лекций по информатике. 2027. стр.133–149. Дои:10.1007/3-540-45306-7_10. ISBN 978-3-540-41861-0.
- ^ а б Бердин, Джош; Кальканьо, Криштиану; Повар, Байрон; Дистефано, Дино; о'Хирн, Питер В .; Виз, Томас; Ян, Хонгсок (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.