一類范圍約束的浮點(diǎn)數(shù)靜態(tài)分析方法.pdf

1、抽象解釋理論是Cousot.P和Cousot.R于1977年提出的程序靜態(tài)分析時(shí)構(gòu)造和逼近程序的不動(dòng)點(diǎn)理論。它的一個(gè)重要應(yīng)用是分析程序中的變量或約束表達(dá)式的值域。這些值域信息有助于進(jìn)行數(shù)組和循環(huán)的界限分析,基于數(shù)組的數(shù)據(jù)依賴性分析,指針?lè)治?循環(huán)時(shí)間分析,可執(zhí)行路徑分析等。
　　 抽象解釋理論的特點(diǎn)是可靠但不完備的,即:如果驗(yàn)證結(jié)果表明抽象系統(tǒng)滿足驗(yàn)證性質(zhì),則抽象解釋理論保證原系統(tǒng)也滿足驗(yàn)證性質(zhì):若驗(yàn)證結(jié)果表明抽象系統(tǒng)不滿足驗(yàn)證

2、性質(zhì),則原系統(tǒng)可能滿足驗(yàn)證性質(zhì),可能不滿足驗(yàn)證性質(zhì),需要更精細(xì)的抽象分析。而一個(gè)精確的抽象域能夠減少這種不完備性,有利于提高驗(yàn)證效率。因此,設(shè)計(jì)一個(gè)精確的抽象域及定義抽象域上抽象運(yùn)算是抽象解釋理論研究的核心內(nèi)容。
　　 本文利用抽象解釋理論對(duì)浮點(diǎn)數(shù)表達(dá)式約束問(wèn)題的值域進(jìn)行了估測(cè),主要的目標(biāo)改善不完備性。其主要工作如下:
　　 首先,基于IEEE754—1985浮點(diǎn)數(shù)模型規(guī)范,結(jié)合抽象解釋理論中的完備格的性質(zhì),本文提出了浮

3、點(diǎn)數(shù)的抽象語(yǔ)義。然后根據(jù)區(qū)間抽象域的一些運(yùn)算特性和IEEE754—1985浮點(diǎn)數(shù)模型的舍入模式,定義了這種抽象域的抽象運(yùn)算。
　　 其次,為均衡浮點(diǎn)數(shù)表達(dá)式的計(jì)算精度和計(jì)算效率,在浮點(diǎn)數(shù)抽象模型以及抽象運(yùn)算的基礎(chǔ)上,本文為兩個(gè)變量的浮點(diǎn)數(shù)線性表達(dá)式約束問(wèn)題建立區(qū)間約束。為區(qū)間約束建立區(qū)間約束圖,在約束圖的基礎(chǔ)上,把這類浮點(diǎn)數(shù)約束問(wèn)題轉(zhuǎn)化為區(qū)間線性方程。利用上面定義的區(qū)間運(yùn)算,本文給出了這類問(wèn)題的解。
　　 最后,本文提出