seahorn
v0.1.0 Release (SV-COMP'16)
Seahorn은 LLVM 기반 언어를위한 자동화 된 분석 프레임 워크입니다. 이 버전은 LLVM 14에 대해 컴파일합니다.
지원되는 기능 중 일부는 다음과 같습니다
Seahorn은 주로 자동 검증에 대한 연구를 수행하기위한 프레임 워크로 개발되었습니다. 프레임 워크는 다양한 방식으로 구성 할 수있는 많은 구성 요소를 제공합니다. 그러나 "외부인"정적 분석 도구가 아닙니다.
많은 분석 도구와 예에 프레임 워크가 제공됩니다. 우리는 지속적으로 새로운 애플리케이션을 찾고 있으며 새로운 사용자에게 지원을 제공하고 있습니다. 무슨 일이 일어나고 있는지에 대한 자세한 내용은 (드물게 업데이트 된) 블로그를 확인하십시오.
Seahorn은 수정 된 BSD 라이센스에 따라 배포됩니다. 자세한 내용은 License.txt를 참조하십시오.
Seahorn은 sea 라는 Python 스크립트를 제공하여 사용자와 상호 작용합니다. 어설 션으로 주석이 달린 C 프로그램이 주어지면 사용자는 다음을 입력하면됩니다 : sea pf file.c
sea-pf 의 결과는 모든 주장이 유지되면 unsat sat
pf 옵션은 Seahorn에게 file.c llvm 비트 코드로 변환하고, 검증 조건 (VC) 세트를 생성하고 마지막으로 해결하도록 지시합니다. 메인 백엔드 솔버는 스페이서입니다.
pf 명령은 무엇보다도 다음 옵션을 제공합니다.
--show-invars : 답변이 unsat 경우 Computed Invariants를 표시합니다.
--cex=FILE : 답변이 sat 경우 FILE 에 카운터 예를 저장합니다.
-g :보다 추적 가능한 반음에 대한 디버그 정보로 컴파일합니다.
--step=large : 큰 단계 인코딩. 각 전이 관계는 루프가없는 조각에 해당합니다.
--step=small : 작은 단계 인코딩. 각 전이 관계는 기본 블록에 해당합니다.
--track=reg : 모델 (정수) 등록 만 가능합니다.
--track=ptr : 모델 레지스터 및 포인터 (메모리 컨텐츠는 아님)
--track=mem : 스칼라, 포인터 및 메모리 내용을 모델링합니다
--inline : 검증 전에 프로그램을 상인합니다
--crab : 게 Abstract-Interpretation 기반 도구에 의해 생성 된 spacer 에 불변량을 주입합니다. 모든 게 옵션 (접두사 --crab )에 대한 자세한 내용은 여기를 참조하십시오. 옵션 --log=crab 입력하여 게에 의해 어떤 불변량이 추론되는지 알 수 있습니다.
--bmc : BMC 엔진을 사용하십시오.
sea pf 는 여러 명령을 실행하는 파이프 라인입니다. 파이프 라인의 개별 부분도 별도로 실행할 수 있습니다.
sea fe file.c -o file.bc : SEAHORN FRONDEND는 C 프로그램을 혼합 내성 변환을 포함하여 최적화 된 LLVM 비트 코드로 변환합니다.
sea horn file.bc -o file.smt2 : Seahorn은 file.bc 에서 확인 조건을 생성하여 smt -lib v2 형식으로 출력합니다. 사용자는 다음을 추가하여 여러 수준의 정밀도로 다양한 인코딩 스타일 중에서 선택할 수 있습니다.
--step={small,large,fsmall,flarge} small 곳은 작은 단계 인코딩, large 차단 인코딩, fsmall 은 작은 경적 경적 조항을 생성하는 작은 단계 인코딩 (즉, 하나의 술어로 전환 시스템을 생성 함)과 flarge 생성하는 평평한 혼 클라우스를 생성합니다.
--track={reg,ptr,mem} 여기서 reg 는 정수 스칼라, ptr 모델 reg 및 포인터 주소 및 mem 모델 ptr 및 메모리 내용을 모델링합니다.
sea smt file.c -o file.smt2 : SMT -LIB2 형식으로 CHC를 생성합니다. sea fe 와 sea horn 의 별칭입니다. sea pf 명령은 sea smt --prove 의 별칭입니다.
sea clp file.c -o file.clp : CLP 형식으로 CHC를 생성합니다.
sea lfe file.c -o file.ll : 레거시 프론트 엔드 실행
모든 명령을 보려면 sea --help 입력하십시오. 각 개별 명령 CMD (예 : horn )에 대한 옵션을 보려면 sea CMD --help (예 : sea horn --help )를 입력하십시오.
Seahorn은 기본적으로 게를 사용하지 않습니다. 게를 활성화하려면 옵션 --crab sea 명령에 추가하십시오.
초록 통역사는 기본적으로 예방 적이며 구역 도메인을 수치 적 추상 영역으로 사용합니다. 이러한 기본 옵션은 일반 사용자에게 충분해야합니다. 개발자의 경우 다른 추상 도메인을 사용하려면 다음을 수행해야합니다.
cmake 옵션으로 컴파일 -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea 달리십시오 --crab-dom=DOM where DOM 다음과 같습니다.intterm-intboxes : 불법 간격octpk 게 크랩 방학 분석을 사용하려면 옵션으로 sea 운영해야합니다 --crab-inter
기본적으로 추상 통역사는 스칼라 변수 (예 : LLVM 레지스터)에 대한 이유 만 있습니다. 옵션으로 sea 실행하십시오 --crab-track=mem --crab-singleton-aliases=true
게는 대부분 경로에 민감하지 않지만 혼 절전 솔버 인 스페이서는 경로에 민감합니다. 경로 감수성 분석은 더 효율적이지만, 관심의 속성을 입증하기 위해서는 경로 감도가 일반적으로 필요합니다. 이것은 첫 번째 게를 달리는 결정에 동기를 부여합니다 (옵션 --crab ). 그런 다음 생성 된 불변을 스페이서에 전달합니다. 스페이서가 게에 의해 생성 된 불변량을 사용하는 두 가지 방법이 있습니다. sea 옵션 --horn-use-invs=VAL spacer 해당 불변의 사용 방법을 알려줍니다.
VAL 이 bg 와 동일하다면 불변은 spacer 를 유도하는 것을 증명하는 데 도움이됩니다.VAL always 동일하다면 동작은 bg 와 유사하지만 불변량은 spacer 반례를 차단하는 데 도움이됩니다. 기본값은 bg 입니다. 물론 크랩이 프로그램이 안전하다는 것을 증명할 수 있다면 스페이서는 추가 비용으로 발생하지 않습니다.
속성은 주장이라고 가정합니다. Seahorn은 다음 예에 설명 된대로 정적 어설 션 명령 sassert 제공합니다.
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();
int main ( void ) {
int k = 1 ;
int i = 1 ;
int j = 0 ;
int n = nd ();
while ( i < n ) {
j = 0 ;
while ( j < i ) {
k += ( i - j );
j ++ ;
}
i ++ ;
}
sassert ( k >= n );
} 내부적으로 Seahorn은 지정된 오류 함수 __VERIFIER_error() 에 대한 호출로 오류 위치를 인코딩하는 SV-Comm 협약을 따릅니다. Seahorn은 __VERIFIER_error() 도달 할 수 없을 때 unsat 반환하고 프로그램은 안전한 것으로 간주됩니다. Seahorn은 __VERIFIER_error() 도달 할 수 있고 프로그램이 안전하지 않을 때 sat . sassert() 메소드는 seahorn/seahorn.h 에서 정의됩니다.
속성을 입증하거나 반례를 생성하는 것 외에도, 복잡성에 대한 아이디어를 얻기 위해 분석중인 코드를 검사하는 것이 유용합니다. 이를 위해 Seahorn은 sea inspect 제공합니다. 예를 들어, C 프로그램 ex.c 유형이 주어지면 :
sea inspect ex.c --sea-dsa=cs+t --mem-dot
옵션 --sea-dsa=cs+t FMCAD19에 설명 된 새로운 컨텍스트-유형에 민감한 SEA-DSA 분석을 가능하게합니다. 이 명령은 입력 프로그램에서 각 함수 FUN 대한 FUN.mem.dot 파일을 생성합니다. 기본 기능의 그래프를 시각화하려면 Web Graphivz 인터페이스 또는 다음 명령을 사용하십시오.
$ dot -Tpdf main.mem.dot -o main.mem.pdf메모리 그래프에 대한 자세한 내용은 SEADSA 저장소에 있습니다.
sea inspect --help 사용하여 모든 옵션을보십시오. 현재 사용 가능한 옵션은 다음과 같습니다.
sea inspect --profiler 기능 수, 기본 블록, 루프 등을 인쇄합니다.sea inspect --mem-callgraph-dot 인쇄는 Seadsa가 구성한 통화 그래프를 dot 합니다.sea inspect --mem-callgraph-stats 표준 출력을 인쇄합니다.sea inspect --mem-smc-stats SEADSA가 안전하게 입증 될 수있는 메모리 접근 수를 인쇄합니다.Seahorn을 시작하는 가장 쉬운 방법은 Docker 분포를 통한 것입니다.
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly sea Command가 할 수있는 일을 탐색하는 것으로 시작하십시오.
$ sea --help
$ sea pf --help nightly 태그는 매일 자동으로 새로 고침되며 최신 개발 버전이 포함되어 있습니다. 우리는 수동 업데이트가 필요한 다른 모든 태그를 드물게 유지합니다. DockerHub의 날짜를 확인하고 너무 오래된 경우 GitHub에 문제를 기록하십시오.
추가 예제 및 구성 옵션은 블로그에 있습니다. 블로그는 드물게 업데이트됩니다. 특히 옵션 변경, 기능이 단계적으로 폐지되고 새로운 것들이 추가됩니다. 블로그에서 문제를 발견하면 알려주십시오. 최소한 블로그 게시물을 업데이트하여 최신 버전의 코드와 작동하지 않을 것으로 예상됩니다.
다음과 같이 수동으로 설치할 수도 있습니다.
Docker 파일 Dockerfile : docker/seahorn-builder.Dockerfile 의 지침에 따라.
이것이 작동하지 않으면 실행하십시오.
$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *처음 3 개의 명령은 llvm 14를 설치하고 4 번째는 llvm 14에서 잘못 생략 된 libpolly를 설치합니다 (그러나 후속 버전에 포함).
다음으로 위의 Docker 파일의 지침을 따르십시오
이 시점의 정보는 개발자만을위한 것입니다. Seahorn에 기여하고 싶거나, 그 도구를 기반으로 자신의 도구를 만들거나 내부의 작동 방식에 관심이 있으시면 계속 읽으십시오.
Seahorn은 LLVM, Z3 및 부스트가 필요합니다. 라이브러리의 정확한 버전은 계속 변경되지만 Cmake 크래프트는 올바른 버전을 사용할 수 있는지 확인하는 데 사용됩니다.
종속성의 특정 버전을 지정하려면 일반적인 <PackageName>_ROOT 및/또는 <PackageName>_DIR (자세한 내용은 find_package () 참조) Cmake 변수를 사용하십시오.
Seahorn은 다른 저장소 (Seahorn Organization)에 거주하는 여러 구성 요소로 나뉩니다. 빌드 프로세스는 필요에 따라 모든 것을 자동으로 확인합니다. 현재 빌드 지침의 경우 CI 스크립트를 확인하십시오.
이것들은 일반적인 단계입니다. 그것들을 사용 하지 마십시오 . 더 나은 방법으로 읽으십시오.
cd seahorn ; mkdir build ; cd build (빌드 디렉토리는 소스 디렉토리 외부에있을 수도 있습니다.)cmake -DCMAKE_INSTALL_PREFIX=run ../ (설치가 필요합니다! )cmake --build . --target extra && cmake .. (다른 곳에 사는 클론 구성 요소)cmake --build . --target crab && cmake .. (클론 크랩 도서관)cmake --build . --target install ( run 중인 모든 것을 빌드 및 설치)cmake --build . --target test-all (실행 테스트)참고 : 테스트가 작동하려면 설치 대상이 필요합니다!
향상된 개발 경험 :
clang 사용하십시오lld 링커를 사용하십시오compile_commands.json 내보내기 Linux에서는 다음 cmake 구성을 제안합니다.
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run
-DCMAKE_BUILD_TYPE=RelWithDebInfo
-DCMAKE_CXX_COMPILER="clang++-14"
-DCMAKE_C_COMPILER="clang-14"
-DSEA_ENABLE_LLD=ON
-DCMAKE_EXPORT_COMPILE_COMMANDS=1
../
-DZ3_ROOT=<Z3_ROOT>
-DLLVM_DIR=<LLMV_CMAKE_DIR>
-GNinja
$ (cd .. && ln -sf build/compile_commands.json .)
여기서 <Z3_ROOT Z3 바이너리 분포를 포함하는 디렉토리이며, LLMV_CMAKE_DIR LLVMConfig.cmake 포함하는 디렉토리입니다.
CMAKE_BUILD_TYPE 에 대한 기타 법적 옵션은 Debug 및 Coverage 입니다. CMAKE_BUILD_TYPE 는 LLVM 컴파일하는 데 사용되는 것과 호환되어야합니다. 특히 '디버그 ** 모드에서 SeaHorn 컴파일하려면 LLVM의 Debug 빌드가 필요합니다. 이 경로로 이동하기로 결정한 경우 인내심, 디스크 공간 및 시간이 많이 있는지 확인하십시오.
또는 CMAKE 사전 설정을 사용하여 프로젝트를 구성 할 수 있습니다. 이렇게하려면 다음 명령을 실행하십시오.
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > cmake를 구성하려면 <BUILD_TYPE> 이 Debug , RelWithDebInfo 또는 Coverage 중 하나입니다. <PRESET_NAME> 은 사용하려는 사전 설정입니다. 현재 사용 가능한 사전 설정은 jammy 입니다. 이 사전 설정은 Z3가 /opt/z3-4.8.9 에 설치되었으며 Yices는 /opt/yices-2.6.1 에 설치되었다고 가정합니다.
또한 CMAKE Tools 확장을 사용하여 프로젝트를 VS 코드 내에서 구성하고 컴파일 할 수 있습니다.
다른 컴파일 설정을 사용하려고하거나 다른 디렉토리에 Z3 또는 YICES가 설치된 경우 자신의 사전 설정으로 자신의 CMakeUserPresets.json 파일을 만들어야합니다.
-DSEA_ENABLE_LLD=ON 포함하지 마십시오 . 기본 컴파일러는 Clang이므로 명시 적으로 설정할 필요가 없습니다.
Seahorn은 extra 대상을 통해 자동 복제 및 설치되는 여러 구성 요소를 제공합니다. 이 구성 요소는 Seahorn 이외의 다른 프로젝트에서 사용할 수 있습니다.
Sea-dsa : git clone https://github.com/seahorn/sea-dsa.git
sea-dsa 는 새로운 DSA 기반 힙 분석입니다. llvm-dsa 와 달리 sea-dsa 상황에 관계가 없으므로 기능 호출이있는 경우 더 세밀한 힙 파티션을 생성 할 수 있습니다.
조개 : git clone https://github.com/seahorn/crab-llvm.git
clam Seahorn의 나머지 뒷면에 추상 해석 기술을 사용하여 유도 성 불변을 제공합니다.
llvm-seahorn : git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn InstCombine 및 IndVarSimplify llvm 패스와 LLVM 패스의 맞춤형 버전을 제공하여 정의되지 않은 값을 비정상적인 호출로 변환하기위한 LLVM 패스를 제공합니다.
Seahorn은 자체 버전의 Clang과 함께 제공되지 않으며 빌드 디렉토리 ( run/bin ) 또는 경로에서 찾을 것으로 기대합니다. Clang의 버전이 Seahorn (현재 LLVM14)을 컴파일하는 데 사용 된 LLVM 버전과 일치해야합니다. 올바른 버전의 Clang을 제공하는 가장 쉬운 방법은 LLVM.org에서 다운로드하고 어딘가에 공간을 해제하고 run/bin 의 clang 및 clang++ 에 대한 상징적 링크를 만드는 것입니다.
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ 여기서 <CLANG_ROOT> 는 Clang이 포장되지 않은 위치입니다.
테스트 인프라는 여러 Python 패키지에 따라 다릅니다. 이것들은 그들 자체 의존성을 가지고 있습니다. 알아낼 수 없다면 대신 Docker를 사용하십시오.
$ pip install lit OutputCheck networkx pygraphviz gcov 및 lcov 사용하여 Seahorn의 테스트 범위 정보를 생성 할 수 있습니다. 커버리지를 활성화하여 빌드하려면 CMAKE 구성 중에 다른 디렉토리에서 빌드를 실행하고 CMAKE_BUILD_TYPE Coverage 로 설정해야합니다.
test-opsem 대상에 대한 적용 범위 보고서 생성 단계 :
mkdir coverage; cd coverage 생성 및 입력 범위 빌드 디렉토리cmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem 실행 Opsem Tests, 이제 .gcda 및 .gcno 파일을 해당 CMakeFiles 디렉토리에서 작성해야합니다.lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info 원하는 모듈에서 커버리지 데이터를 수집하십시오. clang gcc 대신 컴파일러로 사용되는 경우 bash 스크립트 llvm-gcov.sh 만듭니다. #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh 그런 다음 --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh lcov -c ... 명령에 추가하십시오. 6. 원하는 디렉토리에서 데이터를 추출하고 HTML 보고서를 생성하십시오.
lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report 그런 다음 브라우저에서 coverage_report/index.html 열어 보장 보고서를보십시오.
또한 CI에서 사용하는 스크립트의 scripts/coverage 참조하십시오. 야간 빌드에 대한 적용 범위 보고서는 Codecov에서 확인할 수 있습니다
Seahorn 프로젝트 및 모든 하위 프로젝트의 컴파일 데이터베이스는 -DCMAKE_EXPORT_COMPILE_COMMANDS=ON cmake 를 사용하여 생성됩니다.
Compilation Database 지원으로 코드 인덱싱을 수행하는 쉬운 방법은 compilation_database.json 파일을 기본 프로젝트 디렉토리에 연결하고 편집기와 관련된 지침을 따르는 것입니다.
clangd 와 함께 lsp-ui 사용하십시오. Clion Check Clion-Configuration이있는 원격 워크 플로우에 대한 자세한 안내서.
메인 프레이머 포크를 사용하십시오. 예제 구성을 놓치지 마십시오.
