Phân tích chương trình tĩnh

Phân tích chương trình tĩnh kiểm tra mã nguồn hoặc mã trung gian, mà không thực thi, để suy luận các thuộc tính như biến có thể chứa giá trị nào hoặc liệu lỗi có thể xảy ra hay không.

Definition

Phân tích chương trình tĩnh là việc tính toán thông tin gần đúng nhưng đúng đắn về các hành vi có thể có của một chương trình trực tiếp từ mã của nó, mà không chạy chương trình, thường bằng cách giải các phương trình luồng dữ liệu trên một lưới các trạng thái trừu tượng.

Scope

Chủ đề này bao gồm phân tích luồng dữ liệu trên các đồ thị luồng điều khiển, tính toán điểm cố định dựa trên lưới, phân tích liên thủ tục, phân tích con trỏ và bí danh, cũng như phân tích đồ thị cuộc gọi và luồng điều khiển. Nó đề cập đến các chiều chính xác (độ nhạy theo luồng, theo ngữ cảnh và theo đường dẫn), tính đúng đắn của các phân tích và việc sử dụng chúng trong tối ưu hóa và phát hiện lỗi.

Core questions

• Các thuộc tính chương trình được tính toán bằng cách truyền các sự kiện trên một đồ thị luồng điều khiển như thế nào?
• Độ nhạy theo luồng, theo ngữ cảnh và theo đường dẫn ảnh hưởng đến độ chính xác và chi phí như thế nào?
• Phân tích đúng đắn được thực hiện qua các lời gọi thủ tục như thế nào?
• Phân tích con trỏ đối phó với bí danh và gián tiếp như thế nào?

Key theories

Phân tích luồng dữ liệu như điểm cố định trên một lưới

Kildall đã thống nhất các tối ưu hóa chương trình toàn cục thành việc tính toán một điểm cố định của các phương trình luồng dữ liệu trên một lưới, cung cấp khuôn khổ chung cho các phân tích tĩnh.

Phân tích liên thủ tục thông qua khả năng tiếp cận đồ thị

Reps, Horwitz và Sagiv đã giảm một lớp lớn các vấn đề luồng dữ liệu liên thủ tục chính xác thành khả năng tiếp cận đồ thị, cho phép phân tích nhạy ngữ cảnh hiệu quả qua các ranh giới thủ tục.

Các nguyên tắc và chiều phân tích

Nielson, Nielson và Hankin hệ thống hóa các phân tích dựa trên luồng dữ liệu, dựa trên ràng buộc và dựa trên kiểu, cùng với các đánh đổi giữa độ chính xác và chi phí chi phối thiết kế của chúng.

Clinical relevance

Phân tích tĩnh thúc đẩy các tối ưu hóa trình biên dịch, các công cụ tìm lỗi và lỗ hổng, các công cụ kiểm tra cú pháp (linters) và các tính năng của môi trường phát triển tích hợp (IDE). Các phân tích đúng đắn có thể chứng nhận sự vắng mặt của một số lỗi nhất định, trong khi các phân tích heuristic có khả năng mở rộng được triển khai rộng rãi để phát hiện các khiếm khuyết sớm trong quá trình phát triển.

History

Phân tích luồng dữ liệu phát triển từ các trình biên dịch tối ưu hóa, với khuôn khổ lưới của Kildall năm 1973 và các phân tích của Allen-Cocke cung cấp cơ sở lý thuyết. Các phân tích liên thủ tục và con trỏ đã tiến bộ trong những năm 1980 và 1990, bao gồm công thức khả năng tiếp cận của Reps-Horwitz-Sagiv, và phân tích tĩnh sau đó đã được mở rộng để tìm lỗi công nghiệp trên các cơ sở mã rất lớn.

Debates

Độ chính xác so với khả năng mở rộng

Các nhà thiết kế phân tích liên tục đánh đổi các chiều chính xác như độ nhạy theo ngữ cảnh và theo đường dẫn, giúp giảm thiểu các dương tính giả, với chi phí tính toán giới hạn kích thước chương trình có thể được phân tích.

Key figures

• Gary Kildall
• Thomas Reps
• Susan Horwitz
• Flemming Nielson
• Hanne Riis Nielson

Seminal works

• kildall1973
• reps1995
• nielson1999

Frequently asked questions

Một phân tích tĩnh được coi là đúng đắn có nghĩa là gì?

Một phân tích đúng đắn không bao giờ bỏ sót một sự xuất hiện thực sự của thuộc tính mà nó kiểm tra: nếu nó không báo cáo lỗi thuộc một loại nhất định, thì loại lỗi đó thực sự không thể xảy ra, mặc dù nó cũng có thể đưa ra các cảnh báo sai.

Tại sao phân tích con trỏ lại khó khăn?

Các con trỏ và tham chiếu tạo ra bí danh, nơi nhiều tên tham chiếu đến cùng một bộ nhớ, vì vậy phân tích phải ước tính vị trí mà mỗi con trỏ có thể nhắm tới, một vấn đề đánh đổi độ chính xác với khả năng mở rộng.