Анализ программ весна 2020 — различия между версиями

Материал из CSC Wiki
Перейти к:навигация, поиск
(Новая страница: « == Лекции == Преподаватели: Ахин Марат ('''akhin@kspt.icc.spbstu.ru'''), Беляев Михаил ('''belyaev@kspt.icc.spbstu.ru''')»)
 
(не показана 1 промежуточная версия этого же участника)
Строка 1: Строка 1:
 +
Преподаватели: Марат Ахин ('''akhin@kspt.icc.spbstu.ru'''), Михаил Беляев ('''belyaev@kspt.icc.spbstu.ru''')
 +
 +
Ссылки на предыдущие прочтения:
 +
 +
* [[Анализ_программ_3_модуль_2019]]
 +
* [[Анализ программ 4MIT весна 2018]]
  
 
== Лекции ==
 
== Лекции ==
  
Преподаватели: Ахин Марат ('''akhin@kspt.icc.spbstu.ru'''), Беляев Михаил ('''belyaev@kspt.icc.spbstu.ru''')
+
=== Лекция 1 ===
 +
 
 +
Введение в предмет курса. '''[[Медиа:StaticAnalysis2020Lection1.pdf|Слайды]]'''
 +
 
 +
=== Лекция 2 ===
 +
 
 +
Статический анализ на основе систем типов. '''[[Медиа:StaticAnalysis2020Lection2.pdf|Слайды]]'''
 +
 
 +
=== Лекция 3 ===
 +
 
 +
Теория решеток. '''[[Медиа:StaticAnalysis2020Lection3.pdf|Слайды]]'''
 +
 
 +
<!---
 +
=== Лекция 4 ===
 +
 
 +
Потокочувствительные анализы. '''[[Медиа:StaticAnalysis2019Lection4.pdf|Слайды]]'''
 +
 
 +
=== Лекция 5 ===
 +
 
 +
Интервальный анализ. '''[[Медиа:StaticAnalysis2019Lection5.pdf|Слайды]]'''
 +
 
 +
=== Лекция 6 ===
 +
 
 +
Чувствительность к путям и анализ зависимостей. '''[[Медиа:StaticAnalysis2019Lection6.pdf|Слайды]]'''
 +
 
 +
=== Лекция 7 ===
 +
 
 +
Ограниченная проверка моделей. '''[[Медиа:StaticAnalysis2019Lection7.pdf|Слайды]]'''
 +
 
 +
=== Лекция 8===
 +
 
 +
Межпроцедурность и с чем её едят. '''[[Медиа:StaticAnalysis2019Lection8.pdf|Слайды]]'''
 +
 
 +
=== Лекция 9 ===
 +
 
 +
Анализ указателей. '''[[Медиа:StaticAnalysis2019Lection9.pdf|Слайды]]'''
 +
 
 +
=== Лекция 10 ===
 +
 
 +
Память и указатели. Проблемы и решения. '''[[Медиа:StaticAnalysis2019Lection10.pdf|Слайды]]'''
 +
--->
 +
 
 +
== Практика ==
 +
 
 +
Ссылка на репозиторий с TIP: https://github.com/vorpal-research/TIP
 +
 
 +
'''НЕ ВЫКЛАДЫВАЙТЕ РЕШЕНИЯ В ОТКРЫТЫЙ ДОСТУП''' --- это просьба от коллег из университета Орхуса, откуда взяли существенную часть этого курса.
 +
В частности, не выкладывайте решения в открытые репозитории на GitHub.
 +
Используйте сервисы закрытых репозиториев.
 +
 
 +
Задания "на подумать" следует делать в кросс-платформенном человеко-читаемом формате (.pdf, .md, .smth) и складывать в свой форк базового репозитория в папку с говорящим именем (docs, reports).
 +
 
 +
=== Задание к лекции 2 ===
 +
 
 +
# Дописать реализацию класса [https://github.com/vorpal-research/TIP/blob/master/src/tip/analysis/TypeAnalysis.scala TypeAnalysis] в TIP. Подумайте, как будет работать анализ, если в программе есть рекурсивный тип.
 +
## Для консистентного создания экземпляров типов из узлов дерева можно использовать ''TipType.ast2typevar''
 +
# Попробуйте добавить в описанную в лекции систему типов тип 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 для получившегося анализа и посмотрите, что для него получается
 +
#** Для этого можно воспользоваться результатами пункта 3
 +
# Допишите реализацию метода widen в IntervalAnalysisWorklistSolverWithWidening [https://github.com/vorpal-research/TIP/blob/master/src/tip/analysis/IntervalAnalysis.scala здесь].
 +
# Реализуйте придуманный вами анализ размера переменных в файле VariableSizeAnalysis.scala рядом.
 +
 
 +
=== Задание к лекции 6 ===
 +
 
 +
# Напишите вариант программы, для которой анализ открытости-закрытости файлов не показывает корректный результат даже с учётом всех возможных условий в переходах
 +
# Предложите, каким образом можно решить описанные в лекции проблемы в этой ситуации
 +
 
 +
=== Задание к лекции 7 ===
 +
 
 +
Не будет 🙌
 +
 
 +
=== Задание к лекции 8 ===
 +
 
 +
# Напишите вариант программы, для которой контекстно-чувствительный анализ знаков требует коэффициент k > 1
 +
# Приведите пример решётки, для которой контекстно-чувствительный анализ в функциональном стиле является более ресурсозатратным, чем контекстно-чувствительный анализ по месту вызова с глубиной, например, 2
 +
 
 +
=== Задание к лекции 9 ===
 +
 
 +
Не будет 🙌
 +
 
 +
=== Задание к лекции 10 ===
 +
 
 +
Не будет 🙌
 +
--->

Версия 11:32, 12 февраля 2020

Преподаватели: Марат Ахин (akhin@kspt.icc.spbstu.ru), Михаил Беляев (belyaev@kspt.icc.spbstu.ru)

Ссылки на предыдущие прочтения:

Лекции

Лекция 1

Введение в предмет курса. Слайды

Лекция 2

Статический анализ на основе систем типов. Слайды

Лекция 3

Теория решеток. Слайды


Практика

Ссылка на репозиторий с TIP: https://github.com/vorpal-research/TIP

НЕ ВЫКЛАДЫВАЙТЕ РЕШЕНИЯ В ОТКРЫТЫЙ ДОСТУП --- это просьба от коллег из университета Орхуса, откуда взяли существенную часть этого курса. В частности, не выкладывайте решения в открытые репозитории на GitHub. Используйте сервисы закрытых репозиториев.

Задания "на подумать" следует делать в кросс-платформенном человеко-читаемом формате (.pdf, .md, .smth) и складывать в свой форк базового репозитория в папку с говорящим именем (docs, reports).

Задание к лекции 2

  1. Дописать реализацию класса TypeAnalysis в TIP. Подумайте, как будет работать анализ, если в программе есть рекурсивный тип.
    1. Для консистентного создания экземпляров типов из узлов дерева можно использовать TipType.ast2typevar
  2. Попробуйте добавить в описанную в лекции систему типов тип Bool, не меняя синтаксис языка. Перепишите правила так, чтобы они продолжали работать на основе имеющегося алгоритма унификации.
  3. (опционально) Реализуйте пункт 2 в рамках пункта 1.
  4. Попробуйте добавить в описанную в лекции систему типов тип массива (при этом меняется синтаксис, см. слайды). Перепишите правила и попробуйте протипизировать программу из лекции.

Задание к лекции 3

  1. Подумайте, выразим ли анализ типов в монотонном фреймворке? А наоборот?
  2. Допишите метод transfer в трейте IntraprocSignAnalysisFunctions здесь.
  3. Реализуйте класс PowersetLattice в файле GenericLattices.