Abstract Analysis of Numerical and Container Variables

Niniejsza rozprawa poświęcona jest nowym technikom statycznej analizy programów, z wykorzystaniem abstrakcyjnej interpretacji. W pierwszej części rozprawy, skupiamy się na numerycznych dziedzinach abstrakcyjnych, które służą do automatycznego wykrywania zależności między zmiennymi numerycznymi. Przedstawiamy dwie nowe dziedziny abstrakcyjne ważonych sześciokątów i ścisłych ważonych sześciokątów, służące do wykrywania powiązań postaci x <= ay oraz x < ay, gdzie x oraz y oznaczają zmienne w programie, a a jest pewną nieujemną stałą. Dziedziny te plasują się pomiędzy dziedziną pięciokątów i dziedziną TVPI, zarówno pod względem siły wyrazu jak i wydajności. Druga część rozprawy omawia abstrakcyjną analizę programów używających niektórych struktur danych. Istniejące techniki pozwalają jedynie na wnioskowanie na temat zawartości tablic numerycznych. My proponujemy nową technikę, która może być użyta do modelowania zawartości tablic oraz słowników zawierających elementy dowolnych typów. Elastyczność´ naszego rozwiązania została zilustrowana na przykładach analizy tablic numerycznych oraz słowników z kluczami napisowymi.

This thesis presents new techniques of static program analysis by abstract interpretation. In the first part of the thesis we focus on numerical abstract domains that can be used to automatically discover certain numerical properties of programs. We introduce two new abstract domains: the domain of weighted hexagons, and its enriched version, the domain of strict weighted hexagons. These domains capture constraints of the form x <= ay and x < ay, where x and y are program variables and a is a non-negative constant. They lie between the existing domains of pentagons and TVPI in terms of both expressiveness and efficiency. The second part of the thesis concerns analysis of programs that use containers of scalar values. Existing techniques can be used only to analyse arrays of numerical values. We propose a novel technique that can be used to reason about the content of dictionaries and arrays of arbitrary scalar types. The flexibility of our approach is illustrated on various examples, including analysis of numerical arrays and string-keyed dictionaries.