Статический анализ с использованием систем типов и эффектов на основе LLVM

Михаил Анатольевич Беляев; Вадим Александрович Цесько

doi:undefined

Статический анализ с использованием систем типов и эффектов на основе LLVM

Михаил Анатольевич Беляев, Вадим Александрович Цесько

Полный текст:

Аннотация

Описано разрабатываемое средство статического анализа программного обеспечения. Основной идеей данного средства является использование систем типов и эффектов для статического анализа реальных программ. Средство использует формат промежуточного представления LLVM в качестве входного представления программы, таким образом, давая возможность анализировать программы на любых языках, поддерживаемых системой LLVM. Разбор указанного формата осуществляется встроенным парсером, позволяющим осуществить формирование внутренней модели программы, схожей с моделью LLVM. Целью создания описываемого средства является исследование возможностей построения методов статического анализа программ на основе известных алгоритмов, использующих системы типов и эффектов, путём применения этих алгоритмов к модели и опосредованно к исходному коду.

Ключ. слова

статический анализ, системы типов и эффектов, поиск дефектов, SSA,

УДК: 004.415.5+004.416.2

Об авторах

Михаил Анатольевич Беляев

Санкт-Петербургский государственный политехнический университет
Россия

Вадим Александрович Цесько

Санкт-Петербургский государственный политехнический университет
Россия

Список литературы

1. Coverity Scan Open Source Report, 2009. <http://scan.coverity.com/report/>

2. Ertl M.A., Wien TU: Domination-Based Scoping and Static Single Assignment Languages. Static Single-Assignment Form Seminar, 2009.

3. Horwitz S. Precise Flow-Insensitive May-Alias Analysis is NP-Hard. ACM Transactions on Programming Languages and Systems, 1-6. ACM Association for Computing Machinery, 1997.

4. Itsykson V., Moiseev M., Tsesko V., Zakharov A. Automatic defects detection in industrial C/C++ software. Software Engineering Conference in Russia (CEE- SECR), 2009.

5. Jim T., Palsberg J. Type inference in systems of recursive types with subtyping. Manuscript, 1999.

6. Lattner C., Haberman J., Housel P. S. LLVM Bitcode File Format. <http://llvm.org/docs/BitCodeFormat.html>

7. Lattner C. LLVM Language Reference Manual. <http://llvm.org/docs/LangRef.html>

8. llvm-parser - A haskell library for parsing LLVM binary bitcode files. <http://code.google.com/p/llvm-parser>

9. Marino D., Millstein T. A Generic Type-and-Effect System. TLDI, 2010.

10. Nielson F., Nielson H. R. Type and Effect Systems. Correct System Design, 1999. P. 114-136.

11. Nielson F., Nielson H. R., Hankin C. Principles of Program Analysis. Springer- Verlag, 2005.

12. Ross K.P.D. From System F to Typed Assembly Language. Twenty-Fifth ACM SIGPLAN Symposium on Principles of Programming Languages. 1998. P. 85-97.

13. Zadeck K. The Development of Static Single Assignment Form. Static Single- Assignment Form Seminar, 2009.

Дополнительные файлы

Для цитирования: Беляев М.А., Цесько В.А. Статический анализ с использованием систем типов и эффектов на основе LLVM. Моделирование и анализ информационных систем. 2011;18(4):45-55.

For citation: Belyaev M.A., Tsesko V.A. LLVM-based Static Analysis Tool Using Type and Effect Systems. Modeling and Analysis of Information Systems. 2011;18(4):45-55. (In Russ.)

Обратные ссылки

Обратные ссылки не определены.

Контент доступен под лицензией Creative Commons Attribution 4.0 License.

ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)

Логин
Пароль