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

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

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

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