C++ linter based on linear types
|Thesis title in Czech:||Linter pro C++ využívající lineární typy|
|Thesis title in English:||C++ linter based on linear types|
|Key words:||typové systémy, lineární typy, C++, statická analýza|
|English key words:||type systems, linear types, C++, static analysis|
|Academic year of topic announcement:||2017/2018|
|Type of assignment:||Bachelor's thesis|
|Department:||Department of Software Engineering (32-KSI)|
|Supervisor:||Mgr. Miroslav Kratochvíl|
|Author:||hidden - assigned by the advisor|
|Date of registration:||24.09.2018|
|Date of assignment:||24.09.2018|
|C++ allows to represent and pass data around in many different forms -- as values, references, pointers, smart pointers, in containers, etc., all of that constant, non-constant or constexpr on various levels. Programmer choice of the data representation is often sub-optimal: constant-data are often represented as non-constant, and many opportunities to pass data efficiently as references are missed. Such code may inhibit the optimization possibilities of the compiler, which is in turn forced to produce sub-optimal programs.
The thesis aims to develop a static analysis algorithm that uses a linear type system to discover and report such inefficiencies. The resulting program will re-use the infrastructure of the Clang compiler to parse the source code, extract the information required for the analysis, process it using a customized type system, and output the suggested code corrections in a linter-like report.
|Lattner, C. (2008, May). LLVM and Clang: Next generation compiler technology. In The BSD conference (pp. 1-2).
Girard, J. Y. (1987). Linear logic. Theoretical computer science, 50(1), 1-101.
Wadler, P. (1990, April). Linear types can change the world. In IFIP TC (Vol. 2, pp. 347-359).
Nielson, F., Nielson, H. R., & Hankin, C. (2015). Principles of program analysis. Springer.
Jones, M. P. (1999, September). Typing haskell in haskell. In Haskell workshop (Vol. 7).