sea dsa下載 - sea dsa源代碼下載

sea dsa

其他類別

1.0.0

下載

SEADSA：用於驗證低級C/C ++的點對點分析

SeaDsa是一個受DSA啟發的LLVM比特碼的上下文，字段和數組敏感的點對點分析。 SeaDsa是比Dsa更可擴展和精確的數量級，並且由於上下文靈敏度的處理，添加了部分流動敏感性和類型意識，因此SeaDsa的先前實現。

儘管SeaDsa可以分析任意LLVM比特碼，但已針對C/C ++程序的程序驗證進行了定制。它可以用作獨立工具，也可以與海角驗證框架及其分析一起使用。

該分支支持LLVM 14。

要求

SeaDsa用C ++編寫，並使用Boost庫。主要要求是：

C ++支持C ++ 14
Boost> = 1.65
LLVM 14

要運行測試，請安裝以下軟件包：

sudo pip install lit OutputCheck
sudo easy_install networkx
sudo apt-get install libgraphviz-dev
sudo easy_install pygraphviz

項目結構

主點對圖數據結構， Graph ， Cell和Node在include/Graph.hh和src/Graph.cc中定義。
本地分析include/Local.hh和src/DsaLocal.cc 。
自下而上的分析include/BottomUp.hh和src/DsaBottomUp.cc 。
自上而下的分析在include/TopDown.hh和src/DsaTopDown.cc中。
概要室節點克隆器中include/Cloner.hh和src/Clonner.cc 。
類型處理代碼在include/FieldType.hh中， include/TypeUtils.hh src/FieldType.cc src/TypeUtils.cc 。
分配器函數發現在include/AllocWrapInfo.hh和src/AllocWrapInfo.cc中。

彙編和用法

程序驗證基準

可以在TEA-DSA-EXTRAS中找到有關運行程序驗證基準的說明，以及用於構建現實世界項目的食譜以及我們的結果。

集成在其他C ++項目中（用於用戶）

SeaDsa包含兩個目錄： include和src 。由於SeaDsa分析了LLVM比特碼，因此使用SeaDsa構建時必須訪問LLVM標頭文件和庫。

如果您的項目使用cmake ，則只需要添加項目的CMakeLists.txt ：

 include_directories(seadsa/include)
 add_subdirectory(seadsa)

獨立（用於開發人員）

如果您已經在計算機上安裝了llvm-14 ：

 mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake  ..
cmake --build . --target install

否則：

 mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install

進行測試：

 cmake --build . --target test-sea-dsa

可視化存儲器圖和完整的呼叫圖

考慮一個稱為tests/c/simple.c的C程序：

 #include <stdlib.h>

typedef struct S {
  int * * x ;
  int * * y ;  
} S ;

int g ;

int main ( int argc , char * * argv ){

  S s1 , s2 ;

  int * p1 = ( int * ) malloc ( sizeof ( int ));
  int * q1 = ( int * ) malloc ( sizeof ( int ));  
  s1 . x = & p1 ;
  s1 . y = & q1 ;    
  * ( s1 . x ) = & g ;
  
  return 0 ;
}

生成比特代碼：

 clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll

選項-O0用於禁用clang優化。通常，啟用clang優化是一個好主意。但是，對於諸如simple.c之類的瑣碎示例，Clang簡化了太多，因此不會觀察到任何有用的東西。選項-c -emit-llvm -S以人類可讀格式生成比特碼。

在比特碼上運行sea-dsa並打印內存圖到點格式：

 seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot  simple.ll

選項-sea-dsa=butd-cs -sea-dsa-type-aware可以在我們的FMCAD'19論文中實施的分析（請參閱參考文獻）。此命令將在BitCode程序中為每個函數FUN生成一個FUN.mem.dot文件。在我們的情況下，唯一的函數是main ，因此，有一個名為main.mem.dot的文件。該文件是在當前目錄中生成的。如果要將.dot文件存儲在其他目錄DIR中，請添加選項-sea-dsa-dot-outdir=DIR

通過將其轉換為pdf文件，可視化main.mem.dot ：

 dot -Tpdf main.mem.dot -o main.mem.pdf
 open main.mem.pdf  // replace with you favorite pdf viewer

記憶圖的示例

在我們的內存模型中，指針值由一個單元格表示，該單元格是一對內存對象和偏移。內存對像在內存圖中表示為節點。邊緣在細胞之間。

每個節點字段代表一個單元格（即節點中的偏移）。例如，節點字段<0,i32**>和<8,i32**>分別由%6和%15指向，是來自同一內存對象的兩個不同的單元格。字段<8,i32**>表示相應內存對像中偏移8的單元格，其類型為i32** 。黑色邊緣代表細胞之間的點對點關係。它們標記為代表目標節點中偏移的數字。藍色邊緣將功能的形式參數與單元格連接。紫色邊緣將LLVM指針變量與單元格連接。節點可以具有諸如S （堆棧分配的內存）， H （堆分配內存）， M （修改後的內存）， R （讀取存儲器）， E （外部分配的內存）等等標記。標籤{void}用於表示該節點已分配，但該程序尚未使用該節點。

sea-dsa還可以解決間接電話。間接呼叫是一個呼叫，其中callee在靜態上不知道。 sea-dsa識別間接呼叫的所有可能級別，並生成LLVM呼叫圖作為輸出。

在tests/c/complete_callgraph_5.c中考慮此示例：

 struct class_t ;
typedef int ( * FN_PTR )( struct class_t * , int );
typedef struct class_t {
  FN_PTR m_foo ;
  FN_PTR m_bar ;
} class_t ;

int foo ( class_t * self , int x )
{
  if ( x > 10 ) {
    return self -> m_bar ( self , x + 1 );
  } else
    return x ;
}

int bar ( class_t * self , int y ) {
  if ( y < 100 ) {
    return y + self -> m_foo ( self , 10 );
  } else
    return y - 5 ;
}

int main ( void ) {
  class_t obj ;
  obj . m_foo = & foo ;
  obj . m_bar = & bar ;
  int res ;
  res = obj . m_foo ( & obj , 42 );
  return 0 ;
}

輸入命令：

 clang -c -emit-llvm -S tests/c/complete_callgraph_5.c  -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll

它在當前目錄中生成一個名為callgraph.dot的.dot文件。同樣， .dot文件可以轉換為.pdf文件並使用命令打開：

 dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf

呼叫圖的示例

sea-dsa還可以打印一些有關呼叫圖分辨率過程的統計信息（請注意，您需要用-g調用clang以打印文件，行和列信息）：

 sea-dsa --sea-dsa-callgraph-stats ex.ll


=== Sea-Dsa CallGraph Statistics === 
** Total number of indirect calls 0
** Total number of resolved indirect calls 3

%16 = call i32 %12(%struct.class_t* %13, i32 %15) at tests/c/complete_callgraph_5.c:14:12
RESOLVED
Callees:
  i32 bar(%struct.class_t*,i32)
  
%15 = call i32 %13(%struct.class_t* %14, i32 10) at tests/c/complete_callgraph_5.c:23:16
RESOLVED
Callees:
  i32 foo(%struct.class_t*,i32)
  
%11 = call i32 %10(%struct.class_t* %2, i32 42) at tests/c/complete_callgraph_5.c:36:9
RESOLVED
Callees:
  i32 foo(%struct.class_t*,i32)

處理C/C ++庫和外部呼叫

可以通過編寫呼叫包裝器來定義外部呼叫的指針語義，該包裝器調用seadsa/seadsa.h中定義的任何功能中的任何一個。

extern void seadsa_alias(const void *p, ...);
extern void seadsa_collapse(const void *p);
extern void seadsa_mk_seq(const void *p, unsigned sz);

seadsa_alias統一了所有參數的細胞， seadsa_collapse告訴sea-dsa崩潰（即，野外敏感性喪失） p指向P指向的細胞， seadsa_mk_seq告訴sea-dsa將其標記為序列為序列，該節點由p size sz pose o。

例如，考慮一個外部呼叫foo定義如下：

 extern void* foo(const void*p1, void *p2, void *p3);

假設返回的指針應統一為p2 ，而不是p1 。另外，我們希望折疊與p3相對應的細胞。然後，我們可以用以下定義替換上述foo的原型：

 #include "seadsa/seadsa.h"
void* foo(const void*p1, void *p2, void*p3) {
	void* r = seadsa_new();
	seadsa_alias(r,p2);
	seadsa_collapse(p3);
	return r;
}