progge.rs
1.0.0
Proggers é um playground de análise de programa para uma linguagem simples e imperativa.
Dependências:
Nem Elina nem LLVM nem Z3 são necessários para a verificação do tipo e a visualização do CFG, portanto, eles podem ser transformados em um recurso de caixa. Por favor, fique à vontade para contribuir!
Depois que os pré -requisitos forem instalados, você pode instalar os proggers com: 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 podem analisar programas escritos no idioma 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]
Nada de especial. As ligações de letra são autorizadas a sombrear as ligações anteriores.
Build-ins especial de Progge e que parte dos Proggers utiliza-os:
| Embutido | Descrição | Ai | SE | Tc | C |
|---|---|---|---|---|---|
unreachable! | Afirma que o fluxo de controle pode nunca atingir esta declaração | [x] | [x] | ||
testcase! | Instrui a geração de casas de teste que atingem esta declaração | [x] | [x] | ||
assume!(expr) | Assume a expressão de bool dada como verdadeira | [x] | [x] | ||
analyze!(expr) | Instrui a análise numérica para imprimir uma abrangência excessiva da expressão int | [x] | |||
int_arg(expr) | Retorna o argumento da linha de comando expr-th convertido em um int | [x] | [x] | ||
print_int(expr) | Imprime o Int dado para stdout | [x] |
Legenda : TC: Verificação do tipo, SE: Execução simbólica, AI: interpertação abstrata, C: Compilação
Proggers é capaz de analisar o programa abaixo e encontrar possíveis valores de retorno, como pode -se ver no canto inferior direito " z: [-1,0] ", indicando que z pode ser -1 ou 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 ;
} 
Os Proggers também suportam algumas diretivas que usam os resultados da interpretação abstrata.
analisar! : Imprime explicitamente os valores possíveis para uma determinada expressão. Por exemplo, Running proggers --typecheck --analyze analyzer-examples/analyze_loop.progge fornece o seguinte feedback (a imagem não mostra a saída completa):
Observe que os possíveis valores retornados para uma expressão são uma abrangência excessiva .
inacessível! : Afirma que uma declaração é inacessível. Por exemplo, Running proggers --typecheck --analyze analyzer-examples/unreachable.progge fornece o seguinte feedback:
Observe que, novamente, a análise inacreditada usando interpretação abstrata calcula uma abrangência excessiva - ou seja, pode dar falsos unreachable! (alertar sobre as declarações inacessíveis unreachable! Consulte Execução simbólica para declarações garantidas sobre a acessibilidade.
A interpretação abstrata (Wikipedia) calcula uma abrangência excessiva, o que significa que todos os comportamentos possíveis do programa (talvez mais, mas não menos) são capturados por ela, ou seja, a implicação é "se o programa real exibir um comportamento, então esse comportamento é contido na abrangência abstrata".
Em resumo, a interpretação abstrata pode provar ausência de comportamentos de programa indesejados, que podem ser exceções de índices de índices (TODO), execução de unreachable! Declarações, ou chamadas de função cujos argumentos não satisfazem as pré -condições da função.
teste! : Gera testcases (ou seja, valores de argumento para a função) que atingem a instrução. Por exemplo, Running proggers --typecheck --symex analyzer-examples/symex_arr_hard.progge fornece:
NOTA: A geração de testes também funciona para chamadas para int_arg - consulte 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 }
inacessível! : Além disso, se um dado unreachable! Na verdade, não é inacessível, a execução simbólica apresentará um erro e fornecerá uma entrada de amostra que atinge a instrução. Por exemplo, executar proggers --typecheck --symex analyzer-examples/unreachable.progge fornece: 
A execução simbólica (Wikipedia) calcula uma subestimação, o que significa que a implicação é "se a execução simbólica relatar um caminho (conjunto de valores de entrada), o programa real também deve seguir esse caminho".
Em suma, a execução simbólica pode provar a acessibilidade das declarações, dando informações concretas ou, em outras palavras, pode provar a presença de certos comportamentos do programa.
let Shadowing/Lexical Scopes: Proggers percebe que existem cinco variáveis distintas chamadas x , como se pode ver na AST limpa que os proggers retornam:
// 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 ;
}Além disso, o Proggers é capaz de dar boas mensagens de erro (graças a Ariadne):
// Source
fn foo ( ) -> int {
return true ;
} 
Consulte analyzer-examples/tc_bad para obter mais exemplos.
Proggers podem compilar programas para o código nativo.
$ 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
24Licenciado sob qualquer um de
por sua opção.
A menos que você declare explicitamente o contrário, qualquer contribuição enviada intencionalmente para inclusão no trabalho por você, conforme definido na licença Apache-2.0, será licenciado como acima, sem termos ou condições adicionais.
