Original title:
Linter pro C++ využívající lineární typy
Translated title:
C++ linter based on linear types
Authors:
Beneš, Jiří ; Kratochvíl, Miroslav (advisor) ; Šefl, Vít (referee) Document type: Bachelor's theses
Year:
2020
Language:
eng Abstract:
[eng][cze] Low-level programming requires careful management of system resources, most notably memory. In C++ programmers are encouraged to follow idioms like RAII and smart pointers to handle resources correctly as violating them leads to unsafe code. Typed functional programming languages guarantee safe automatic mem- ory management, but are often sub-optimal in handling system resources. A nice, formal solution to handling resources naturally is linear types. Unfortu- nately, existing languages that support linearity are cumbersome and require explicit, complicated annotations from the programmer. We bridge the two worlds by exploring a novel combination of C++ and linear types. We describe a new type system with linearity for C++ by using constrained qualified types, while requiring no additional input from the programmer. The applied result of our work is called Lily, a static analysis tool for C++ using the Clang compiler infrastructure. Lily can statically detect large, general classes of issues, some of which are not detected by common state-of-the-art tools for C++. 1Nízkoúrovňové programování vyžaduje opatrnou práci se systémovými zdroji, hlavně s pamětí. Programátoři v C++ používají ustálené zásady jako RAII a chytré ukazatele ke korektní práci se zdroji. Porušení podobných zásad vede často k nebezpečnému kódu. Funkcionální programovací jazyky s typy garantují bezpečnou a automat- ickou správu paměti, ale jejich práce se systémovými zdroji je často subop- timální. Hezký, formální prostředek k práci se zdroji jsou lineární typy. Bo- hužel, existující jazyky podporující linearitu jsou složité a vyžadují explicitní anotace od programátora. Prozkoumáváme propojení těchto světů pomocí kombinace C++ a lineárních typů. V práci popisujeme nový typový systém s linearitou pro C++ použitím omezených kvalifikovaných typů, bez požadavku na součinnost programá- tora. Aplikovaný výsledek naší práce je Lily, nástroj pro statickou analýzu C++ používající infrastrukturu překladače Clang. Lily umí staticky deteko- vat velké, obecné třídy problémů, z nichž některé nejsou detekované jinými běžně používanými nástroji pro C++. 1
Keywords:
C++; linear types; static analysis; type systems; C++; lineární typy; statická analýza; typové systémy
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/120939