2012-12-21 7 views
3

IR에 일부 코드가 있습니다.이 코드는 이미 SSA 형식입니다. 이제이 코드를 SMT 공식으로 변환하고 Z3으로 피드하여 검증을 시도합니다. 몇 가지 질문이 있습니다.IR을 Z3 공식으로 변환 하시겠습니까?

  1. SSA IR을 SMT 공식으로 변환하는 방법에 대한 기술 자료가 있습니까? 나는 아무 쓸데없는 주위를 수색했다.

  2. 이러한 계산 지침의 경우 Z3 수식으로 변환하는 데 많은 문제가 없습니다. 그러나, 나는 무조건 조건부 분기 명령으로 여전히 고심하고있다. 이 지침을 Z3 공식으로 변환하는 방법에 대한 제안이 있으십니까?

감사합니다.

답변

7

나는이 두 가지 주요 그룹의 SMT 기반 프로그램 검증 도구를 분할하는 것이 공정하다고 생각 :

  • Fuzzers 및 버그 측정기. 이러한 도구는 본질적으로 프로그램의 하나의 실행 경로를 SMT 공식으로 인코딩합니다. 이러한 도구는 SMT를 사용하여 특정 실행 경로가 실행 가능한지 여부를 확인합니다. 예 또는 도구는 Pex, EXE, Sage입니다. 귀하의 질문에 따라, 그것은 이미 SMT로 한 경로를 인코딩하는 방법을 알고있는 것 같습니다.

  • 확장 정적 검사기 및 확인 컴파일러. 이러한 도구는 일반적으로 프로그램을 중간 형식으로 축소합니다. 그런 다음 여러 검증 조건 (VC)이 생성되어 SMT 솔버로 전송됩니다. 대부분의 사람들은 전체 프로그램을 단일 SMT 문제로 확인하는 데 너무 비싸기 때문에 모듈 식 검증을 시도합니다. Boogie-PL은 매우 대중적인 중간 형식입니다. IR을 Boogie-PL에 매핑하면 Boogie을 사용하여 SMT 형식의 VC를 생성 할 수 있습니다. "Weakest-Precondition of Unstructured Programs"문서는 Boogie-PL이 수식에 어떻게 인코딩되는지 설명합니다. Boogie는 오픈 소스이며 코드는 매우 읽기 쉽습니다. 따라서 코드를 탐색하여 세부 정보를 명확히 할 수도 있습니다. Rustan Leino에는 Boogie VC를 수식에 인코딩하는 방법을 설명하는 슬라이드가 있습니다. 기타 관련 프로젝트는 ESC/Java 2, Why3, VeriFast입니다.

편집 (처리 루프) : 단지 주어진 시간에 그들을 전개 루프를 처리하기위한 가장 간단한 방법. 이를 수행 할 때 검증 도구는 모든 가능한 경로를 분석하는 것을 포기하기 때문에 "버그 발견 자"가됩니다. 도구 (예 : ESC/Java, Why3, VeriFast)에서 loop invariants이 사용됩니다. Rustan은 루프 불변량에 대해 좋은 video and lectures notes을 가지고 있습니다. 루프 불변량은 사용자에 의해 제공되거나 자동으로 계산 될 수 있습니다. "루프 불변 합성"에 관한 많은 논문이 있습니다.

루프 불변 예 :이 Why3 verification example의 함수 duplet.

또 다른 가능성은 muZ으로 IR을 인코딩하는 것입니다. muZ는 Z3에서 사용할 수있는 고정 소수점 엔진입니다. 이 방법에서는 루프를 직접 인코딩 할 수 있으므로 (muZ 페이지의 아티클 참조) 루프 불변 조건을 제공 할 필요가 없습니다. 012Z그러나 muZ와 같은 엔진은 최첨단 SMT 솔버로 성숙되지 않았습니다.

+0

항상 그렇듯이 답은 굉장합니다, 레오!그러나 나는 아직도 질문을 가지고있다. 나는 언급 된 논문 "구조화되지 않은 프로그램의 가장 약한 전제 조건"을 읽고 수식을 생성하기 전에 루프가없는 코드를 갖는 것이 왜 필요한지 이해하지 못한다. (저자는 루프의 모든 뒷 가장자리를 제거했다). 이 문제는 IR 코드에 조건부 및 무조건 분기가 있기 때문에 걱정 스럽지만 여전히 어떻게 처리해야하는지 잘 모릅니다. 고마워, 레오! – user311703

+0

루프에 추가 노트를 추가했습니다. –