Preview

Труды Института системного программирования РАН

Расширенный поиск

Внутрипроцедурный анализ для поиска ошибок на основе символьного выполнения

https://doi.org/10.15514/ISPRAS-2020-32(6)-7

Аннотация

В работе описывается внутрипроцедурный анализ отдельных функций, использующийся в инструменте статического поиска ошибок Svace. Отличительные особенности анализа: анализ по графу потока управления, символьное выполнение с объединением состояний анализа в точках слияния путей, анализ только части путей в функциях с циклами, одновременный запуск всех анализаторов, моделирование достижимых ячеек памяти, нумерация значений переменных.

Об авторах

Алексей Евгеньевич БОРОДИН
Институт системного программирования им. В.П. Иванникова РАН
Россия
Кандидат физико-математических наук, научный сотрудник


Ирина Александровна ДУДИНА
Институт системного программирования им. В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова
Россия
Кандидат физико-математических наук, сотрудник ИСП РАН и ассистент кафедры системного программирования факультета ВМК МГУ


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

1. В.П. Иванников, А.А. Белеванцев, А.Е. Бородин, В.Н. Игнатьев, Д.М. Журихин, А.И. Аветисян, М.И. Леонов. Статический анализатор Svace для поиска дефектов в исходном коде программ. Труды ИСП РАН, том 26, вып. 1, 2014 г., стр. 231-250 / V.P. Ivannikov, A.A. Belevantsev, A.E. Borodin, V.N. Ignatyev, D.M. Zhurikhin, A.I. Avetisyan, M.I. Leonov. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 231-250 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-7.

2. A. Borodin, A. Belevantsev, D. Zhurikhin, and A. Izbyshev. Deterministic static analysis. In Proc. of the 2018 Ivannikov Memorial Workshop, 2018, pp. 10-14. DOI: 10.1109/IVMEM.2018.00009.

3. Clang. URL: https://clang.llvm.org, accessed September 10, 2020.

4. The javac compiler. URL: https: //docs.oracle.com/en/java/javase/11/tools/javac.html, accessed September 10, 2020.

5. LLVM bitcode. URL: https: //releases.llvm.org/8.0.1/docs/BitCodeFormat.html, accessed September 10, 2020.

6. J. C. King. Symbolic execution and program testing. Communications of the ACM, vol. 19, no. 7, 1976, pp. 385-394.

7. А.Е. Бородин и А.А. Белеванцев. Статический анализатор Svace как коллекция анализаторов разных уровней сложности. Труды ИСП РАН, том 27, вып. 2, 2015 г., стр. 111-134 / A.E. Borodin, A.A. Belevancev. A Static Analysis Tool Svace as a Collection of Analyzers with Various Complexity Levels. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 6, 2015, pp.111-134 (in Russian). DOI: 10.15514/ISPRAS-2015-27(6)-8.

8. Р.Р. Мулюков, А.Е. Бородин. Использование анализа недостижимого кода в статическом анализаторе для поиска ошибок в исходном коде программ. Труды ИСП РАН, том 28, вып. 5, 2016 г., стр. 145-158 / R.R. Mulyukov, A.E. Borodin. Using unreachable code analysis in static analysis tool for finding defects in source code. Trudy ISP RAN/Proc. ISP RAS, 2016, vol. 28, issue 5, 2016, pp. 145-158 (in Russian). DOI: 10.15514/ISPRAS-2016-28(5)-9.

9. W.R. Bush, J.D. Pincus, and D.J. Sielaff. A static analyzer for finding dynamic programming errors. Software-Practice and Experience, vol. 30, no. 7, 2000, pp. 775-802.

10. Y. Xie, A. Chou, and D. Engler. Archer: using symbolic, path-sensitive analysis to detect memory access errors. ACM SIGSOFT Software Engineering Notes, vol. 28, no. 5, 2003, pp. 327–336.

11. A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Communications of the ACM, vol. 53, no. 2, 2010, pp. 66–75.

12. A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, and P. Hawkins. An overview of the saturn project. In Proc of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2007, pp. 43–48. ACM.

13. D. Babic and A.J. Hu. Calysto: scalable and precise extended static checking. In Proc. of the 30th International Conference on Software Engineering, 2008, pp. 211–220.

14. В.К. Кошелев, И.А. Дудина, В.Н. Игнатьев, А.И. Борзилов. Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 59-86 / V.K. Koshelev, I.A. Dudina, V.N. Ignatyev, A.I. Borzilov. Path-Sensitive Bug Detection Analysis of C# Program Illustrated by Null Pointer Dereference. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 5, 2015, pp.59-86 (in Russian). DOI: 10.15514/ISPRAS-2015-27(5)-5.

15. V. Koshelev, V. Ignatiev, A. Borzilov, and A. Belevantsev. Sharpchecker: static analysis tool for C# programs. Programming and Computer Software, vol. 43, no. 4, 2017, pp. 268–276. DOI: 10.1134/S0361768817040041.


Рецензия

Для цитирования:


БОРОДИН А.Е., ДУДИНА И.А. Внутрипроцедурный анализ для поиска ошибок на основе символьного выполнения. Труды Института системного программирования РАН. 2020;32(6):87-100. https://doi.org/10.15514/ISPRAS-2020-32(6)-7

For citation:


BORODIN A.E., DUDINA I.A. Symbolic Execution Based Intra-Procedural Analysis for Search for Defects. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(6):87-100. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(6)-7



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


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)