sea dsa
1.0.0
SeaDsa DSA에서 영감을 얻은 LLVM 비트 코드에 대한 컨텍스트, 필드 및 어레이에 민감한 통일 기반 포인트-투 포인트-투 포인트 분석입니다. SeaDsa 는 컨텍스트 감도의 개선, 부분 흐름 감수성 추가 및 유형 인식 덕분에 Dsa 보다 확장 가능하고 정확한 순서이며 이전 SeaDsa 구현입니다.
SeaDsa 임의의 LLVM 비트 코드를 분석 할 수 있지만 C/C ++ 프로그램의 프로그램 검증에 사용하도록 조정되었습니다. 독립형 도구 또는 Seahorn Verification Framework 및 분석과 함께 사용할 수 있습니다.
이 지점은 LLVM 14를 지원합니다.
SeaDsa C ++로 작성되었으며 Boost 라이브러리를 사용합니다. 주요 요구 사항은 다음과 같습니다.
테스트를 실행하려면 다음 패키지를 설치하십시오.
sudo pip install lit OutputChecksudo easy_install networkxsudo apt-get install libgraphviz-devsudo easy_install pygraphvizGraph , 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에서 찾을 수 있습니다.
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 논문에서 구현 된 분석을 가능하게합니다 (참조 참조). 이 명령은 FUN 코드 프로그램에서 각 함수에 대한 FUN.mem.dot 파일을 생성합니다. 우리의 경우 유일한 기능은 main 이므로 main.mem.dot 이라는 파일이 하나 있습니다. 파일은 현재 디렉토리에서 생성됩니다. .dot 파일을 다른 디렉토리에 저장하려면 옵션을 추가하십시오 -sea-dsa-dot-outdir=DIR 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 로 가리키며 동일한 메모리 객체와 2 개의 다른 셀입니다. 필드 <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)
외부 통화의 포인터 의미론은 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 에 의해 지적 된 셀을 붕괴 시키라고 지시하고 (예 : seadsa_mk_seq sea-dsa 크기 sz 로 p 에 의해 P를 순서 대로 표시하도록 지시합니다.
예를 들어, 다음과 같이 정의 된 외부 통화 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;
}
A. Gurfinkel 및 JA Navas의 "C/C ++ 프로그램 검증을위한 컨텍스트 감각 메모리 모델". SAS'17에서. (종이) | (슬라이드)
J. Kuderski, Ja Navas 및 A. Gurfinkel의 "Oversharing없이 통일 기반 포인터 분석". fmcad'19에서. (종이)
