progge.rs
1.0.0
Proggers는 단순하고 명령적인 언어를위한 프로그램 분석 놀이터입니다.
종속성 :
Elina 또는 LLVM 또는 Z3은 유형 검사 및 CFG 시각화에 필요하지 않으므로 상자 기능으로 바뀔 수 있습니다. 자유롭게 기여 해주세요!
전제 조건이 설치되면 : cargo install --git https://github.com/skius/progge.rs 사용하여 프로그램을 설치할 수 있습니다.
proggers
<sourcefile> # the sourcefile to analyze
--cfg # visualize the control flow graph
--typecheck # type-check the source
--analyze # shorthand for --symex --ai
--symex # run symbolic execution
--ai # run abstract interpretation
--ast # print the abstract syntax tree
-o <outputfile> # compile source into the executable <outputfile>
--verbose # print LLVM IR when compiling
Proggers는 Progge Language로 작성된 프로그램을 분석 할 수 있습니다.
program: funcdef*
funcdef: fn var((var: type,)*) -> type { block }
block: stmt;*
stmt: let var = expr
| var = expr
| expr[expr] = expr
| var(expr,*)
| testcase!
| unreachable!
| if expr { block } [ else { block } ]
| while expr { block }
| return [expr]
expr: var
| int
| bool
| expr binop expr
| unop expr
| var(expr,*)
| [expr,*]
| [expr; expr]
binop: + | - | * | / | % | < | <= | > | >= | == | !=
unop: - | !
var: [A-Za-z_][A-Za-z0-9_]*
type: int | bool | [type]
특별한 것은 없습니다. Let-Bindings는 이전 바인딩을 어둡게합니다.
Progge의 특별한 내장과 프로그래거의 일부를 사용합니다.
| 내장 | 설명 | 일체 포함 | SE | TC | 기음 |
|---|---|---|---|---|---|
unreachable! | 제어 흐름 이이 진술에 도달 할 수 없다고 주장합니다 | [엑스] | [엑스] | ||
testcase! | 이 진술에 도달하는 테스트 케이스 생성을 지시합니다 | [엑스] | [엑스] | ||
assume!(expr) | 주어진 bool 표현이 참으로 가정합니다 | [엑스] | [엑스] | ||
analyze!(expr) | int 표현의 과다 발사를 인쇄하도록 수치 분석을 지시합니다. | [엑스] | |||
int_arg(expr) | int로 변환 된 expr-th 명령 줄 인수를 반환합니다. | [엑스] | [엑스] | ||
print_int(expr) | 주어진 int를 stdout으로 인쇄합니다 | [엑스] |
범례 : TC : Type-Checking, SE : Symbolic Execution, AI : Abstract Interpertation, C : 컴파일
Proggers는 아래 프로그램을 분석하고 가능한 반환 값을 찾을 수 있습니다. 오른쪽 하단에서 볼 수 있듯이 " z: [-1,0] " z -1 또는 0 일 수 있습니다.
fn analyze ( x : int , y : int ) -> int {
if x < y {
while x < y {
x = x + 1 ;
y = y - 1 ;
}
let z = y - x ;
return z ;
}
return - 2 ;
} 
Proggers는 또한 추상 해석 결과를 사용하는 몇 가지 지침을 지원합니다.
분석하다! : 주어진 표현식에 대한 가능한 값을 명시 적으로 인쇄합니다. 예를 들어, 실행 proggers --typecheck --analyze analyzer-examples/analyze_loop.progge 다음과 같은 피드백을 제공합니다 (이미지는 전체 출력이 표시되지 않음).
발현에 대한 반환 가능한 값은 과도한 용사 입니다.
도달 할 수없는! : 진술은 도달 할 수 없다고 주장합니다. 예를 들어, 실행 proggers --typecheck --analyze analyzer-examples/unreachable.progge 다음과 같은 피드백을 제공합니다.
다시 말하지만, 추상적 해석을 사용한 비교 가능성 분석은 과다 발사를 계산합니다. 즉, 잘못된 양성을 제공 할 수 있습니다 (실제로 도달 할 수없는 도달 할 수없는 진술에 대해 경고 할 unreachable! unreachable! 도달 할 수없는 진술). 도달 가능성에 대한 보장 된 진술은 상징적 실행을 참조하십시오.
초록 해석 (Wikipedia)은 과도한 용사를 계산합니다. 즉, 가능한 모든 프로그램 행동 (아마도 더 많을 수도 있지만)은 그것에 의해 포착된다는 것을 의미합니다. 즉, 실제 프로그램이 행동을 보인다면, 그 행동은 초록 해석의 과도한 감사에 포함되어 있습니다.
요컨대, 추상적 해석은 원치 않는 프로그램 행동이 없다는 것을 증명할 수 있으며, 이는 예외적으로 인덱스가없는 예외 (TODO), unreachable! 인수가 기능의 전제 조건을 충족시키지 않는 진술 또는 함수 호출.
테스트 케이스! : 진술에 도달하는 TestCases (예 : 함수에 대한 인수 값)를 생성합니다. 예를 들어, 실행 proggers --typecheck --symex analyzer-examples/symex_arr_hard.progge 과 같습니다.
참고 : TestCase Generation은 int_arg 에 대한 통화에도 효과가 있습니다. symex_blackbox.progge 참조
analyzer-examples/symex_arr_hard.progge:7:13: sample inputs reaching this statement:
{ x = 1, y = 0 }
{ x = 0, y = 1 }
{ x = 0, y = 2 }
{ x = 2, y = 1 }
{ x = 1, y = 2 }
도달 할 수없는! : 또한 주어진 unreachable! 실제로 도달 할 수없는 것이 아니며, 상징적 실행은 오류를 던지고 명령문에 도달하는 샘플 입력을 제공합니다. 예를 들어, 실행 proggers --typecheck --symex analyzer-examples/unreachable.progge 제공합니다. 
상징적 실행 (Wikipedia)은 언더러스산화를 계산합니다. 즉, 상징적 실행이 경로를보고하는 경우 (입력 값 세트), 실제 프로그램도 해당 경로를 따라야한다 "는 의미입니다.
요컨대, 상징적 실행은 구체적인 예제 입력을 제공함으로써 진술의 도달 가능성을 입증 할 수 있습니다. 즉, 특정 프로그램 행동의 존재를 증명할 수 있습니다.
Shadowing/Lexical Scopes를 let : Proggers는 Proggers가 반환하는 정리 된 AST에서 볼 수 있듯이 x 라는 5 가지 변수가 있음을 알 수 있습니다.
// Original source code
fn analyze ( x : int ) -> int {
x = 0 ;
let x_2 = 10 ;
let x = x ;
let x = x + 1 ;
x_2 = 5 ;
if true {
let x = 2 ;
x = 3 ;
} else {
let x = 4 ;
}
// returns 1
return x ;
}
// Type-checked AST
fn analyze ( x_1 : int ) {
x_1 = 0 ;
let x_2_1 = 10 ;
let x_2 = x_1 ;
let x_3 = ( x_2 + 1 ) ;
x_2_1 = 5 ;
if true {
let x_4 = 2 ;
x_4 = 3 ;
} else {
let x_5 = 4 ;
}
return x_3 ;
}또한 Proggers는 멋진 오류 메시지를 제공 할 수 있습니다 (Ariadne 덕분에).
// Source
fn foo ( ) -> int {
return true ;
} 
더 많은 예는 analyzer-examples/tc_bad 참조하십시오.
프로그램은 프로그램을 기본 코드로 컴파일 할 수 있습니다.
$ proggers codegen-examples/factorial.progge -t -o factorial
$ ./factorial 4
24
0
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24어느 쪽에도 라이센스가 부여되었습니다
귀하의 선택에.
귀하가 명시 적으로 명시 적으로 명시하지 않는 한, Apache-2.0 라이센스에 정의 된대로 귀하의 작업에 포함되도록 의도적으로 제출 된 기부금은 추가 이용 약관이나 조건없이 위와 같이 이중 라이센스를받습니다.
