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.
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.
