crab
1.0.0
Crab은 추상 해석을 기반으로 한 프로그램 정적 분석을위한 C ++ 라이브러리입니다. Crab은 풍부한 추상 도메인, Kleene 기반 Fixpoint Solvers 및 DataFlow, 교차 및 후진과 같은 다양한 분석을 제공합니다. 게의 디자인은 매우 모듈 식이므로 새로운 초록 도메인 및 솔버를 쉽게 플러그인하거나 새로운 분석을 구축 할 수 있습니다.
게 초록 도메인은 메모리 내용, C와 같은 어레이 및 수치 특성에 대해 추론 할 수 있습니다. Crab은 구역 및 문어와 같은 인기있는 수치 도메인의 효율적인 구현과 예를 들어 상징적 인 용어 (일명 해석되지 않은 함수)에 대해 추론하기 위해 소설 도메인을 사용합니다. Crab은 또한 효율적인 환경 맵을 사용하여 Interval 또는 Congricences와 같은 대중적인 비 관계형 영역을 구현하고 표준 감소 된 제품 구성을 통해 임의의 도메인의 조합을 허용합니다. Crab은 또한 선형 의사 결정 다이어그램을 기반으로하는 박스라는 특수 분리 간격 및 임의의 도메인을 분리 완료의 과도한 태도로 끌어 올리는보다 일반적인 가치 파티셔닝 전략과 같은 비 컨버드 도메인을 제공합니다. 게 저자가 개발 한이 도메인 외에도 크랩 라이브러리는 Apron, Elina 및 Pplite와 같은 인기있는 추상 도메인 라이브러리를 통합합니다.
Crab은 Bourdoncle의 약한 토폴로지 순서를 사용하여 넓은 포인트 세트를 선택하는 최첨단 인터리브 Fixpoint 솔버를 제공합니다. 넓어지는 동안 정밀 손실을 완화하기 위해 Crab은 임계 값으로 넓어 지거나 넓은 넓어지는 것과 같은 인기있는 기술을 구현합니다.
CRAB는 두 가지 서로 다른 교차 분석의 구현을 제공합니다. 재귀 통화를 지원하는 Memoization 간 분석 간 분석 및 상향식 + 상단 다운 분석의 하이브리드. 마지막으로, Crab은 또한 필요한 전제 조건을 계산하고/또는 허위 경보의 수를 줄이는 데 사용할 수있는보다 실험적인 후진 분석을 구현합니다.
Crab은 주류 프로그래밍 언어를 직접 분석하지 않고 대신 Crabir라는 자체 CFG 기반 중간 표현을 분석합니다. Crabir는 3 주소 코드이며 강력하게 입력되었습니다. 크라비르에서 제어 흐름은 비 결정적 GOTO 지침을 통해 정의됩니다. Crabir는 표준 부울 및 산술 작업 외에도 특별한 가정 및 주장 진술을 제공합니다. 전자는 제어 흐름을 개선하는 데 사용될 수 있으며 후자는 사용자 정의 속성을 확인하기 위해 간단한 기계를 제공합니다. 단순한 디자인에도 불구하고 Crabir는 LLVM과 같은 언어를 대표 할만 큼 풍부합니다.
게는 적극적으로 개발 중입니다. 버그를 찾으면 Github 문제를 열어주십시오. 새로운 기능을 갖춘 요청은 매우 환영합니다. 사용 가능한 문서는 위키에서 찾을 수 있습니다. 이 라이브러리를 사용하면이 논문을 인용하십시오.
| 창 | 우분투 | OS x | 적용 범위 |
|---|---|---|---|
| TBD |  | TBD |
모든 테스트를 실행하는 (야간) 사전 구축 된 크랩 버전의 Docker를 사용하여 얻을 수 있습니다.
docker pull seahorn/crab:bionic
docker run -v ` pwd ` :/host -it seahorn/crab:bionic게는 C ++로 작성되었으며 부스트 라이브러리에 의존합니다. 주요 요구 사항은 다음과 같습니다.
-DCRAB_USE_APRON=ON 또는 -DCRAB_USE_ELINA=ON )-DCRAB_USE_PPLITE=ON 인 경우에만)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
게를 설치하려면 다음을 입력하십시오.
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
3. cmake --build . --target install
tests 디렉토리에는 Crabir로 작성된 프로그램을 구축하는 방법에 대한 많은 예가 포함되어 있으며 다양한 분석 및 추상 영역을 사용하여 불변량을 계산합니다. 이 테스트를 컴파일하려면 옵션 -DCRAB_ENABLE_TESTS=ON on the line 2를 추가하십시오.
예를 들어, test1 실행하려면 :
build/test-bin/test1
상자/앞치마/Elina/Pplite 도메인에는 타사 라이브러리가 필요합니다. 해당 도메인에 관심이없는 사용자에게 부담을 피하기 위해 라이브러리 설치는 선택 사항입니다.
상자 도메인을 사용하려면 -DCRAB_USE_LDD=ON 옵션을 추가하십시오.
앞치마 라이브러리 도메인을 사용하려면 -DCRAB_USE_APRON=ON 옵션을 추가하십시오.
Elina 라이브러리 도메인을 사용하려면 -DCRAB_USE_ELINA=ON 옵션을 추가하십시오.
pplite 라이브러리 도메인을 사용하려면 -DCRAB_USE_PPLITE=ON 옵션을 추가하십시오.
중요 : Apron과 Elina는 현재 호환되지 않으므로 -DCRAB_USE_APRON=ON 및 -DCRAB_USE_ELINA=ON 동시에 활성화 할 수 없습니다.
예를 들어, 상자와 앞치마로 게를 설치하려면 다음을 입력하십시오.
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target ldd && cmake ..
4. cmake --build . --target apron && cmake ..
5. cmake --build . --target install
3 번과 4 행은 각각 상자와 앞치마 도메인을 다운로드, 컴파일 및 설치합니다. elina 또는 Pplite를 대신 사용하려면 Elina 또는 pplite 로 4 행의 apron 교체하십시오. 이미 시스템에 이러한 라이브러리를 컴파일하고 설치 한 경우 3 행 및 4 행에서 명령을 건너 뛰고 2 행에서 다음 옵션을 추가하십시오.
-DAPRON_ROOT=$APRON_INSTALL_DIR-DELINA_ROOT=$ELINA_INSTALL_DIR-DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR-DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIRC ++ 애플리케이션에 게를 포함하려면 다음을 수행해야합니다.
$INSTALL_DIR/crab/include 에 위치한 C ++ 헤더 파일을 포함시키고
$INSTALL_DIR/crab/lib 에 설치된 게 라이브러리와 응용 프로그램을 연결하십시오.
상자/Apron/Elina/Pplite로 컴파일하는 경우 $INSTALL_DIR/EXT/include 포함시키고 $INSTALL_DIR/EXT/lib where EXT=apron|elina|ldd|pplite 도 포함해야합니다.
프로젝트가 cmake 사용하는 경우 프로젝트의 CMakeLists.txt 추가하면됩니다.
add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})
그런 다음 실행 파일을 ${CRAB_LIBS} 로 연결하십시오.
프로젝트에서 make 사용하는 경우이 샘플 MakeFile을 읽으십시오.
