maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1097Research ArticleОригинальные статьиArticlesСтатический анализ с использованием систем типов и эффектов на основе LLVMLLVM-based Static Analysis Tool Using Type and Effect SystemsБеляевМихаил АнатольевичBelyaevM. A.belyaev@kspt.ftk.spbstu.ruЦеськоВадим АлександровичTseskoV. A.tsesko@kspt.ftk.spbstu.ruСанкт-Петербургский государственный политехнический университетRussian Federation2011201220111844555Copyright © Беляев М.А., Цесько В.А., 20112011Беляев М.А., Цесько В.А.Belyaev M.A., Tsesko V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1097

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

The intention of this paper is to describe a static analysis tool under development. The principal idea behind the design of this tool is to use type and effect systems for static analysis of real programs. The tool uses LLVM bitcode files as input, thus extending the set of analyzed languages to those supported by LLVM compiler infrastructure. It uses its own parser of bitcode files and a program model similar to that of LLVM. The approach taken is to research feasibility of designing instruments for static analysis by applying known type and effect system based algorithms for detecting defects to LLVM bitcode language and effectively to the original source code.

статический анализсистемы типов и эффектовпоиск дефектовSSAstatic program analysistype and effect systemlow level virtual machinedefect detectionSSAReferencesCoverity Scan Open Source Report, 2009. <http://scan.coverity.com/report/>Coverity Scan Open Source Report, 2009. <http://scan.coverity.com/report/>Ertl M.A., Wien TU: Domination-Based Scoping and Static Single Assignment Languages. Static Single-Assignment Form Seminar, 2009.Ertl M.A., Wien TU: Domination-Based Scoping and Static Single Assignment Languages. Static Single-Assignment Form Seminar, 2009.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.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.Itsykson V., Moiseev M., Tsesko V., Zakharov A. Automatic defects detection in industrial C/C++ software. Software Engineering Conference in Russia (CEE- SECR), 2009.Itsykson V., Moiseev M., Tsesko V., Zakharov A. Automatic defects detection in industrial C/C++ software. Software Engineering Conference in Russia (CEE- SECR), 2009.Jim T., Palsberg J. Type inference in systems of recursive types with subtyping. Manuscript, 1999.Jim T., Palsberg J. Type inference in systems of recursive types with subtyping. Manuscript, 1999.Lattner C., Haberman J., Housel P. S. LLVM Bitcode File Format. <http://llvm.org/docs/BitCodeFormat.html>Lattner C., Haberman J., Housel P. S. LLVM Bitcode File Format. <http://llvm.org/docs/BitCodeFormat.html>Lattner C. LLVM Language Reference Manual. <http://llvm.org/docs/LangRef.html>Lattner C. LLVM Language Reference Manual. <http://llvm.org/docs/LangRef.html>llvm-parser - A haskell library for parsing LLVM binary bitcode files. <http://code.google.com/p/llvm-parser>llvm-parser - A haskell library for parsing LLVM binary bitcode files. <http://code.google.com/p/llvm-parser>Marino D., Millstein T. A Generic Type-and-Effect System. TLDI, 2010.Marino D., Millstein T. A Generic Type-and-Effect System. TLDI, 2010.Nielson F., Nielson H. R. Type and Effect Systems. Correct System Design, 1999. P. 114-136.Nielson F., Nielson H. R. Type and Effect Systems. Correct System Design, 1999. P. 114-136.Nielson F., Nielson H. R., Hankin C. Principles of Program Analysis. Springer- Verlag, 2005.Nielson F., Nielson H. R., Hankin C. Principles of Program Analysis. Springer- Verlag, 2005.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.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.Zadeck K. The Development of Static Single Assignment Form. Static Single- Assignment Form Seminar, 2009.Zadeck K. The Development of Static Single Assignment Form. Static Single- Assignment Form Seminar, 2009.

The authors declare that there are no conflicts of interest present.