[發(fā)明專利]一種遞歸最大執(zhí)行頻度與深度的靜態(tài)估計(jì)方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201410589530.4
• 申請(qǐng)日: 2014-10-28
• 公開(kāi)（公告）號(hào): CN104317773A
• 公開(kāi)（公告）日: 2015-01-28
• 發(fā)明（設(shè)計(jì)）人: 湯恩義;劉璐;方園;李宣東;馮世寧;張慶壘
• 申請(qǐng)（專利權(quán)）人: 南京大學(xué)
• 主分類號(hào): G06F17/10
• 分類號(hào): G06F17/10
• 代理公司: 南京瑞弘專利商標(biāo)事務(wù)所(普通合伙) 32249
• 代理人: 楊曉玲

技術(shù)領(lǐng)域

本發(fā)明屬于計(jì)算機(jī)程序分析應(yīng)用領(lǐng)域，涉及利用靜態(tài)程序分析、可滿足性模條件約束求解等技術(shù)，高效求解程序遞歸最大執(zhí)行頻度與最大執(zhí)行深度，從而為設(shè)計(jì)開(kāi)發(fā)人員進(jìn)行程序優(yōu)化，能耗估計(jì)，時(shí)間分析等提供依據(jù)，為一種程序遞歸最大執(zhí)行頻度與最大執(zhí)行深度的靜態(tài)估計(jì)方法。

背景技術(shù)

遞歸作為一種算法設(shè)計(jì)思想，在程序設(shè)計(jì)與開(kāi)發(fā)中被廣泛使用。實(shí)際工業(yè)程序中的遞歸具有執(zhí)行密度大，占用執(zhí)行時(shí)間長(zhǎng)等特點(diǎn)，對(duì)程序的執(zhí)行效率，計(jì)算機(jī)的性能和吞吐量有重要影響。因此，遞歸作用域的最大執(zhí)行頻度和深度是程序優(yōu)化，時(shí)間分析，系統(tǒng)能耗分析等領(lǐng)域所關(guān)注的重要指標(biāo)。

已有的遞歸執(zhí)行頻度和深度估計(jì)方法一般采用動(dòng)態(tài)測(cè)試方法，通過(guò)生成測(cè)試用例對(duì)程序反復(fù)執(zhí)行，來(lái)獲得遞歸作用域可能達(dá)到的執(zhí)行頻率和執(zhí)行深度。這樣的方法有以下幾個(gè)不足：1.檢測(cè)效率不高：由于動(dòng)態(tài)方法需要反復(fù)執(zhí)行程序，因此需要一定的執(zhí)行量才能檢測(cè)到所關(guān)心的遞歸作用域的相應(yīng)指標(biāo)；2.檢測(cè)結(jié)果準(zhǔn)確度不夠：由于動(dòng)態(tài)檢測(cè)方法依賴于測(cè)試用例，當(dāng)測(cè)試用例的覆蓋度不夠時(shí)，未覆蓋到的遞歸作用域是無(wú)法獲得檢測(cè)結(jié)果的；即使測(cè)試用例能覆蓋到的遞歸，也很難保證測(cè)試用例能使得遞歸執(zhí)行到最大的頻度和深度。

近年來(lái)，計(jì)算機(jī)自動(dòng)化的符號(hào)約束求解能力大大提升，為能自動(dòng)地靜態(tài)檢測(cè)遞歸執(zhí)行頻度和深度提供了可能。本發(fā)明基于可滿足性模理論，通過(guò)靜態(tài)收集與求解不同深度與頻度的遞歸符號(hào)執(zhí)行條件，來(lái)獲得遞歸能在程序執(zhí)行中達(dá)到的最大執(zhí)行頻度與深度信息，能夠在較少的計(jì)算時(shí)間內(nèi)達(dá)到較為準(zhǔn)確的檢測(cè)結(jié)果。

可滿足性模理論是計(jì)算機(jī)科學(xué)領(lǐng)域中在一階謂詞邏輯等式的基礎(chǔ)上發(fā)展起來(lái)的邏輯公式判定理論，主要用于判斷一階邏輯公式是否可被滿足。由于許多領(lǐng)域的實(shí)際問(wèn)題最終都可以被歸結(jié)為可滿足性模理論問(wèn)題(例如軟硬件的形式化驗(yàn)證問(wèn)題、電路的自動(dòng)向量測(cè)試生成、人工智能中的規(guī)劃與優(yōu)化問(wèn)題等)，可滿足性模理論近年來(lái)受到計(jì)算機(jī)理論界的廣泛關(guān)注。目前廣泛使用的可滿足性模理論求解方法大約有三種：第一種方法將一階謂詞邏輯公式轉(zhuǎn)換成更為簡(jiǎn)單的布爾公式，然后在此基礎(chǔ)上求解布爾公式的可滿足性；第二種方法將需要求解的內(nèi)容根據(jù)其特性而劃分成專門(mén)的理論域，并在各個(gè)理論域分別求解；第三種方法將該問(wèn)題的求解歸結(jié)到一種基于回溯的搜索算法框架中，并通過(guò)置換理論域，而達(dá)到高效可滿足性求解的目的。經(jīng)過(guò)研究者多年的努力，可滿足性模理論求解算法得到了不斷的改進(jìn)與完善，已經(jīng)能夠解決實(shí)際應(yīng)用中規(guī)模較大的問(wèn)題。本發(fā)明利用可滿足性模理論來(lái)靜態(tài)求解遞歸作用域的執(zhí)行條件約束，從而實(shí)現(xiàn)遞歸最大執(zhí)行頻度與最大執(zhí)行深度的靜態(tài)估計(jì)。

發(fā)明內(nèi)容

技術(shù)問(wèn)題：本發(fā)明提出了一種遞歸最大執(zhí)行頻度與最大執(zhí)行深度的靜態(tài)估計(jì)方法，該方法不需要反復(fù)執(zhí)行程序，即可以較為準(zhǔn)確的估計(jì)出程序遞歸的最大執(zhí)行頻度和最大執(zhí)行深度。

技術(shù)方案：本發(fā)明的一種遞歸最大執(zhí)行頻度與深度的靜態(tài)估計(jì)方法，通過(guò)靜態(tài)程序分析的方法來(lái)收集程序的遞歸路徑條件，并使用可滿足性模理論來(lái)求解該遞歸路徑條件，從而能高效準(zhǔn)確的估計(jì)程序中遞歸作用域的最大執(zhí)行深度，以及作用域中各遞歸函數(shù)的最大執(zhí)行頻度，具體步驟為：

1-1)、使用基于調(diào)用圖的回路查找技術(shù)來(lái)檢測(cè)程序中的遞歸作用域，所檢測(cè)到的遞歸作用域?yàn)橐粋€(gè)函數(shù)集合，集合中的各個(gè)函數(shù)相互調(diào)用，而構(gòu)成遞歸，在檢測(cè)過(guò)程中，使用強(qiáng)連通組件擴(kuò)展技術(shù)來(lái)擴(kuò)展調(diào)用圖的回路，從而保證了所得到的函數(shù)集合包含當(dāng)前遞歸作用域中的每一個(gè)函數(shù)；

1-2)、分別分析步驟1-1)所得到的各個(gè)遞歸作用域，收集作用域中各個(gè)遞歸函數(shù)調(diào)用和遞歸函數(shù)返回的分支條件與路徑條件，并將相同遞歸函數(shù)的調(diào)用條件和返回條件合并，作為符號(hào)條件約束儲(chǔ)存，以供步驟1-3)進(jìn)行綜合求解；

1-3)、將各遞歸作用域放回原始程序中進(jìn)行綜合分析與求解，即在原始程序中求得各個(gè)遞歸作用域的初始入口條件，并依據(jù)此入口條件與步驟1-2)給出的符號(hào)條件約束綜合構(gòu)建不同執(zhí)行深度與執(zhí)行頻度的實(shí)際遞歸執(zhí)行約束，最終使用可滿足性模求解器對(duì)這些實(shí)際的遞歸執(zhí)行約束求解。通過(guò)結(jié)合不同的遞歸深度與頻度嘗試策略，求解器能估計(jì)出遞歸實(shí)際可達(dá)的最大執(zhí)行頻度和深度。

所述的步驟1-1)中使用強(qiáng)連通組件擴(kuò)展技術(shù)來(lái)擴(kuò)展調(diào)用圖的回路的遞歸檢測(cè)方法，使得所得到的函數(shù)集合必然包含當(dāng)前遞歸作用域中的每一個(gè)函數(shù)，具體如下：

2-1)、由程序源代碼按照傳統(tǒng)方法構(gòu)建調(diào)用圖，調(diào)用圖是一個(gè)用來(lái)表示程序調(diào)用關(guān)系的有向圖，圖中每一條有向邊(f,g)代表程序中存在函數(shù)f到函數(shù)g的調(diào)用關(guān)系，因此，調(diào)用圖上的任意回路表明在程序中存在函數(shù)遞歸關(guān)系；