progge.rs
1.0.0
Proggers是一個計劃分析遊樂場，適用於一種簡單的命令性語言。
依賴性：
類型檢查和CFG可視化不需要Elina，LLVM和Z3，因此可以將它們變成板條箱功能。請隨時做出貢獻！
安裝先決條件後，您可以使用： cargo install --git https://github.com/skius/progge.rs安裝proggers。
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語言編寫的程序。
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]
沒什麼特別的。允許將結合點遮蓋以前的綁定。
Progge的特殊內置以及Proggers的哪一部分利用它們：
| 內建 | 描述 | 人工智慧 | se | TC | c |
|---|---|---|---|---|---|
unreachable! | 斷言控制流可能永遠不會達到此聲明 | [x] | [x] | ||
testcase! | 指導生成的測試櫃，以達到此陳述 | [x] | [x] | ||
assume!(expr) | 假設給定的布爾表達為真 | [x] | [x] | ||
analyze!(expr) | 指示數值分析打印INT表達式的過度透明度 | [x] | |||
int_arg(expr) | 返回expr-th命令行參數轉換為int | [x] | [x] | ||
print_int(expr) | 打印給定的int to stdout | [x] |
圖例：TC：類型檢查，SE：符號執行，AI：抽象插入，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）計算出不適當的影響，這意味著暗示是“如果符號執行報告路徑（一組輸入值），那麼真實程序也必須遵循該路徑”。
簡而言之，符號執行可以通過給出具體的示例輸入，或者，換句話說，它可以證明某些程序行為的存在。
let陰影/詞彙範圍：Proggers注意到有五個不同的變量稱為x ，正如人們可以在proggers返回的清理上看到的那樣：
// 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 。
prog可以將程序編譯為本機代碼。
$ 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許可證中定義）應為雙重許可，如上所述，沒有任何其他條款或條件。
