Krótkie przykłady implementacji interpretacji abstrakcyjnej

Question

Biorę udział w kursie interpretacji abstrakcyjnej, ale nie widziałem przykładów, w jaki sposób teoria mapuje się do rzeczywistego kodu.

Szukam krótkich przykładów kodu, w których nie będę musiał pracować z całym kompilatorem. Analiza nie musi być przydatna, chciałbym tylko zobaczyć przykład, w którym analiza jest wyprowadzana, a następnie wdrażana.

Czy ktoś wie o takich przykładach, być może z kursu uniwersyteckiego?

Answer 1

Istnieje MonoREIL, który pochodzi z niedawno otwartego narzędzia źródłowego BinNavi.

Zobacz here jest krótkim wprowadzeniem.

Należy zauważyć, że kontekstem struktury MonoREIL nie jest kompilacja, ale analiza kodu binarnego. Jednak został on użyty w aplikacjach świata rzeczywistego, patrz slajd 34 ff z this wstęp (zawierający bardziej formalne tło).

Answer 2

Jest to papier o Bertot

Structural abstract interpretation, A formal study using Coq

To daje pełną realizację abstrakcyjnego tłumacza dla prostego języka zabawki przy użyciu Coq Proof Assistant. Użyłem tego dla konkretnego odniesienia, i uznałem, że jest użyteczny, choć trochę trudny, czego należy się spodziewać, biorąc pod uwagę temat. Coq to świetny mały program.

Ja również natrafiłem na papierze Cousot:

A gentle introduction to formal verification of computer systems by abstract interpretation

szorstki Szczegóły (ale jestem pewien, że będzie użyteczne cytaty dla pełnych szczegółów) z implementacji w Astrée, nie jestem zaznajomiony z Astrée , więc tak naprawdę nie czytałem tej sekcji, ale myślę, że spełnia ona twoje kryteria.

Jeśli już spotkasz się, daj mi znać! Szczególnie chciałbym zobaczyć tłumacza abstrakcji prologu.

Answer 3

AI jest oparty na matematycznej nazwie teorii Galois Połączenie. Teoria jest bardzo prosta:

1. Streszczenie zachowania programu.
2. Przeprowadź analizę na poziomie abstrakcyjnym.

Galois connection: Aby powiązać program Actual i Abstract.

This jest najlepszy poradnik widziałem do tej pory o Streszczenie Interpretacja:

Answer 4

Może to narzędzie jest również interesujące dla Ciebie: Interproc Analyzer

Jest to abstrakcyjny analizator na bardzo prostym językiem, co jednak oferuje analizy interprocedyczne . Możesz wypróbować analizę i uzyskać niezmienniki numeryczne dotyczące analizowanego programu. Kod źródłowy jest dostępny (OCaml).

Bardzo dokładny i precyzyjny kurs, nadany przez jednego z "twórców" interpretacji abstrakcyjnej Patricka Cousota (wspomniana już w jednej z odpowiedzi): MIT course about Abstract Interpretation. Kurs oferuje również zadania w OCaml.