lart
1.0.0
LART = LLVM 추상화 및 정제 도구. 이 도구의 목표는 다양한 프로그램 추상화를 구현하는 LLVM-to-LLVM 변환을 제공하는 것입니다. 명령어 세트와 관련하여 결과 프로그램은 실행 및 분석 할 수있는 정상적인 구체적인 LLVM 프로그램입니다. (Fragment) 프로그램을 통해 사실상의 추상화에 대한 추가 정보는 특수 LLVM 고유 함수 및 LLVM 메타 데이터 노드를 사용하여 삽입됩니다. Lart는 온 디스크 비트 코드 파일을 처리하는 독립형 도구와 복잡한 LLVM 기반 도구에 통합 될 수있는 프레임 워크를 제공합니다. LART의 주요 동기는 LLVM 기반 모델 검사기 및 기타 분석 도구에 "전처리 기"를 제공하여 분석의 건전성을 손상시키지 않고 문제 크기를 줄임으로써 작업을 단순화하는 것입니다. Lart에 의해 구현 된 추상화는 일반적으로 추상화의 "부분"이 너무 거칠지 않은 특정 지침에 기초하여 정제 될 수 있습니다 (너무 거칠기 때문에 추상적 인 추상화는 후속 분석에 가짜 오류가 발생하지만 원래 프로그램에는 존재하지 않습니다).
전체 운동의 목적은 LLVM 비트 코드에서 정보를 추상화하여 후속 분석이보다 효율적으로 만들어지는 것입니다 (일부 정밀도로). 이를 위해, 우리는 주로 LLVM 프로그램에서 비 결정적 선택을 인코딩 할 수 있어야하며, 이는 특수 목적 기능 (LLVM Intrinsics와 유사)을 통해 간단히 수행 할 수 있습니다. 이 함수는 @lart.choice 라는 이름으로, 인수로 한 쌍의 경계를 취하고 비 결정적으로 해당 경계 사이에있는 값을 반환합니다.
LLVM 시맨틱으로 의이 확장은 다운 스트림 도구로 인식해야합니다. 이것은 또한 표준 LLVM 비트 코드에서 유일하게 중요한 편차입니다. 많은 분석 도구는 이미 내부적 또는 외부 인터페이스를 사용하여 유사한 메커니즘을 구현합니다. @lart.choice 를 지원하지 않고 도구를 적응하는 것은 일반적으로 매우 간단합니다.
Lart가 제공하는 다른 특수 목적 기능, 즉 @lart.meta.* 가족이 있지만 이러한 지침에 관한 한, 대부분의 도구는 기존 @llvm.dbg.* 와 마찬가지로 그들의 존재를 안전하게 무시할 수 있습니다. LART가 추상화를 개선하기 위해 LART가 호출되는 경우 프로그램 변환은 해당 호출을 유지해야 할 것으로 예상됩니다 (LART가 제공 한 각 추상화에는 해당 정제 절차가 제공되며, 이는 종종 @lart.meta 호출을 찾아야합니다).
대부분의 전통적인 추상화 엔진은 통역사로서 작동하지만 추상화는 프로그램에 "컴파일"될 수 있습니다. 상징적으로 지시를 해석하는 대신, 상징적 지침을 편집 할 수 있습니다. 술어 추상화의 경우, 결과 비트 코드는 콘크리트 변수 대신 사례 평가를 직접 조작하고 사용합니다. 위에서 설명한 바와 같이, 중요한 차이점은 비트 코드가 비 결정적 선택을해야한다는 것입니다. 일부 사전 대상은 불확실한 평가를 가질 수 있기 때문입니다 (참과 거짓). 일부 변수는 완전히 추상화 될 수 있으며, 그러한 변수에 대한 모든 테스트는 예와 아니오 답변을 모두 산출합니다.
당분간 ./devcontainer/Dockerfile 에서 설정을 사용하거나 반복하십시오.
그런 다음 사용하십시오 :
./scripts/build.sh
./build/bin/lartcc <domain> <compiler arguments> in.c
opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc
lit -v build/test
참고 : build/lartcc/lartcc 부 외투 허가가 있어야합니다.
