Interpretacja abstrakcyjna - Abstract interpretation

W informatyce , streszczenie interpretacja jest teorią dźwięku zbliżenia z semantyki programów komputerowych , na podstawie monotonicznych funkcji ponad zamawianych zestawów , zwłaszcza kraty . To może być postrzegane jako częściowe wykonanie z programem komputerowym , który posiada informację o jej semantyki (np kontrola przepływu , przepływie danych ) bez wykonywania wszystkich obliczeń .

Jego głównym konkretnym zastosowaniem jest formalna analiza statyczna , automatyczne wyodrębnianie informacji o możliwych wykonaniach programów komputerowych; takie analizy mają dwa główne zastosowania:

Abstrakcyjna interpretacja została sformalizowana przez francuską parę informatyków Patricka Cousota i Radhię Cousot pod koniec lat 70. XX wieku.

Intuicja

Ta sekcja ilustruje abstrakcyjną interpretację za pomocą rzeczywistych, nieobliczeniowych przykładów.

Pomyśl o ludziach w sali konferencyjnej. Przyjmij unikalny identyfikator dla każdej osoby w pokoju, np. numer ubezpieczenia społecznego w Stanach Zjednoczonych. Aby udowodnić, że kogoś nie ma, wystarczy sprawdzić, czy jego numeru ubezpieczenia społecznego nie ma na liście. Ponieważ dwie różne osoby nie mogą mieć tego samego numeru, możliwe jest udowodnienie lub obalenie obecności uczestnika, po prostu sprawdzając jego numer.

Możliwe jednak, że zarejestrowane zostały tylko nazwiska uczestników. Jeśli nazwisko osoby nie znajduje się na liście, możemy bezpiecznie wywnioskować, że ta osoba nie była obecna; ale jeśli tak, nie możemy ostatecznie zakończyć bez dalszych dociekań, ze względu na możliwość homonimów (na przykład dwie osoby o nazwisku John Smith). Należy pamiętać, że ta nieprecyzyjna informacja będzie nadal wystarczająca dla większości celów, ponieważ homonimy są rzadkością w praktyce. Jednak ze wszystkimi rygorami nie możemy powiedzieć z całą pewnością, że ktoś był w pokoju; wszystko, co możemy powiedzieć, to to, że prawdopodobnie był tutaj. Jeśli osoba, na którą patrzymy, jest przestępcą, uruchomimy alarm ; ale jest oczywiście możliwość wystawienia fałszywego alarmu . Podobne zjawiska wystąpią w analizie programów.

Jeśli interesuje nas tylko konkretna informacja, powiedzmy „czy w pokoju była osoba w wieku n ?”, prowadzenie spisu wszystkich nazwisk i dat urodzenia jest zbędne. Możemy bezpiecznie i bez utraty precyzji ograniczyć się do prowadzenia listy wiekowej uczestników. Jeśli to już za dużo, możemy zachować tylko wiek najmłodszej, mi najstarszej osoby, M . Jeśli pytanie dotyczy wieku ściśle niższego niż m lub ściśle wyższego niż M , możemy śmiało odpowiedzieć, że taki uczestnik nie był obecny. W przeciwnym razie możemy tylko powiedzieć, że nie wiemy.

W przypadku obliczeń, konkretna, dokładna informacja jest generalnie nieobliczalna w skończonym czasie i pamięci (patrz twierdzenie Rice'a i problem zatrzymania ). Abstrakcja jest używana, aby umożliwić uogólnione odpowiedzi na pytania (na przykład odpowiedź „być może” na pytanie tak/nie, co oznacza „tak lub nie”, gdy my (algorytm interpretacji abstrakcyjnej) nie możemy obliczyć dokładnej odpowiedzi z pewnością); upraszcza to problemy, czyniąc je podatnymi na automatyczne rozwiązania. Jednym z kluczowych wymagań jest dodanie wystarczającej niejasności, aby problemy można było rozwiązać, zachowując jednocześnie wystarczającą precyzję odpowiedzi na ważne pytania (takie jak „czy program może się zawiesić?”).

Abstrakcyjna interpretacja programów komputerowych

Biorąc pod uwagę język programowania lub specyfikacji, abstrakcyjna interpretacja polega na podaniu kilku semantyk połączonych relacjami abstrakcji. Semantyka to matematyczna charakterystyka możliwego zachowania programu. Najdokładniejszą semantykę, opisującą bardzo dokładnie faktyczne wykonanie programu, nazywamy semantyką konkretną . Na przykład konkretna semantyka imperatywnego języka programowania może skojarzyć z każdym programem zbiór śladów wykonania, które może wytworzyć – ślad wykonania będący sekwencją możliwych kolejnych stanów wykonania programu; stan zazwyczaj składa się z wartości licznika programu i lokalizacji w pamięci (globalnych, stosu i sterty). Następnie wyprowadzana jest bardziej abstrakcyjna semantyka; na przykład w wykonaniach można brać pod uwagę tylko zbiór stanów osiągalnych (co sprowadza się do uwzględniania ostatnich stanów w skończonych śladach).

Celem analizy statycznej jest uzyskanie w pewnym momencie obliczalnej interpretacji semantycznej. Na przykład, można wybrać reprezentację stanu programu manipulującego zmiennymi całkowitymi, zapominając o rzeczywistych wartościach zmiennych i zachowując tylko ich znaki (+, − lub 0). W przypadku niektórych operacji elementarnych, takich jak mnożenie , taka abstrakcja nie traci żadnej precyzji: aby uzyskać znak iloczynu, wystarczy znać znak operandów. W przypadku niektórych innych operacji abstrakcja może stracić precyzję: na przykład niemożliwe jest poznanie znaku sumy, której argumenty są odpowiednio dodatnie i ujemne.

Czasami utrata precyzji jest konieczna, aby semantyka była rozstrzygalna (patrz twierdzenie Rice'a i problem zatrzymania ). Ogólnie rzecz biorąc, istnieje kompromis między precyzją analizy a jej rozstrzygalnością ( obliczalność ) lub wykonalnością ( koszt obliczeniowy ).

W praktyce zdefiniowane abstrakcje są dostosowane zarówno do właściwości programu, które chcemy analizować, jak i do zestawu programów docelowych. Pierwsza zautomatyzowana analiza programów komputerowych na dużą skalę z interpretacją abstrakcyjną była motywowana wypadkiem, który doprowadził do zniszczenia pierwszego lotu rakiety Ariane 5 w 1996 roku.

Formalizowanie

Przykład: abstrakcja zestawów liczb całkowitych (czerwony) do zestawów znaków (zielony)

Niech L będzie zbiorem uporządkowanym, zwanym zbiorem konkretnym i niech L ′ będzie innym zbiorem uporządkowanym, zwanym zbiorem abstrakcyjnym . Te dwa zestawy są ze sobą powiązane, definiując wszystkie funkcje, które odwzorowują elementy od jednego do drugiego.

Funkcja α nazywana jest funkcją abstrakcji, jeśli odwzorowuje element x ze zbioru konkretnego L na element α( x ) ze zbioru abstrakcyjnego L ′. Oznacza to, że elementem α ( x ) w L "jest abstrakcją od X w L .

Funkcja γ nazywana jest funkcją konkretyzacyjną, jeśli odwzorowuje element x ′ w zbiorze abstrakcyjnym L ′ na element γ( x ′) w zbiorze konkretnym L . Oznacza to, że elementem γ ( x '), w L jest konkretyzacja z X ' w l '.

Niech L 1 , L 2 , L ′ 1 i L ′ 2 będą zbiorami uporządkowanymi. Konkretna semantyka f jest funkcją monotoniczną od L 1 do L 2 . Funkcja F "z L " 1 do l ' 2 mówi się być ważne poboru z F , jeżeli dla wszystkich x ' w l ' 1 ( f ∘ γ) ( x ") ≤ (γ ∘ f ') ( x " ).

Semantyka programu jest ogólnie opisana za pomocą stałych punktów w obecności pętli lub procedur rekurencyjnych. Załóżmy, że L jest pełną siecią i niech f będzie funkcją monotoniczną od L do L . Wtedy każdy x ′ taki, że f ( x ′) ≤ x ′ jest abstrakcją najmniej ustalonego punktu f , który istnieje zgodnie z twierdzeniem Knastera-Tarskiego .

Trudność polega teraz na uzyskaniu takiego x ′. Jeżeli L ′ ma skończoną wysokość lub przynajmniej weryfikuje warunek łańcucha rosnącego (wszystkie ciągi rosnące są ostatecznie stacjonarne), to taki x ′ można otrzymać jako granicę stacjonarności ciągu rosnącego x ′ n zdefiniowaną przez indukcję w następujący sposób: x ′ 0 =⊥ (najmniejszy element L ′) i x ′ n +1 = f ′( x ′ n ).

W innych przypadkach nadal możliwe jest otrzymanie takiego x ′ poprzez operator rozszerzający ∇ : dla wszystkich x i y , x ∇ y powinno być większe lub równe zarówno x i y , a dla dowolnego ciągu y ′ n , ciąg zdefiniowana przez x ′ 0 =⊥ i x ′ n +1 = x ′ n ∇ y ′ n jest ostatecznie stacjonarna. Możemy wtedy przyjąć y ′ n = f ′( x ′ n ).

W niektórych przypadkach możliwe jest zdefiniowanie abstrakcji za pomocą połączeń Galois (α, γ) gdzie α jest od L do L ′ a γ od L ′ do L . Zakłada to istnienie najlepszych abstrakcji, co niekoniecznie musi mieć miejsce. Na przykład, jeśli abstrahujemy zbiory par ( x , y ) liczb rzeczywistych przez objęcie wielościanów wypukłych , nie ma optymalnej abstrakcji do dysku zdefiniowanego przez x 2 + y 2 ≤ 1.

Przykłady domen abstrakcyjnych

Każdej zmiennej x dostępnej w danym punkcie programu można przypisać odstęp [ L x , H x ]. Stan przypisujący wartość v ( x ) zmiennej x będzie konkretyzacją tych przedziałów, jeśli dla wszystkich x , v ( x ) jest w [ L x , H x ]. Z przedziałów [ L x , H x ] i [ L y , H y ] dla zmiennych x i y można łatwo uzyskać przedziały dla x + y ([ L x + L y , H x + H y ]) oraz dla x - y ([ L x - H y , H x - L y ]); zauważ, że są to dokładne abstrakcje, ponieważ zbiór możliwych wyników dla, powiedzmy, x + y , jest dokładnie przedziałem ([ L x + L y , H x + H y ]). Bardziej złożone wzory można wyprowadzić na mnożenie, dzielenie itp., dając tzw. arytmetykę przedziałową .

Rozważmy teraz następujący bardzo prosty program: 

y = x;
z = x - y;
Kombinacja arytmetyki przedziałowej ( zielony ) i kongruencji mod 2 na liczbach całkowitych ( cyjan ) jako domen abstrakcyjnych do analizy prostego fragmentu kodu C ( czerwony : konkretne zestawy możliwych wartości w czasie wykonywania). Używając informacji o zgodności ( 0 = parzyste, 1 = nieparzyste), można wykluczyć dzielenie przez zero . (Ponieważ w grę wchodzi tylko jedna zmienna, domeny relacyjne i nierelacyjne nie stanowią tutaj problemu).
Trójwymiarowy wypukły przykład wielościanu opisujący możliwe wartości 3 zmiennych w pewnym punkcie programu. Każda ze zmiennych może wynosić zero, ale wszystkie trzy nie mogą być zerem jednocześnie. Ta ostatnia właściwość nie może być opisana w dziedzinie arytmetyki przedziałowej.

Przy rozsądnych typach arytmetycznych wynik dla zpowinna wynosić zero. Ale jeśli robimy arytmetykę przedziałową, zaczynając odx w [0, 1] otrzymuje się zw [-1, +1]. O ile każda z operacji branych z osobna była dokładnie wyabstrahowana, o tyle ich skład nie.

Problem jest oczywisty: nie śledziliśmy relacji równości między x oraz tak; w rzeczywistości ta dziedzina przedziałów nie uwzględnia żadnych relacji między zmiennymi, a zatem jest dziedziną nierelacyjną . Domeny nierelacyjne są zazwyczaj szybkie i proste w implementacji, ale nieprecyzyjne.

Oto kilka przykładów relacyjnych liczbowych domen abstrakcyjnych:

  • relacje kongruencji na liczbach całkowitych
  • wielościany wypukłe (por. lewy rysunek) – z pewnymi wysokimi kosztami obliczeniowymi
  • macierze różniczkowe
  • „ośmiokąty”
  • liniowe równości

i ich kombinacje (takie jak zredukowany produkt, por. prawy rysunek).

Wybierając domenę abstrakcyjną, zazwyczaj trzeba zachować równowagę między utrzymywaniem precyzyjnych relacji a wysokimi kosztami obliczeniowymi.

Zobacz też

Bibliografia

Linki zewnętrzne

Notatki do wykładów