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许可证中定义）应为双重许可，如上所述，没有任何其他条款或条件。
