Анализ программ 4MIT весна 2018 — различия между версиями
(Новая страница: «Преподаватели: Ахин Марат ('''akhin@kspt.icc.spbstu.ru ''') Беляев Михаил ('''belyaev@kspt.icc.spbstu.ru ''') ==…») |
(→Лекции) |
||
(не показано 28 промежуточных версий 5 участников) | |||
Строка 1: | Строка 1: | ||
− | Преподаватели: Ахин Марат ('''akhin@kspt.icc.spbstu.ru ''') | + | Преподаватели: |
− | + | ||
+ | Ахин Марат ('''akhin@kspt.icc.spbstu.ru ''') | ||
+ | |||
+ | Беляев Михаил ('''belyaev@kspt.icc.spbstu.ru ''') | ||
== Лекции == | == Лекции == | ||
+ | |||
+ | === Лекция 1=== | ||
+ | |||
+ | Введение в предмет курса. '''[[Медиа:StaticAnalysis2018Lection1.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 2=== | ||
+ | |||
+ | Анализ на основе систем типов. '''[[Медиа:StaticAnalysis2018Lection2.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 3=== | ||
+ | |||
+ | Теория решеток и монотонный фреймворк. '''[[Медиа:StaticAnalysis2018Lection3.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 4=== | ||
+ | |||
+ | Примеры потокочувствительных анализов. '''[[Медиа:StaticAnalysis2018Lection4.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 5=== | ||
+ | |||
+ | Интервальный анализ. Widening и narrowing. '''[[Медиа:StaticAnalysis2018Lection5.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 6=== | ||
+ | |||
+ | Path sensitivity. Анализ зависимостей. '''[[Медиа:StaticAnalysis2018Lection6.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 7=== | ||
+ | |||
+ | Bounded model checking. '''[[Медиа:StaticAnalysis2018Lection7.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 8=== | ||
+ | |||
+ | Межпроцедурность и с чем её едят. '''[[Медиа:StaticAnalysis2018Lection8.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 9=== | ||
+ | |||
+ | Память и указатели. Проблемы и решения. '''[[Медиа:StaticAnalysis2018Lection9.pdf|Слайды]]''' | ||
+ | |||
+ | === Лекция 10=== | ||
+ | |||
+ | Анализ указателей. '''[[Медиа:StaticAnalysis2018Lection10.pdf|Слайды]]''' | ||
== Практика == | == Практика == | ||
+ | |||
+ | '''НЕ ВЫКЛАДЫВАЙТЕ РЕШЕНИЯ В ОТКРЫТЫЙ ДОСТУП''' - это просьба от коллег из университета | ||
+ | Орхуса ([https://upload.wikimedia.org/wikipedia/commons/4/49/%C3%85rhus.ogg ˈɒːhuːˀs]), | ||
+ | откуда взяли существенную часть этого курса. В частности, не выкладывайте решения в открытые репозитории на GitHub. Используйте сервисы закрытых репозиториев (например, Gitlab или Bitbucket). | ||
+ | |||
+ | === Задание к лекции 2 === | ||
+ | |||
+ | # Дописать реализацию класса [https://github.com/vorpal-research/TIP/blob/master/src/tip/analysis/TypeAnalysis.scala TypeAnalysis] в TIP. Подумайте, как будет работать анализ, если в программе есть рекурсивный тип. | ||
+ | # Попробуйте добавить в описанную в лекции систему типов тип Bool, не меняя синтаксис языка. Перепишите правила так, чтобы они продолжали работать на основе имеющегося алгоритма унификации. | ||
+ | # (опционально) Реализуйте пункт 2 в рамках пункта 1. | ||
+ | # Попробуйте добавить в описанную в лекции систему типов тип массива (при этом меняется синтаксис, см. слайды). Перепишите правила и попробуйте протипизировать программу из лекции. | ||
+ | |||
+ | === Задание к лекции 3 === | ||
+ | |||
+ | # Подумайте, выразим ли анализ типов в монотонном фреймворке? А наоборот? | ||
+ | # Допишите метод transfer в трейте IntraprocSignAnalysisFunctions [https://github.com/vorpal-research/TIP/blob/master/src/tip/analysis/SignAnalysis.scala здесь]. | ||
+ | # Реализуйте класс PowersetLattice в файле [https://github.com/vorpal-research/TIP/blob/master/src/tip/lattices/GenericLattices.scala GenericLattices]. | ||
+ | |||
+ | === Задание к лекции 4 === | ||
+ | |||
+ | # Рассмотрим плоскую решётку над типами {Bool,Int} из задания 1. Если реализовать для неё анализ, каким по предложенной классификации он будет? Попробуйте выписать правила вывода. | ||
+ | # Дореализуйте live variables analysis [https://github.com/vorpal-research/TIP/blob/master/src/tip/analysis/LiveVarsAnalysis.scala здесь]. | ||
+ | # Реализуйте reaching definitions analysis в файле ReachingDefsAnalysis.scala рядом. | ||
+ | |||
+ | === Задание к лекции 5 === | ||
+ | |||
+ | # Допустим, мы хотим реализовать оптимизирующий компилятор для языка TIP. Среди прочего, для работы ему требуется информация о размерах различных переменных: bool (1 bit), byte (8 bit signed), char (16 bit unsigned), int (32 bit signed), bigint (any integer), any (any other thing). | ||
+ | #* Предложите решетку для реализации анализа размера переменных | ||
+ | #** Нужно описать не только решетку для одного абстрактного значения, но и все другие решетки, требуемые для анализа целой программы | ||
+ | #* Опишите правила вычисления различных выражений | ||
+ | #* Придумайте нетривиальный пример программы на TIP для получившегося анализа и посмотрите, что для него получается | ||
+ | # Допишите реализацию метода widen в IntervalAnalysisWorklistSolverWithWidening [https://github.com/vorpal-research/TIP/blob/master/src/tip/analysis/IntervalAnalysis.scala здесь]. | ||
+ | # Реализуйте придуманный вами анализ размера переменных в файле VariableSizeAnalysis.scala рядом. | ||
+ | |||
+ | === Задание к лекции 6 === | ||
+ | |||
+ | # Напишите вариант программы, для которой анализ открытости-закрытости файлов не показывает корректный результат даже с учётом всех возможных условий в переходах | ||
+ | # Предложите, каким образом можно решить описанные в лекции проблемы в этой ситуации | ||
+ | |||
+ | === Задание к лекции 7 === | ||
+ | |||
+ | Не будет 🙌 | ||
+ | |||
+ | === Задание к лекции 8 === | ||
+ | |||
+ | # Напишите вариант программы, для которой контекстно-чувствительный анализ знаков требует коэффициент k > 1 | ||
+ | # Приведите пример решётки, для которой контекстно-чувствительный анализ в функциональном стиле является более ресурсозатратным, чем контекстно-чувствительный анализ по месту вызова с глубиной, например, 2 | ||
+ | |||
+ | === Задание к лекции 9 === | ||
+ | |||
+ | Не будет 🙌 |
Текущая версия на 18:14, 25 апреля 2018
Преподаватели:
Ахин Марат (akhin@kspt.icc.spbstu.ru )
Беляев Михаил (belyaev@kspt.icc.spbstu.ru )
Содержание
Лекции
Лекция 1
Введение в предмет курса. Слайды
Лекция 2
Анализ на основе систем типов. Слайды
Лекция 3
Теория решеток и монотонный фреймворк. Слайды
Лекция 4
Примеры потокочувствительных анализов. Слайды
Лекция 5
Интервальный анализ. Widening и narrowing. Слайды
Лекция 6
Path sensitivity. Анализ зависимостей. Слайды
Лекция 7
Bounded model checking. Слайды
Лекция 8
Межпроцедурность и с чем её едят. Слайды
Лекция 9
Память и указатели. Проблемы и решения. Слайды
Лекция 10
Анализ указателей. Слайды
Практика
НЕ ВЫКЛАДЫВАЙТЕ РЕШЕНИЯ В ОТКРЫТЫЙ ДОСТУП - это просьба от коллег из университета Орхуса (ˈɒːhuːˀs), откуда взяли существенную часть этого курса. В частности, не выкладывайте решения в открытые репозитории на GitHub. Используйте сервисы закрытых репозиториев (например, Gitlab или Bitbucket).
Задание к лекции 2
- Дописать реализацию класса TypeAnalysis в TIP. Подумайте, как будет работать анализ, если в программе есть рекурсивный тип.
- Попробуйте добавить в описанную в лекции систему типов тип Bool, не меняя синтаксис языка. Перепишите правила так, чтобы они продолжали работать на основе имеющегося алгоритма унификации.
- (опционально) Реализуйте пункт 2 в рамках пункта 1.
- Попробуйте добавить в описанную в лекции систему типов тип массива (при этом меняется синтаксис, см. слайды). Перепишите правила и попробуйте протипизировать программу из лекции.
Задание к лекции 3
- Подумайте, выразим ли анализ типов в монотонном фреймворке? А наоборот?
- Допишите метод transfer в трейте IntraprocSignAnalysisFunctions здесь.
- Реализуйте класс PowersetLattice в файле GenericLattices.
Задание к лекции 4
- Рассмотрим плоскую решётку над типами {Bool,Int} из задания 1. Если реализовать для неё анализ, каким по предложенной классификации он будет? Попробуйте выписать правила вывода.
- Дореализуйте live variables analysis здесь.
- Реализуйте reaching definitions analysis в файле ReachingDefsAnalysis.scala рядом.
Задание к лекции 5
- Допустим, мы хотим реализовать оптимизирующий компилятор для языка TIP. Среди прочего, для работы ему требуется информация о размерах различных переменных: bool (1 bit), byte (8 bit signed), char (16 bit unsigned), int (32 bit signed), bigint (any integer), any (any other thing).
- Предложите решетку для реализации анализа размера переменных
- Нужно описать не только решетку для одного абстрактного значения, но и все другие решетки, требуемые для анализа целой программы
- Опишите правила вычисления различных выражений
- Придумайте нетривиальный пример программы на TIP для получившегося анализа и посмотрите, что для него получается
- Предложите решетку для реализации анализа размера переменных
- Допишите реализацию метода widen в IntervalAnalysisWorklistSolverWithWidening здесь.
- Реализуйте придуманный вами анализ размера переменных в файле VariableSizeAnalysis.scala рядом.
Задание к лекции 6
- Напишите вариант программы, для которой анализ открытости-закрытости файлов не показывает корректный результат даже с учётом всех возможных условий в переходах
- Предложите, каким образом можно решить описанные в лекции проблемы в этой ситуации
Задание к лекции 7
Не будет 🙌
Задание к лекции 8
- Напишите вариант программы, для которой контекстно-чувствительный анализ знаков требует коэффициент k > 1
- Приведите пример решётки, для которой контекстно-чувствительный анализ в функциональном стиле является более ресурсозатратным, чем контекстно-чувствительный анализ по месту вызова с глубиной, например, 2
Задание к лекции 9
Не будет 🙌