progge.rs
1.0.0
Proggers เป็นสนามกีฬาวิเคราะห์โปรแกรมสำหรับภาษาที่เรียบง่ายและจำเป็น
การพึ่งพา:
ทั้ง Elina และ 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]
ไม่มีอะไรพิเศษ การให้การปล่อยให้ได้รับอนุญาตให้เงาการผูกก่อนหน้านี้
Built-ins พิเศษของ Progge และส่วนใดของ proggers ใช้ประโยชน์จากพวกเขา:
| ในตัว | คำอธิบาย | AI | SE | TC | C |
|---|---|---|---|---|---|
unreachable! | ยืนยันว่าการไหลของการควบคุมอาจไม่ถึงคำแถลงนี้ | [x] | [x] | ||
testcase! | แนะนำการสร้าง testcases ที่ไปถึงคำสั่งนี้ | [x] | [x] | ||
assume!(expr) | สมมติว่าการแสดงออกของบูลที่กำหนดเป็นจริง | [x] | [x] | ||
analyze!(expr) | สั่งการวิเคราะห์เชิงตัวเลขเพื่อพิมพ์การแสดงออกของการแสดงออกของ Int มากเกินไป | [x] | |||
int_arg(expr) | ส่งคืนอาร์กิวเมนต์บรรทัดคำสั่ง expr-th ที่แปลงเป็น int | [x] | [x] | ||
print_int(expr) | พิมพ์ int ที่กำหนดเพื่อ stdout | [x] |
Legend : TC: การตรวจสอบประเภท, SE: การดำเนินการเชิงสัญลักษณ์, AI: บทคัดย่อ 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) คำนวณการเปลี่ยนแปลงที่มากเกินไปซึ่งหมายความว่าพฤติกรรมของโปรแกรมที่เป็นไปได้ทั้งหมด (อาจจะมากกว่า แต่ไม่น้อย) จะถูกจับโดยนั่นคือความหมายคือ "หากโปรแกรมจริงแสดงพฤติกรรม
ในระยะสั้นการตีความนามธรรมสามารถพิสูจน์ได้ว่าไม่มีพฤติกรรมของโปรแกรมที่ไม่พึงประสงค์ซึ่งอาจเป็นข้อยกเว้นดัชนีออกจากขอบเขต (สิ่งที่ต้องทำ) การดำเนินการ unreachable! คำสั่งหรือการเรียกใช้ฟังก์ชันที่มีข้อโต้แย้งไม่เป็นไปตามเงื่อนไขของฟังก์ชัน
TESTCASE! : สร้าง 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 ให้: 
Symbolic Execution (Wikipedia) คำนวณการเปลี่ยนแปลงที่ต่ำกว่าซึ่งหมายถึงความหมายคือ "ถ้าการดำเนินการเชิงสัญลักษณ์รายงานเส้นทาง (ชุดของค่าอินพุต) จากนั้นโปรแกรมจริงจะต้องปฏิบัติตามเส้นทางนั้นด้วย"
ในระยะสั้นการดำเนินการเชิงสัญลักษณ์สามารถพิสูจน์ความสามารถในการเข้าถึงของข้อความโดยให้อินพุตตัวอย่างที่เป็นรูปธรรมหรือกล่าวอีกนัยหนึ่งมันสามารถพิสูจน์การมีอยู่ของพฤติกรรมของโปรแกรมบางอย่าง
let ขอบเขตเงา/คำศัพท์: proggers สังเกตว่ามีตัวแปรที่แตกต่างกันห้าตัวที่เรียกว่า 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 จะได้รับใบอนุญาตคู่ดังกล่าวข้างต้นโดยไม่มีข้อกำหนดหรือเงื่อนไขเพิ่มเติมใด ๆ
