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言語で記述されたプログラムを分析できます。
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の特別なビルドインとProggersのどの部分がそれらを利用しています。
| 組み込み | 説明 | ai | se | TC | c |
|---|---|---|---|---|---|
unreachable! | コントロールフローがこの声明に決して到達しない可能性があると主張します | [x] | [x] | ||
testcase! | このステートメントに到達するテストケースの生成に指示します | [x] | [x] | ||
assume!(expr) | 与えられたブール式を真であると仮定します | [x] | [x] | ||
analyze!(expr) | 数値分析に、INT式の過剰近接を印刷するように指示します | [x] | |||
int_arg(expr) | intに変換されたexpr-thコマンドライン引数を返します | [x] | [x] | ||
print_int(expr) | 指定されたINTを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!引数が関数の前提条件を満たさないステートメント、または関数呼び出し。
テストケース！ ：ステートメントに到達するテストケース（関数の引数値）を生成します。たとえば、 proggers --typecheck --symex analyzer-examples/symex_arr_hard.progge次のようになります。
注：testcaseの生成は、 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次のようになります。 
Symbolic Execution（Wikipedia）は、承認不足を計算します。つまり、意味は「シンボリック実行がパス（入力値のセット）を報告する場合、実際のプログラムもそのパスに従わなければならない」ことを意味します。
要するに、象徴的な実行は、具体的な例の入力を与えることにより、ステートメントの到達可能性を証明できます。つまり、特定のプログラム行動の存在を証明できます。
シャドウイング/語彙スコープをlet ：Progersは、クリーンアップされたASTでProggersが返すことを見ることができるように、 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はプログラムをネイティブコードにコンパイルできます。
$ 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ライセンスで定義されているように、お客様による仕事に含めるために意図的に提出された貢献は、追加の条件なしで、上記のように二重ライセンスを取得するものとします。
