以程式變換方法協助程式分析器驗證遞迴程式

Abstract

在程序分析(Program Analysis) 領域中，分析遞迴程式(Recursive Program) 是一項難以處理的課題。現有程式分析工具往往因為無法處理程式中的遞迴函式，既而忽略部分程式碼不進行分析，或甚至拒絕檢驗遞迴程式。本篇論文針對遞迴程式的分析提出新的觀點與分析方法；作者認為與其重新設計演算法且實作新的分析器，不如改進現有的程式分析工具。但更改他人實作的軟體工具並非易事，因此本文提出的方法將現有的工具視為黑箱不做任何更動，反而是利用程式變換方法(Program Transformation) 將待分析的遞迴程式轉換成無遞迴的程式，再交給黑箱分析工具進行檢驗；並使用黑箱工具提供被分析程式中的不變量(Invariants)，進而證明原遞迴程式的正確性。 本篇作者與實驗室團隊受惠於程式分析工具CPAchecker，實作出此演算法的雛型CPArec，且參與2015年度軟體驗證競賽(Competition on Software Verification)；和其它頂尖實驗室所開發工具相較，我們的工具針對遞迴程式進行分析時，亦表現出相當的效率及效能，獲得第三名的佳績。 關鍵字：軟體驗證、程序分析、靜態分析、遞迴程式、程式變換方法

Recursion can complicate program analysis significantly. Some program analyzers simply ignore recursion or even refuse to check recursive programs. In this paper, we propose an algorithm that uses a recursion-free program analyzer as a black box to check recursive programs. With extended program constructs for assumptions, assertions, and non-deterministic values, our algorithm computes function summaries from inductive invariants computed by the underlying program analyzer. Such function summaries enable our algorithm to check recursive programs. We implement a prototype named CPArec using the recursion-free program analyzer CPAchecker. Under the comparison with other program analyzers on the benchmarks in the 2014 and 2015 Competitions on Software Verification, our tool shows competitive efficiency and effectiveness on verifying programs with recursion. Key words: CPArec, Software Verification, Program Analysis, Static Analysis, Recursion, Program Transformation