charon
1.0.0
Patinir, E., 1515-1524, Charon이 Styx [Oil on Wood]를 가로 지르는 풍경 . Museo del Prado, 마드리드. 원천Charon은 Rustc 컴파일러와 프로그램 검증 프로젝트 사이의 인터페이스 역할을합니다. 그 목적은 Rust Crates를 처리하여 프로그램 검증자가 처리하기 쉬운 파일로 변환하는 것입니다. RustC 컴파일러의 사용자 정의 드라이버로 구현됩니다.
Charon은 그리스 신화에서 사망 한 사람들의 영혼을 낳는 노인입니다. 현재의 맥락에서, Charon은 우리가 Rust 프로그램의 세계에서 공식적인 검증의 세계로 갈 수 있도록 허용합니다.
우리는 기부에 개방적 입니다! 기꺼이 기부하려는 경우 우리 자신을 조정할 수 있도록 저희에게 연락하십시오. 이를 위해 Zulip에 가입 할 수 있습니다.
Charon은 miR 코드를 ULLBC (구조화되지 않은 저수준 차용 미적분학)로 변환 한 다음 LLBC로 변환합니다. 두 asts는 Charon에 의해 출력 될 수 있습니다.
ULLBC는 약간 단순화 된 MIR로 가능한 한 많은 중복성을 제거하려고합니다. 예를 들어, 녹 컴파일러에서 오는 상수의 표현을 크게 단순화합니다.
LLBC는 ULLBC로 if ... then ... else ... 우리는 루프로 제어 흐름을 재구성했습니다. 결과적으로, 우리는 miR 문 및 터미네이터를 단일 LLBC 명령문 유형으로 병합합니다. 또한 몇 가지 추가 수정을 수행하며 일부는 다음과 같습니다.
비고 : miR을 ULLBC로 변환하는 대부분의 변환은 마이크로 패스를 통해 LLBC를 구현합니다. 필요에 따라 선택 사항을 선택하고 깃발로 제어 할 수 있습니다. 세부 사항에 대해 자세히 알고 싶다면 src/driver.rs 로 translate 하여 마이크로 패스를 적용합니다.
비고 : (u) llbc의 전체 세부 사항을 알고 싶다면 types.rs , values.rs , expressions.rs , ullbc_ast.rs 및 llbc_ast.rs 를 살펴보십시오.
추출 된 AST는 .ullbc 및 .llbc 파일 (JSON 형식 사용)에서 직렬화됩니다. 하나의 파일로 전체 상자를 추출합니다.
charon : Rust 구현.charon-ml : ML 라이브러리. OCAML에서 AST를 검색하고 조작 할 수있는 유틸리티를 제공합니다 (사막화, 인쇄 등).tests 및 tests-polonius : 테스트 파일 디렉토리. tests-polonius 에는 Polonius 차용 체커가 필요한 코드가 포함되어 있습니다. 먼저 rustup 설치해야합니다.
Charon이화물을 사용하여 설정되면 Rustup은 프로젝트를 구축 할 때 적절한 패키지를 자동으로 다운로드하여 설치합니다. Rust Project ( ./charon ) 만 빌드하려면 최상위 디렉토리에서 make build-charon-rust .
ML 라이브러리 ( ./charon-ml )를 구축하려면 OCAML 및 적절한 종속성을 설치해야합니다.
해당 지침을 따르고 OPAM을 설치하는 것이 좋습니다 (동일한 지침).
Charon-ML의 경우 OCAML 4.13.1 : opam switch create 4.13.1+options
종속성은 다음 명령으로 설치할 수 있습니다.
opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind
그런 다음 make build-charon-ml 실행하여 ML 라이브러리를 구축하거나 전체 프로젝트 (Rust and OCAML)를 구축 make 위해 실행할 수 있습니다. 마지막으로 make test 로 테스트를 실행할 수 있습니다.
또는 Nix를 사용하고 nix develop (또는 https://direnv.net/ 및 direnv allow )을 사용할 수 있으며 모든 종속성을 사용할 수 있어야합니다.
Rust Documentation에 온라인으로 액세스 할 수 있습니다.
문서를 로컬로 생성하기 위해 make 실행할 수도 있습니다. doc-rust.html (Rust Project) 및 doc-ml.html (ML 라이브러리)에서 액세스 할 수있는 문서를 생성합니다.
Charon을 운영하려면 cargo build 로 상자를 건설하려는 것처럼 컴파일하려는 상자 내 에서 Charon Binary를 실행해야합니다. Charon 실행 파일은 bin/charon 에 있습니다.
Charon은 상자와 그 종속성을 구축 한 다음 AST를 추출합니다. Charon은 행동을 조정하기 위해 다양한 옵션과 플래그를 제공합니다. --help 로 자세한 문서를 표시 할 수 있습니다. 특히, 당신은 --print-llbc 로 Charon에서 생성 한 LLBC를 인쇄 할 수 있습니다.
프로젝트의 루트에 Charon.toml 파일이있는 경우 Charon도 옵션을 가져갑니다. 파일은 --print-llbc 와 같은 입력/출력과 관련된 옵션을 제외하고 CLI 인터페이스에서 동일한 옵션을 지원합니다. Charon.toml 예제 :
[ charon ]
extract_opaque_bodies = true
[ rustc ]
flags = [ " --cfg " , " abc " ] 비고 : Charon은 Nigthly Rust (Rustc 드라이버를 구현하기위한 요구 사항)로 편집되어 있기 때문에 밤마다 Rust로 상자를 건설 할 것입니다. rust-toolchain.template 에서 Charon에 고정 된 야간 버전을 찾을 수 있습니다.
