https://chacker.pl/
Uściślijmy koncepcję wykonywania symbolicznego, korzystając z pseudokodu z Listingu.
Listing : Przykład pseudokodu ilustrujący wykonywanie symboliczne
Ten program pseudokodu pobiera dwie liczby całkowite o nazwach x i y z danych wprowadzonych przez użytkownika. Przykład omawiany w tej sekcji wykorzystuje wykonywanie symboliczne w celu znalezienia danych wprowadzonych przez użytkownika, które obejmowałyby ścieżki w kodzie prowadzące odpowiednio do funkcji foo i bar. Aby to osiągnąć, należy przedstawić wartości x i y jako wartości symboliczne, a następnie symbolicznie wykonać program, aby obliczyć ograniczenie ścieżki i wyrażenia symboliczne nałożone na wartości x i y przez operacje programu. Na koniec rozwiązuje się te formuły, aby znaleźć konkretne wartości (jeśli istnieją) dla wartości x i y, które prowadzą program do przejścia każdej ścieżki. Rysunek pokazuje, jak ewoluuje stan symboliczny dla wszystkich możliwych ścieżek w funkcji przykładowej.
Listing rozpoczyna się od odczytania x i y z danych wejściowych użytkownika (1). Jak widać na rysunku , ograniczenie ścieżki π jest początkowo ustawione na ⊤, symbol tautologii. Oznacza to, że żadne gałęzie nie zostały jeszcze wykonane, więc nie nałożono żadnych ograniczeń. Podobnie, magazyn wyrażeń symbolicznych jest początkowo zbiorem pustym. Po odczytaniu x, silnik Symbex tworzy nowe wyrażenie symboliczne φ1 = α1, które odpowiada nieograniczonej wartości symbolicznej, która może reprezentować dowolną konkretną wartość, i odwzorowuje x na to wyrażenie. Odczyt y powoduje analogiczny efekt, odwzorowując y na φ2 = α2. Następnie, operacja z = x + y (2) powoduje, że silnik Symbex odwzorowuje z na nowe wyrażenie symboliczne, φ3 = φ1 + φ2. Załóżmy, że silnik wykonania symbolicznego najpierw bada prawdziwą gałąź warunku if(x >= 5) (3). Aby to zrobić, silnik dodaje ograniczenie rozgałęzienia φ1 ≥ 5 do π i kontynuuje symboliczne wykonywanie w miejscu docelowym rozgałęzienia, którym jest wywołanie funkcji foo. Przypomnijmy, że celem było znalezienie konkretnych danych wejściowych użytkownika, które prowadzą do funkcji foo lub bar. Ponieważ dotarliśmy do wywołania funkcji foo, możemy rozwiązać wyrażenia i ograniczenia rozgałęzienia, aby znaleźć konkretne wartości dla x i y, które prowadzą do tego wywołania funkcji foo. Na tym etapie wykonywania x i y są mapowane na wyrażenia symboliczne φ1 = α1 i φ2 = α2, odpowiednio, a α1 i α2 są jedynymi wartościami symbolicznymi. Co więcej, masz tylko jedno ograniczenie gałęzi: φ1 ≥ 5. Zatem jednym z możliwych rozwiązań prowadzących do tego wywołania foo jest α1 = 5 ∧ α2 = 0. Oznacza to, że jeśli uruchomisz program normalnie (konkretne wykonanie) z danymi wejściowymi użytkownika x = 5 i y = 0, dojdziesz do wywołania foo. Zauważ, że α2 może przyjmować dowolną wartość, ponieważ nie występuje w żadnym z wyrażeń symbolicznych pojawiających się w ograniczeniu ścieżki. Rozwiązanie takie jak to, które właśnie zobaczyłeś, nazywa się modelem. Zwykle modele oblicza się automatycznie za pomocą specjalnego programu zwanego rozwiązywaczem ograniczeń, który jest w stanie rozwiązywać problemy dla wartości symbolicznych w taki sposób, że wszystkie ograniczenia i wyrażenia symboliczne są spełnione, jak wkrótce poznasz w rozdziale 12.2. Załóżmy teraz, że chcesz dowiedzieć się, jak zamiast tego dotrzeć do wywołania bar. Aby to zrobić, musisz uniknąć gałęzi if(x >= 5) i zamiast tego wziąć gałąź else (4). Zmieniasz więc stare ograniczenie ścieżki φ1 ≥ 5 na φ1 < 5 i prosisz solver o nowy model. W tym przypadku możliwym modelem byłby α1 = 4 ∧ α2 = 0. W niektórych przypadkach solver może również zgłosić brak rozwiązania, co oznacza, że ścieżka jest nieosiągalna. Ogólnie rzecz biorąc, nie jest możliwe pokrycie wszystkich ścieżek za pomocą nietrywialnego programu, ponieważ liczba możliwych ścieżek rośnie wykładniczo wraz z liczbą rozgałęzień. Dowiesz się, jak używać heurystyk do decydowania, które ścieżki eksplorować. Jak wspomniałem, istnieje kilka wariantów wykonywania symbolicznego, z których niektóre działają nieco inaczej niż w przykładzie, który właśnie omówiłem. Przyjrzyjmy się tym innym wariantom wykonywania symbolicznego i zbadajmy ich wady i zalety.
