progge.rs
1.0.0
Proggers ist ein Programmanalyse -Spielplatz für eine einfache, imperative Sprache.
Abhängigkeiten:
Weder Elina noch LLVM oder Z3 sind für die Typ-Überprüfung und die CFG-Visualisierung erforderlich, weshalb sie in eine Kistenfunktion verwandelt werden konnten. Bitte zögern Sie nicht, einen Beitrag zu leisten!
Sobald die Voraussetzungen installiert sind, können Sie Progger mit: 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
Progger können Programme in der Progge -Sprache analysieren.
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]
Nichts Besonderes. Die LaD-Bindungen dürfen frühere Bindungen beschatten.
Progge's spezielle Einbauten und welcher Teil von Proggers verwenden sie:
| Eingebaut | Beschreibung | Ai | Se | TC | C |
|---|---|---|---|---|---|
unreachable! | Behauptet, dass der Kontrollfluss diese Aussage niemals erreichen könnte | [X] | [X] | ||
testcase! | Weisen die Erzeugung von Tests, die diese Aussage erreichen | [X] | [X] | ||
assume!(expr) | Nimmt den gegebenen BOOL -Ausdruck als wahr an | [X] | [X] | ||
analyze!(expr) | Weist die numerische Analyse an, eine Überprüfung des INT-Expression zu drucken | [X] | |||
int_arg(expr) | Gibt das Ausdruck der Befehlszeilenargument zurück, das in ein int konvertiert ist | [X] | [X] | ||
print_int(expr) | Druckt die gegebene int an stdout | [X] |
Legende : TC: Typ Überprüfung, SE: Symbolische Ausführung, AI: Abstract Interpertation, C: Zusammenstellung
Proggers ist in der Lage z: [-1,0] z folgende Programm zu analysieren und mögliche Rückgabewerte zu finden, wie man von unten 0 sehen kann -1
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 unterstützt auch einige Richtlinien, die die abstrakten Interpretationsergebnisse nutzen.
analysieren! : Drucken Sie ausdrücklich mögliche Werte für einen bestimmten Ausdruck aus. Beispielsweise läuft das Ausführen proggers --typecheck --analyze analyzer-examples/analyze_loop.progge ergibt das folgende Feedback (Bild zeigt nicht die vollständige Ausgabe an):
Beachten Sie, dass die zurückgegebenen möglichen Werte für einen Ausdruck eine Überprüfung sind.
unerreichbar! : Behauptet, dass eine Aussage nicht erreichbar ist. Zum Beispiel leiten proggers --typecheck --analyze analyzer-examples/unreachable.progge
Beachten Sie erneut, dass die Nicht -Erreger -Analyse unter Verwendung einer abstrakten Interpretation eine Überprüfung berechnet - dh sie kann falsch positive Positive geben (warnen vor erreichbaren unreachable! Aussagen, die in Wahrheit nicht erreichbar sind), aber möglicherweise niemals falsche Negative (wenn es keine Warnungen vor einem nicht erreichbaren Warnungen gibt unreachable! In der symbolischen Ausführung finden Sie garantierte Aussagen zur Erreichbarkeit.
Abstract Interpretation (Wikipedia) berechnet eine Überprüfung, was bedeutet, dass alle möglichen Programmverhalten (möglicherweise mehr, aber nicht weniger) von dieser erfasst werden. Die Implikation ist "wenn das reale Programm ein Verhalten aufweist, dann wird dieses Verhalten in der Überprüfung der abstrakten Interpretation enthalten".
Kurz gesagt, eine abstrakte Interpretation kann das Fehlen unerwünschter Programmverhalten erweisen, bei dem es sich um eine Indexausnahme (TODO) auswirkt, die unreachable! Aussagen oder Funktionsaufrufe, deren Argumente die Voraussetzungen der Funktion nicht erfüllen.
TestCase! : Generiert Tests (dh Argumentwerte für die Funktion), die die Anweisung erreichen. Zum Beispiel läuft proggers --typecheck --symex analyzer-examples/symex_arr_hard.progge gibt:
Hinweis: Die TestCase -Generation funktioniert auch für Anrufe an int_arg - siehe 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 }
unerreichbar! : Außerdem, wenn eine gegebene unreachable! ist nicht wirklich unerreichbar, symbolische Ausführung wirft einen Fehler und gibt eine Beispieleingabe an, die die Anweisung erreicht. Zum Beispiel läuft proggers --typecheck --symex analyzer-examples/unreachable.progge ergibt: 
Die symbolische Ausführung (Wikipedia) berechnet eine Unterabnahmeregelung, was bedeutet, dass die Implikation "Wenn symbolische Ausführung einen Pfad (Satz von Eingabetwerten) meldet, muss das reale Programm auch diesem Pfad folgen".
Kurz gesagt, die symbolische Ausführung kann die Erreichbarkeit von Aussagen nachweisen, indem konkrete Beispieleingaben angegeben werden, oder mit anderen Worten, sie kann das Vorhandensein bestimmter Programmverhalten beweisen.
let Schattierungs-/lexikalische Bereiche: Proggers bemerkt, dass es fünf verschiedene Variablen gibt, die als x bezeichnet werden, wie man in dem aufgeräumten Ast sehen kann, dass Proggers zurückkehrt:
// 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 ;
}Darüber hinaus ist Proggers in der Lage, nette Fehlermeldungen zu geben (dank Ariadne):
// Source
fn foo ( ) -> int {
return true ;
} 
Weitere Beispiele finden Sie unter analyzer-examples/tc_bad .
Progger können Programme zu nativem Code kompilieren.
$ 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
24Lizenziert unter einem von
nach Ihrer Option.
Sofern Sie nicht ausdrücklich anders angeben, ist ein Beitrag, der absichtlich zur Aufnahme in die Arbeit von Ihnen eingereicht wird, wie in der Apache-2.0-Lizenz definiert, ohne zusätzliche Bedingungen doppelt lizenziert wie oben.
