Modeling of library functions in an industrial static code analyzer
https://doi.org/10.15514/ISPRAS-2020-32(3)-2
Abstract
SharpChecker is an industrial level static analyzer, which is aimed at detection of various bugs in C# source code. Because the tool is actively developed, it requires more and more precise information about program environment, especially about results and side-effects of library functions. The paper is devoted to the evolution of models for the standard library historically used by SharpChecker, its advantages and drawbacks. We have started from SQLite database with the most important functions properties, then introduced manually written C# model implementations of frequently used methods to add support of data container states and have recently developed a model, built by a preliminary analysis of library source code, which allows to gather all significant side-effects with conditions for almost whole C# library.
About the Authors
Mikchail Vladimirovitch BELYAEV
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Intern Researcher
Russian Federation
Intern Researcher
Egor Sergeevitch ROMANENKOV
Lomonosov Moscow State University
Russian Federation
Master student of the CMC faculty
Russian Federation
Master student of the CMC faculty
Valery Nikolaevitch IGNATYEV
Ivannikov Institute for System Programming of the Russian Academy of Sciences,
Lomonosov Moscow State University
Russian Federation
Candidate of Physical and Mathematical Sciences, Senior Researcher, ISP RAS, Senior Lecturer, Faculty of VMK MSU
Russian Federation
Candidate of Physical and Mathematical Sciences, Senior Researcher, ISP RAS, Senior Lecturer, Faculty of VMK MSU
References
1. V. K. Koshelev, V. N. Ignatiev, A. I. Borzilov, and A. A. Belevantsev. SharpChecker: Static analysis tool for C# programs. Programming and Computer Software, vol. 43, issue 4, 2017, pp. 268-276.
2. V. P. Ivannikov, A. A. Belevantsev, A. E. Borodin, V. N. Ignatiev, D. M. Zhurikhin, and A. I. Avetisyan. Static analyzer Svace for finding defects in a source program code. Programming and Computer Software, vol. 40, issue 5, 2014, pp. 265-275.
3. A. Belevantsev, A. Borodin, I. Dudina, V. Ignatiev, A. Izbyshev, S. Polyakov, E. Velesevich, and D. Zhurikhin. Design and development of Svace static analyzers. In Proc. of the 2018 Ivannikov Memorial Workshop (IVMEM), 2018, pp. 3-9.
4. Koshelev V., Dudina I., Ignatyev V., Borzilov A. 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 / Кошелев В.К., Дудина И.А., Игнатьев В.Н., Борзилов А.И. Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 59-86
5. M.V. Belyaev, N.V. Shimchik, V.N. Ignatyev, and A.A. Belevantsev. Comparative analysis of two approaches to static taint analysis. Programming and Computer Software, vol. 44, issue 6, 2018, pp. 459-466.
6. G. Morgachev, V. Ignatyev, and A. Belevantsev. Detection of variable misuse using static analysis combined with machine learning. In Proc. of the 2019 Ivannikov ISP RAS Open Conference (ISPRAS), 2019, pp. 16-24.
7. .NET Framework API Reference. Available at: https://docs.microsoft.com/en-us/dotnet/api/?view=netframework-4.5. Accessed: Apr. 10, 2020.
8. E. Meijer, B. Beckman, and G. Bierman. LINQ: Reconciling object, relations and XML in the .NET Framework. In Proc. of the 2006 ACM SIGMOD International Conference on Management of Data, 2006, p. 706.
9. Source code implementation for string.IsNullOrEmpty(). Available at: https://github.com/dotnet/coreclr/blob/1f3f474a13bdde1c5fecdf8cd9ce525dbe5df000/src/System.Private.CoreLib/shared/System/String.cs#L439-L448. Accessed: Apr. 10, 2020.
10. Source Link – a language- and source-control system for providing source debugging experiences for binaries. Available at: https://github.com/dotnet/sourcelink/blob/master/README.md. Accessed: Apr. 10, 2020.
11. Features – ReSharper. Available at: https://www.jetbrains.com/resharper/features/. Accessed: May 18, 2020.
12. Features – Rider. Available at: https://www.jetbrains.com/rider/features/. Accessed: May 18, 2020.
13. External Annotations – Help ReSharper. Available at: https://www.jetbrains.com/help/resharper/Code_Analysis__External_Annotations.html. Accessed: May 18, 2020.
14. Coverity Static Analysis. Available at: https://www.synopsys.com/content/dam/synopsys/sig-assets/datasheets/SAST-Coverity-datasheet.pdf. Accessed: May 18, 2020.
15. Coverity 2018.09 Command Reference. Available at: https://www.academia.edu/38375284/Cov command ref. Accessed: May 18, 2020.
16. C# Reserved attributes: Nullable static analysis. Available at: https://docs.microsoft.com/en-us/dotnet/csharp/language-reference/attributes/nullable-analysis, Accessed: May 18, 2020.
17. CIL – Common Intermediate Language. Available at: https://en.wikipedia.org/wiki/Common Intermediate Language. Accessed: Apr. 10, 2020.
18. V. K. Koshelev, V. N. Ignatiev, A. I. Borzilov, and A. A. Belevantsev. SharpChecker: Static analysis tool for C# programs. Programming and Computer Software, vol. 43, issue 4, 2017, pp. 268-276.
19. V. P. Ivannikov, A. A. Belevantsev, A. E. Borodin, V. N. Ignatiev, D. M. Zhurikhin, and A. I. Avetisyan. Static analyzer Svace for finding defects in a source program code. Programming and Computer Software, vol. 40, issue 5, 2014, pp. 265-275.
20. A. Belevantsev, A. Borodin, I. Dudina, V. Ignatiev, A. Izbyshev, S. Polyakov, E. Velesevich, and D. Zhurikhin. Design and development of Svace static analyzers. In Proc. of the 2018 Ivannikov Memorial Workshop (IVMEM), 2018, pp. 3-9.
21. Koshelev V., Dudina I., Ignatyev V., Borzilov A. 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 / Кошелев В.К., Дудина И.А., Игнатьев В.Н., Борзилов А.И. Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 59-86
22. M.V. Belyaev, N.V. Shimchik, V.N. Ignatyev, and A.A. Belevantsev. Comparative analysis of two approaches to static taint analysis. Programming and Computer Software, vol. 44, issue 6, 2018, pp. 459-466.
23. G. Morgachev, V. Ignatyev, and A. Belevantsev. Detection of variable misuse using static analysis combined with machine learning. In Proc. of the 2019 Ivannikov ISP RAS Open Conference (ISPRAS), 2019, pp. 16-24.
24. .NET Framework API Reference. Available at: https://docs.microsoft.com/en-us/dotnet/api/?view=netframework-4.5. Accessed: Apr. 10, 2020.
25. E. Meijer, B. Beckman, and G. Bierman. LINQ: Reconciling object, relations and XML in the .NET Framework. In Proc. of the 2006 ACM SIGMOD International Conference on Management of Data, 2006, p. 706.
26. Source code implementation for string.IsNullOrEmpty(). Available at: https://github.com/dotnet/coreclr/blob/1f3f474a13bdde1c5fecdf8cd9ce525dbe5df000/src/System.Private.CoreLib/shared/System/String.cs#L439-L448. Accessed: Apr. 10, 2020.
27. Source Link – a language- and source-control system for providing source debugging experiences for binaries. Available at: https://github.com/dotnet/sourcelink/blob/master/README.md. Accessed: Apr. 10, 2020.
28. Features – ReSharper. Available at: https://www.jetbrains.com/resharper/features/. Accessed: May 18, 2020.
29. Features – Rider. Available at: https://www.jetbrains.com/rider/features/. Accessed: May 18, 2020.
30. External Annotations – Help ReSharper. Available at: https://www.jetbrains.com/help/resharper/Code_Analysis__External_Annotations.html. Accessed: May 18, 2020.
31. Coverity Static Analysis. Available at: https://www.synopsys.com/content/dam/synopsys/sig-assets/datasheets/SAST-Coverity-datasheet.pdf. Accessed: May 18, 2020.
32. Coverity 2018.09 Command Reference. Available at: https://www.academia.edu/38375284/Cov command ref. Accessed: May 18, 2020.
33. C# Reserved attributes: Nullable static analysis. Available at: https://docs.microsoft.com/en-us/dotnet/csharp/language-reference/attributes/nullable-analysis, Accessed: May 18, 2020.
34. CIL – Common Intermediate Language. Available at: https://en.wikipedia.org/wiki/Common Intermediate Language. Accessed: Apr. 10, 2020.
Review
For citations:
BELYAEV M.V., ROMANENKOV E.S., IGNATYEV V.N. Modeling of library functions in an industrial static code analyzer. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(3):21-31. https://doi.org/10.15514/ISPRAS-2020-32(3)-2
Email this article 