progge.rs
1.0.0
Proggers هو ملعب تحليل البرنامج للغة بسيطة وضرورية.
التبعيات:
لا يلزم إيلينا ولا LLVM ولا Z3 لتصور النوع و CFG ، وبالتالي يمكن تحويلها إلى ميزة قفص. من فضلك ، لا تتردد في المساهمة!
بمجرد تثبيت المتطلبات المسبقة ، يمكنك تثبيت proggers مع: 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 بتظليل الارتباطات السابقة.
Bruign-Prinive INS الخاصة بـ Progge وأي جزء من Proggers يستخدمها:
| مدمج | وصف | منظمة العفو الدولية | SE | TC | ج |
|---|---|---|---|---|---|
unreachable! | يؤكد أن تدفق التحكم قد لا يصل أبدًا إلى هذا البيان | [x] | [x] | ||
testcase! | يرشد توليد testcases التي تصل إلى هذا البيان | [x] | [x] | ||
assume!(expr) | يفترض أن تعبير منطقي المعطى صحيح | [x] | [x] | ||
analyze!(expr) | يرشد التحليل العددي لطباعة القرب المفرط للتعبير الباحث | [x] | |||
int_arg(expr) | إرجاع وسيطة سطر الأوامر expr-th تم تحويلها إلى int | [x] | [x] | ||
print_int(expr) | يطبع int المعطى إلى stdout | [x] |
Legend : TC: Type-Decking ، SE: التنفيذ الرمزي ، الذكاء الاصطناعي: Interpertation التجريدي ، 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 أيضًا على مكالمات إلى 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 يعطي: 
يقوم التنفيذ الرمزي (ويكيبيديا) بحساب القرب من نقص الجبهة ، مما يعني أن المعنى الضمني هو "إذا كان التنفيذ الرمزي يبلغ مسارًا (مجموعة من قيم الإدخال) ، فيجب أن يتبع البرنامج الحقيقي أيضًا هذا المسار".
باختصار ، يمكن أن يثبت التنفيذ الرمزي إمكانية الوصول إلى البيانات من خلال إعطاء مدخلات مثال ملموس ، أو ، وبعبارة أخرى ، يمكن أن يثبت وجود بعض سلوكيات البرنامج.
let التظليل/النطاقات المعجمية: يلاحظ بروججرز أن هناك خمسة متغيرات متميزة تسمى x ، كما يمكن للمرء أن يرى في AST المنحذ أن 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 لمزيد من الأمثلة.
يمكن لـ 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 ، تكون مرخصة مزدوجة على النحو الوارد أعلاه ، دون أي شروط أو شروط إضافية.
