Статический анализ с использованием систем типов и эффектов на основе LLVM
Аннотация
Описано разрабатываемое средство статического анализа программного обеспечения. Основной идеей данного средства является использование систем типов и эффектов для статического анализа реальных программ. Средство использует формат промежуточного представления LLVM в качестве входного представления программы, таким образом, давая возможность анализировать программы на любых языках, поддерживаемых системой LLVM. Разбор указанного формата осуществляется встроенным парсером, позволяющим осуществить формирование внутренней модели программы, схожей с моделью LLVM. Целью создания описываемого средства является исследование возможностей построения методов статического анализа программ на основе известных алгоритмов, использующих системы типов и эффектов, путём применения этих алгоритмов к модели и опосредованно к исходному коду.
Об авторах
Михаил Анатольевич Беляев
Санкт-Петербургский государственный политехнический университет
Россия
Россия
Вадим Александрович Цесько
Санкт-Петербургский государственный политехнический университет
Россия
Россия
Список литературы
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.)
Просмотров:
587
Послать статью по эл. почте 