clam

조개 : 게의 LLVM 프론트 엔드

Clam은 크랩 라이브러리를 기반으로 LLVM 비트 코드에 대한 유도 불일치를 계산하는 추상 해석 기반 정적 분석기입니다. 이 지점은 LLVM 14를 지원합니다.

사용 가능한 문서는 Clam Wiki와 Crab Wiki에서 찾을 수 있습니다.

도커

명령을 사용하여 Docker Hub (야간 제작)에서 조개를 얻을 수 있습니다.

 docker pull seahorn/clam-llvm14:nightly

요구 사항

Clam은 C ++로 작성되었으며 Boost 라이브러리를 많이 사용합니다. 주요 요구 사항은 다음과 같습니다.

• C ++ 14를 지원하는 최신 C ++ 컴파일러
• 부스트> = 1.65
• GMP
• mpfr ( -DCRAB_USE_APRON=ON or -DCRAB_USE_ELINA=ON ).
• Flint ( -DCRAB_USE_PPLITE=ON 인 경우에만)
• 파이썬> = 3.6

Linux에서는 명령을 입력하는 요구 사항을 설치할 수 있습니다.

 sudo apt-get install libboost-all-dev libboost-program-options-dev
 sudo apt-get install libgmp-dev
 sudo apt-get install libmpfr-dev	
 sudo apt-get install libflint-dev

테스트

테스트 인프라는 여러 Python 패키지에 따라 다릅니다. 테스트를 실행하려면 lit 및 OutputCheck 설치해야합니다.

 pip3 install lit
 pip3 install OutputCheck

편집 및 설치

기본 컴파일 단계는 다음과 같습니다.

 1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR ../
3. cmake --build . --target crab && cmake ..   
4. cmake --build . --target extra && cmake ..                  
5. cmake --build . --target install 

2 행의 명령은 표준 경로에서 LLVM 14를 찾으려고합니다. 비표준 경로에 llvm 14를 설치 한 경우 옵션 -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm 에 2 행을 추가하십시오. 3 행의 명령은 크랩을 다운로드하여 소스에서 컴파일합니다. Clam은 4 행의 extra 대상을 통해 설치된 두 가지 외부 구성 요소를 사용합니다. 이러한 구성 요소는 다음과 같습니다.

• SEA-DSA는 LLVM 메모리 지침을 번역하는 데 사용되는 힙 분석입니다. 자세한 내용은 여기와 여기에서 찾을 수 있습니다.

• LLVM-Seahorn은 LLVM 구성 요소의 특수 버전을 제공하여 검증에 더 적합합니다. llvm-seahorn 은 선택 사항이지만 Hightly 권장입니다.

상자/앞치마/Elina/Pplite 도메인에는 타사 라이브러리가 필요합니다. 해당 도메인에 관심이없는 사용자에게 부담을 피하기 위해 라이브러리 설치는 선택 사항입니다.

• 상자 도메인을 사용하려면 -DCRAB_USE_LDD=ON 옵션을 추가하십시오.

• 앞치마 라이브러리 도메인을 사용하려면 -DCRAB_USE_APRON=ON 옵션을 추가하십시오.

• Elina 라이브러리 도메인을 사용하려면 -DCRAB_USE_ELINA=ON 옵션을 추가하십시오.

• pplite 라이브러리 도메인을 사용하려면 -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON 옵션을 추가하십시오.

중요 : Apron과 Elina는 현재 호환되지 않으므로 -DCRAB_USE_APRON=ON 및 -DCRAB_USE_ELINA=ON 동시에 활성화 할 수 없습니다.

예를 들어, 상자와 앞치마로 조개를 설치하려면 :

 1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target crab && cmake ..
4. cmake --build . --target extra && cmake ..                
5. cmake --build . --target ldd && cmake ..
6. cmake --build . --target apron && cmake ..             
7. cmake --build . --target install 

예를 들어, 5와 6 행은 각각 상자와 앞치마 라이브러리를 다운로드, 컴파일 및 설치합니다. 이미 시스템에 이러한 라이브러리를 컴파일하고 설치 한 경우 5 번 및 6 행에서 명령을 건너 뛰고 2 행에 다음 옵션을 추가하십시오.

• 앞치마의 경우 : -DAPRON_ROOT=$APRON_INSTALL_DIR
• Elina의 경우 : -DELINA_ROOT=$ELINA_INSTALL_DIR
• 상자의 경우 : -DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR
• pplite의 경우 : -DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR

설치 확인

회귀 테스트를 실행하려면 :

 cmake --build . --target test-simple

용법

Clam은 사용자와 상호 작용하기 위해 clam.py ( $DIR/bin 에 위치한 $DIR 에 위치)라는 파이썬 스크립트를 제공합니다. 가장 간단한 명령은 clam.py test.c 입니다. clam.py --help 모든 옵션에 대해 help를 입력하고 Wiki를 읽으십시오.