一種基於JPF的Java代碼SSA單路徑的生成方法與流程

2023-06-07 03:53:46

本發明涉及一種基於JPF的Java代碼SSA單路徑的生成方法。

背景技術：

程序靜態分析(Program Static Analysis)是在不運行程序的前提下進行的代碼分析工作，隨著越來越多的代碼被上傳到開原始碼庫中，大多數代碼不可以直接運行，我們要對這些開原始碼進行分析理解，就需要藉助靜態分析技術。靜態分析技術中經常會涉及到符號執行(Symbolic Execution)，抽象語法樹(Abstract Syntax Tree，AST)分析，控制流分析(Control Flow Analysis)等，借鑑這些靜態分析技術的思想，我們旨在提供一種Java代碼靜態單賦值(Static Single Assignment，SSA)格式的單路徑的生成方法支持Java代碼靜態分析方面的工作，研究者可以在該工具的基礎上進行Java代碼的分析，降低了直接從代碼文本進行分析的複雜性。

JPF(Java PathFinder)是由NASA開發的針對Java程序的模型檢驗工具，它的核心是一個Java虛擬機，其符號執行模塊jpf-symbc可以對Java代碼進行符號執行，提取出程序中的每一條可達路徑以及路徑上的約束。

JDT(Java Development Tools)是Eclipse提供的一組用於實現Java IDE的工具，核心是AST，利用JDT提供的AST訪問API，我們可以將Java代碼轉化成AST，遍歷AST樹節點，修改AST樹結構並將修改寫回到原始碼。

技術實現要素：

針對現有技術中存在的問題，本發明目的是，提供一種Java代碼SSA格式的單路徑的生成方法支持Java代碼靜態分析方面的工作，研究者可以在該工具的基礎上進行Java代碼的分析，降低了直接從代碼文本進行分析的複雜性。

本發明是通過以下的技術方案實現的：一種基於JPF的Java代碼SSA單路徑的生成方法，包括步驟：

步驟10：輸入.java文件和.jpf文件，存放在src目錄下；

步驟11：對.java文件進行代碼插樁，以便獲得path condition；

步驟12：編譯得到.class文件，存放在bin目錄下；

步驟13：從.jpf文件獲得JPF執行的相關參數；

步驟14：使用JPF的jpf-symbc模塊對.class文件進行符號執行，獲取指定方法中的可達的單路徑，根據插樁信息提取出path condition；

步驟15：使用JDT AST修改單路徑代碼的AST，將單路徑轉化為SSA的格式；

步驟16：將SSA格式的單路徑以及path condition封裝成符合Java語法規範的Java類，存放在path目錄下，作為輸出。

其中步驟10所輸入的Java工程原始碼和JPF配置文件具有如下的目錄結構：

經過步驟16之後，最終輸出相應的結果：

在步驟11中，進行代碼插樁過程包括：

步驟20：使用ASTParser獲得單路徑代碼的AST；

步驟21：使用ASTVisitor遍歷Java代碼的AST獲取所有控制轉移語句如IfStatement，WhileStatement，以IfStatement為例；

步驟22：使用ASTRewrite修改AST的樹結構，在IfStatement成立的程序入口(ThenStatement)處插入一條空的IfStatement，控制條件與當前控制語句的控制條件相同；

步驟23：使用ASTRewrite修改AST的樹結構，在IfStatement不成立的程序入口(ElseSatement)處插入一條空的IfStatement，控制條件為當前控制語句的控制條件的非；

步驟24：將上述修改操作寫回到原始碼。

在步驟14中，使用JPF的jpf-symbc對.class文件進行符號執行，獲取指定方法中的可達的單路徑，根據插樁信息提取出path condition的過程包括：

步驟30：將.jpf中的配置信息傳給JPF啟動類，其中.jpf文件的書寫遵循JPF配置文件的書寫規範

步驟31：將classpath指定為步驟12得到的bin目錄，將sourcepath指定為src目錄，將Listener設為MyPathListener；

步驟32：MyListener是工具自定義的一個ListenerAdapter，它在JPF執行過程中監聽每一條指令的執行，抽取出每條指令所對應的原始碼行號；

步驟33：JPF會執行Java代碼中的每一條路徑，在執行過程中我們獲得每一條路徑對應的行號序列，將其對應到原始碼，提取插樁信息作為path condition。

處理流程如圖5所示：本發明實施例的監聽JPF指令執行獲得單路徑示意圖。

在步驟15中，將單路徑轉化為SSA的形式的過程包括：

步驟40：使用ASTParser獲得單路徑代碼的AST；

步驟41：使用ASTVisitor遍歷AST，收集變量的聲明、引用、賦值；

步驟42：使用ASTRewrite刪掉AST所有關於變量聲明的ASTNode；

步驟43：每當變量被賦值，就為該變量賦予一個新的變量名(對應AST中的SimpleName節點)，使之成為一個新變量，該次賦值之後到下一次賦值之前對變量的引用均用新的變量名替換，在程序的開頭添加新變量的聲明；

步驟44：將上述修改操作寫回到原始碼。

本發明有益效果：這是一個原始碼層面的藉助於JPF提取Java代碼中的單路徑然後利用JDT AST將其轉化為SSA格式的靜態分析輔助工具，利用這種工具，Java程序被簡化成了一條條SSA格式的單路徑代碼，從而降低了直接從原始碼進行分析的複雜性。

附圖說明

圖1本發明實施例的Java代碼轉化為SSA單路徑示意圖。

圖2本發明實施例的輸入目錄結構示意圖。

圖3本發明實施例的輸出目錄結構示意圖。

圖4本發明實施例的代碼插樁獲得路徑條件示意圖。

圖5本發明實施例的監聽JPF指令執行獲得單路徑示意圖。

圖6本發明實施例的單路徑代碼轉換為SSA格式示意圖。

具體實施方式

以下結合附圖和具體實施例對本發明作進一步詳細說明。

本發明方法工作流程如圖1-圖6所示。

圖1所示為本方法實施的整體結構和工作原理。本方法的目的是提供一個原始碼層面的藉助於JPF提取Java代碼中的單路徑然後利用JDT AST將其轉化為SSA格式的靜態分析輔助工具，利用這種工具，Java程序被簡化成了一條條SSA格式的單路徑代碼，從而降低了直接從原始碼進行分析的複雜性。

本實施例的一種基於JPF的Java代碼SSA單路徑的生成方法，包括如下步驟：

步驟10：輸入.java文件和.jpf文件，存放在src目錄下；

步驟11：對.java文件進行代碼插樁，以便獲得path condition；

步驟12：編譯得到.class文件，存放在bin目錄下；

步驟13：從.jpf文件獲得JPF執行的相關參數；

步驟14：使用JPF的jpf-symbc模塊對.class文件進行符號執行，獲取指定方法中的可達的單路徑，根據插樁信息提取出path condition；

步驟15：使用JDT AST修改單路徑代碼的AST，將單路徑轉化為SSA的格式；

步驟16：將SSA格式的單路徑以及path condition封裝成符合Java語法規範的Java類，存放在path目錄下，作為輸出。

圖2表示的是步驟10所輸入的Java工程原始碼和JPF配置文件所在src目錄的目錄結構示意圖。其中步驟10所輸入的Java工程原始碼和JPF配置文件具有如下的目錄結構：

圖3表示的是經過步驟16之後，存放單路徑代碼的path目錄所具有的目錄結構示意圖。經過步驟16之後，最終的輸出結果如下：

圖4表示的是在步驟11中使用JDT AST進行代碼插樁的處理示意圖，執行的過程包括：

步驟20：使用ASTParser獲得單路徑代碼的AST；

步驟21：使用ASTVisitor遍歷Java代碼的AST獲取所有控制轉移語句如IfStatement，WhileStatement，下面以IfStatement為例；

步驟22：使用ASTRewrite修改AST的樹結構，在IfStatement成立的程序入口(ThenStatement)處插入一條空的IfStatement，控制條件與當前控制語句的控制條件相同；

步驟23：使用ASTRewrite修改AST的樹結構，在IfStatement不成立的程序入口(ElseSatement)處插入一條空的IfStatement，控制條件為當前控制語句的控制條件的非；

步驟24：將上述修改操作寫回到原始碼。

下面給出一個插樁前後對比的例子：

圖5表示的是在步驟14中使用JPF的jpf-symbc對.class文件進行符號執行，獲取指定方法中的可達的單路徑，根據插樁信息提取出path condition的處理示意圖，執行的過程包括：

步驟30：將.jpf中的配置信息傳給JPF啟動類，其中.jpf文件的書寫遵循JPF配置文件的書寫規範；

步驟31：將classpath指定為步驟12得到的bin目錄，將sourcepath指定為src目錄，將Listener設為MyPathListener；

步驟32：MyListener是工具自定義的一個ListenerAdapter，它在JPF執行過程中監聽每一條指令的執行，抽取出每條指令所對應的原始碼行號；

步驟33：JPF會執行Java代碼中的每一條路徑，在執行過程中我們獲得每一條路徑對應的行號序列，將其對應到原始碼，提取插樁信息作為path condition。

處理流程如圖5所示：本發明實施例的監聽JPF指令執行獲得單路徑示意圖。

圖6表示的是在步驟15中，將單路徑轉化為SSA的形式的處理示意圖，執行的過程包括：

步驟40：使用ASTParser獲得單路徑代碼的AST；

步驟41：使用ASTVisitor遍歷AST，收集變量的聲明、引用、賦值；

步驟42：使用ASTRewrite刪掉AST所有關於變量聲明的ASTNode；

步驟43：每當變量被賦值，就為該變量賦予一個新的變量名(對應AST中的SimpleName節點)，使之成為一個新變量，該次賦值之後到下一次賦值之前對變量的引用均用新的變量名替換，在程序的開頭添加新變量的聲明；

步驟44：將上述修改操作寫回到原始碼。

下面給出一個轉換前後對比的例子：

以上所述，僅為本發明的較佳實施例而已，並非對本發明作任何形式上的限制，雖然本發明已以較佳實施例揭露如上，然而並非用以限定本發明，任何熟悉本專業的技術人員，在不脫離本發明技術方案範圍內，當可利用上述揭示的技術內容作出些許更改或修飾為等同變化的等效例，則仍屬於本發明技術方案的保護範圍內。