Статикалық бағдарлама талдауына қатысты әдіс-тәсілдер

Кіріспе

Бағдарламаны статикалық талдауға қатысты ұсыныс. Компьютерлік ғылымда абстрактілі интерпретация – компьютерлік бағдарламалардың семантикасын шамалаудың дұрыс теориясы, ол реттелген жиынтарға, әсіресе торларға қатысты монотонды функцияларға негізделген. Оны компьютерлік бағдарламаның ішінара орындалуы ретінде қарастыруға болады, ол барлық есептеулерді орындамай-ақ оның семантикасы туралы ақпаратты (мысалы, басқару ағыны, дерек ағыны) алуға мүмкіндік береді. Оның негізгі қолданылуы – формалды статикалық талдау, компьютерлік бағдарламалардың мүмкін болатын орындалуы туралы ақпаратты автоматты түрде алу; мұндай талдаулардың екі негізгі мақсаты бар: компиляторлар ішінде, бағдарламаларды талдау арқылы белгілі бір оңтайландырулар немесе түрлендірулердің қолданылу мүмкіндігін анықтау; қателерді жою немесе бағдарламаларды қателер кластарына қарсы сертификаттау. Абстрактілі интерпретацияны француз компьютерлік ғалымдары Патрик Кузо және Радия Кузо 1970 жылдардың соңында формалдаған.

Интуиция

Бұл бөлім нақты әлемдегі, есептеуге қатысы жоқ мысалдар арқылы абстрактілік интерпретацияны түсіндіреді. Конференц-залға жиналған адамдарды қарастырайық. Бөлмедегі әрбір адамға бірегей идентификатор тағайындаңыз, мысалы, Америка Құрама Штаттарындағы әлеуметтік қамсыздандыру нөмірі сияқты. Біреудің қатыспағанын дәлелдеу үшін, оның әлеуметтік қамсыздандыру нөмірі тізімде бар-жоғын тексеру жеткілікті. Екі адамның бірдей нөмірі болмайтындықтан, қатысушының бар-жоқтығын оның нөмірін қарап ғана анықтауға болады. Дегенмен, тізімге тек қатысушылардың аттары енгізілген болуы мүмкін. Егер тізімде адамның аты табылса, ол адамның қатыспағанын сенімді түрде айтуға болады; бірақ егер аты табылса, омонимдердің болу мүмкіндігіне байланысты (мысалы, Джон Смит есімді екі адам) қосымша тексерусіз нақты қорытынды жасау қиын. Бұл дәл емес ақпараттың көп жағдайда жеткілікті екенін ескеру қажет, себебі практикада омонимдер сирек кездеседі. Бірақ, толыққанды қатаңдықпен айтқанда, кімнің бөлмеде болғанын нақты біле алмаймыз; тек олардың болуы мүмкін екенін айта аламыз. Егер іздеп отырған адам қылмыскер болса, дабыл береміз; бірақ жалған дабыл беру қаупі де бар. Бағдарламаларды талдау кезінде де осындай жағдайлар туындауы мүмкін. Егер бізге тек белгілі бір ақпарат қызығушылық тудырса, мысалы, "бөлмеде белгілі бір жастағы адам болды ма?", барлық аттар мен туған күндерін тізімдеудің қажеті жоқ. Қатысушылардың жастарын тізімдеу арқылы қауіпсіз және дәлдікті жоғалтпай шектеу қоюға болады. Егер бұл мәселе тым қиын болса, ең жас және ең үлкен адамның жасын ғана сақтай аламыз. Сұрақ нақты жасқа қатысты болса, онда мұндай қатысушының жоқ екенін сенімді түрде айтуға болады. Әйтпесе, біз жауап бере алмайтынымызды ғана айта аламыз. Есептеуде нақты ақпаратты шекті уақыт пен жад көлемінде алу көбінесе мүмкін емес (Райс теоремасы мен тоқтату мәселесін қараңыз). Абстракция сұрақтарға жалпыланған жауап беруге мүмкіндік береді (мысалы, "әлдеқайда" деп жауап беру, "иә" немесе "жоқ" дегенді білдіреді, егер абстрактілік интерпретация алгоритмі нақты жауапты анықтай алмаса); бұл мәселені жеңілдетеді және автоматты шешімдерге бейімдейді. Маңызды талап – маңызды сұрақтарға жауап беру үшін жеткілікті дәлдікті сақтай отырып, проблемаларды шешуге жететіндей белгісіздікті қосу (мысалы, "бағдарлама құлап қалуы мүмкін бе?" деген сұраққа жауап беру).

This section illustrates abstract interpretation by means of real world, non computing examples. Consider the people in a conference room. Assume a unique identifier for each person in the room, like a social security number in the United States. To prove that someone is not present, all one needs to do is see if their social security number is not on the list. Since two different people cannot have the same number, it is possible to prove or disprove the presence of a participant simply by looking up their number. However it is possible that only the names of attendees were registered. If the name of a person is not found in the list, we may safely conclude that that person was not present; but if it is, we cannot conclude definitely without further inquiries, due to the possibility of homonyms (for example, two people named John Smith). Note that this imprecise information will still be adequate for most purposes, because homonyms are rare in practice. However, in all rigor, we cannot say for sure that somebody was present in the room; all we can say is that they were possibly here. If the person we are looking up is a criminal, we will issue an alarm; but there is of course the possibility of issuing a false alarm. Similar phenomena will occur in the analysis of programs. If we are only interested in some specific information, say, "was there a person of age in the room? ", keeping a list of all names and dates of births is unnecessary. We may safely and without loss of precision restrict ourselves to keeping a list of the participants' ages. If this is already too much to handle, we might keep only the age of the youngest, and oldest person, If the question is about an age strictly lower than or strictly higher than , then we may safely respond that no such participant was present. Otherwise, we may only be able to say that we do not know. In the case of computing, concrete, precise information is in general not computable within finite time and memory (see Rice's theorem and the halting problem). Abstraction is used to allow for generalized answers to questions (for example, answering "maybe" to a yes/no question, meaning "yes or no", when we (an algorithm of abstract interpretation) cannot compute the precise answer with certainty); this simplifies the problems, making them amenable to automatic solutions. One crucial requirement is to add enough vagueness so as to make problems manageable while still retaining enough precision for answering the important questions (such as "might the program crash? ").

Компьютерлік бағдарламалардың тұжырымдамалық интерпретациясы

Бағдарламалау немесе спецификация тілінің негізінде абстрактілік интерпретация – абстракция қатынастары арқылы байланыстырылған бірнеше семантиканы ұсынудан тұрады. Семантика – бағдарламаның мүмкін болатын мінез-құлқының математикалық сипаттамасы. Бағдарламаның нақты орындалуын өте жақын сипаттайтын ең нақты семантика нақты семантика деп аталады. Мысалы, императивті бағдарламалау тілінің нақты семантикасы әр бағдарламаны оның тудыра алатын орындалу іздерінің жиынтығымен байланыстырады – орындалу іздері бағдарламаның орындалуының ықтимал тізбекті күйлері болып табылады; күй әдетте бағдарлама санағышының және жад орындарының (глобалдық, стек және үйінді) мәнінен тұрады. Содан кейін абстрактілірек семантикалар туындырылады; мысалы, орындалулардағы қолжетімді күйлердің жиынтығын ғана қарастыруға болады (бұл шекті іздердегі соңғы күйлерді қарастырумен тең). Статикалық талдаудың мақсаты – белгілі бір сәтте есептеуге болатын семантикалық интерпретацияны алу. Мысалы, бүтін сан айнымалыларын өңдейтін бағдарламаның күйін айнымалылардың нақты мәндерін естен шығарып, тек олардың таңбаларын (+, - немесе 0) сақтап беру арқылы бейнелеуге болады. Кейбір қарапайым операциялар үшін, мысалы, көбейту үшін, мұндай абстракция дәлдікті жоғалтпайды: көбейтіндінің таңбасын алу үшін операндтардың таңбасын білу жеткілікті. Ал кейбір басқа операциялар үшін абстракция дәлдікті жоғалтуы мүмкін: мысалы, операндалары тиісінше оң және теріс болатын қосындының таңбасын білу мүмкін емес. Кейде семантиканы шешімді ету үшін дәлдікті жоғалту қажет (Райс теоремасы мен тоқтау мәселесін қараңыз). Жалпы алғанда, талдаудың дәлдігі мен оның шешімділігі (есептеу мүмкіндігі) немесе тиімділігі (есептеу шығындары) арасында компромисс жасау қажет. Іс жүзінде анықталатын абстракциялар талдауға ұмтылатын бағдарламаның қасиеттеріне және мақсатты бағдарламалар жиынтығына бейімделеді. Компьютерлік бағдарламаларды абстрактілік интерпретация арқылы алғашқы ірі масштабты автоматтандырылған талдау 1996 жылы Ariane 5 зымыранының алғашқы ұшырылысын құлатқан апаттан туындады.

Given a programming or specification language, abstract interpretation consists of giving several semantics linked by relations of abstraction. A semantics is a mathematical characterization of a possible behavior of the program. The most precise semantics, describing very closely the actual execution of the program, are called the concrete semantics. For instance, the concrete semantics of an imperative programming language may associate to each program the set of execution traces it may produce – an execution trace being a sequence of possible consecutive states of the execution of the program; a state typically consists of the value of the program counter and the memory locations (globals, stack and heap). More abstract semantics are then derived; for instance, one may consider only the set of reachable states in the executions (which amounts to considering the last states in finite traces). The goal of static analysis is to derive a computable semantic interpretation at some point. For instance, one may choose to represent the state of a program manipulating integer variables by forgetting the actual values of the variables and only keeping their signs (+, − or 0). For some elementary operations, such as multiplication, such an abstraction does not lose any precision: to get the sign of a product, it is sufficient to know the sign of the operands. For some other operations, the abstraction may lose precision: for instance, it is impossible to know the sign of a sum whose operands are respectively positive and negative. Sometimes a loss of precision is necessary to make the semantics decidable (see Rice's theorem and the halting problem). In general, there is a compromise to be made between the precision of the analysis and its decidability (computability), or tractability (computational cost). In practice the abstractions that are defined are tailored to both the program properties one desires to analyze, and to the set of target programs. The first large scale automated analysis of computer programs with abstract interpretation was motivated by the accident that resulted in the destruction of the first flight of the Ariane 5 rocket in 1996.