progge.rs
1.0.0
Proggers es un patio de juegos de análisis de programas para un lenguaje simple e imperativo.
Dependencias:
Ni Elina ni LLVM ni Z3 son necesarios para la verificación de tipo y la visualización de CFG, por lo tanto, podrían convertirse en una función de caja. ¡Por favor, no dude en contribuir!
Una vez que se instalan los requisitos previos, puede instalar Proggers con: 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
Los proggers pueden analizar programas escritos en el lenguaje 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 especial. Los vínculos de alquiler están permitidos a las ataduras anteriores.
Los empotrados especiales de Progge y qué parte de Proggers los hace uso:
| Incorporado | Descripción | AI | SE | TC | do |
|---|---|---|---|---|---|
unreachable! | Afirma que el flujo de control nunca puede llegar a esta declaración | [incógnita] | [incógnita] | ||
testcase! | Instruye la generación de casos de prueba que llegan a esta declaración | [incógnita] | [incógnita] | ||
assume!(expr) | Asume la expresión de bool dada como verdadera | [incógnita] | [incógnita] | ||
analyze!(expr) | Instruye el análisis numérico para imprimir una sobrecargación excesiva de la expresión int | [incógnita] | |||
int_arg(expr) | Devuelve el argumento de línea de comandos expr-th convertido a un int | [incógnita] | [incógnita] | ||
print_int(expr) | Imprime el int to stdout dado | [incógnita] |
Leyenda : TC: Comprobación de tipo, SE: Ejecución simbólica, IA: Interpertación abstracta, C: Compilación
Proggers puede analizar a continuación el programa y encontrar posibles valores de retorno, como se puede ver desde la parte inferior derecha " z: [-1,0] " que indica que z puede ser -1 o 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 también admite algunas directivas que utilizan los resultados de interpretación abstracta.
¡analizar! : Explícitamente imprime valores posibles para una expresión dada. Por ejemplo, ejecutar proggers --typecheck --analyze analyzer-examples/analyze_loop.progge da la siguiente retroalimentación (la imagen no muestra la salida completa):
Tenga en cuenta que los valores posibles devueltos para una expresión son una sobrecargación excesiva .
Inconocador! : Afirma que una declaración es inalcanzable. Por ejemplo, ejecutar proggers --typecheck --analyze analyzer-examples/unreachable.progge ofrece los siguientes comentarios:
Tenga en cuenta que, nuevamente, el análisis de inalcanzabilidad utilizando una interpretación abstracta calcula una sobreapasa excesiva , es decir, puede dar falsos positivos ( unreachable! advierta sobre las declaraciones accesibles inalcanzables unreachable! Vea la ejecución simbólica para declaraciones garantizadas sobre accesibilidad.
La interpretación abstracta (Wikipedia) calcula una sobrecargación excesiva, lo que significa que todos los comportamientos del programa posibles (quizás más, pero no menos) son capturados por él, es decir, la implicación es "si el programa real exhibe un comportamiento, entonces ese comportamiento está contenido en la sobrecargación de la interpretación abstracta".
En resumen, la interpretación abstracta puede demostrar la ausencia de comportamientos del programa no deseados, que podrían ser excepciones de índice por EG-fuera de los límites (TODO), ¡ejecución de unreachable! declaraciones o llamadas de función cuyos argumentos no satisfacen las condiciones previas de la función.
¡Caso de prueba! : Genera tareas de prueba (es decir, valores de argumento para la función) que alcanzan la declaración. Por ejemplo, ejecutar proggers --typecheck --symex analyzer-examples/symex_arr_hard.progge da:
Nota: La generación de pruebas también funciona para llamadas a 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 }
Inconocador! : Además, si es un unreachable! no es realmente inalcanzable, la ejecución simbólica arrojará un error y dará una entrada de muestra que llegue a la declaración. Por ejemplo, ejecutar proggers --typecheck --symex analyzer-examples/unreachable.progge da: 
La ejecución simbólica (Wikipedia) calcula una subocreximación, lo que significa que la implicación es "si la ejecución simbólica informa una ruta (conjunto de valores de entrada), entonces el programa real también debe seguir esa ruta".
En resumen, la ejecución simbólica puede demostrar la accesibilidad de las declaraciones al dar entradas de ejemplo concretas o, en otras palabras, puede demostrar la presencia de ciertos comportamientos del programa.
let SHOWING/LEXICAL ESCOPES: Proggers se da cuenta de que hay cinco variables distintas llamadas x , como se puede ver en el AST limpiado que los Proggers regresan:
// 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 ;
}Además, Proggers puede dar buenos mensajes de error (gracias a Ariadne):
// Source
fn foo ( ) -> int {
return true ;
} 
Consulte analyzer-examples/tc_bad para obtener más ejemplos.
Los proggers pueden compilar programas en 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
24Con licencia bajo cualquiera de
a tu opción.
A menos que declare explícitamente lo contrario, cualquier contribución presentada intencionalmente para su inclusión en el trabajo por usted, como se define en la licencia Apache-2.0, se debe tener doble licencia como se indicó anteriormente, sin ningún término o condiciones adicionales.
