Chương 1 Giới thiệu 1. Giới thiệu về phân tích chương trình Phân tích chương trình tĩnh là kỹ thuật xác định tính chất/hành vi của một chương trình mà không cần phải chạy chương trình đó. Phân tích tĩnh được xây dựng dựa trên lý thuyết diễn giải trừu tượng (abstract interpretation) [5, 6] để chứng minh tính chính xác của các phân tích liên quan đến ngữ nghĩa của một ngôn ngữ lập trình. Có rất nhiều câu hỏi thú vị mà có thể được hỏi về một chương trình hoặc các điểm (point) riêng lẻ trong chương trình như: • Chương trình có dừng hay không? • Độ lớn có thể của vùng nhớ (heap) trong khi chạy? • Đầu ra (output) có thể là gì? • Biến x có luôn luôn cùng giá trị không? • Giá trị của x sẽ được đọc trong tương lai? • Con trỏ p null? • Biến x đã được khởi tạo trước khi đọc không? • v.
Theo lý thuyết Rice [14], tất cả các câu hỏi trên về hành vi của chương trình là không thể quyết định/chứng minh được (undecidable). Thay vì mức mô hình như nhiều phương pháp hình thức, luận văn hướng tới việc phân tích chương trình tĩnh. Cụ thể, luận văn trình bày một kỹ thuật để cải z 10 tiến mã chương trình và phát hiện các lỗi tiềm năng bằng việc phân tích chương trình tĩnh dựa trên phân tích luồng dữ liệu. Điểm mạnh và điểm yếu Phân tích chương trình tĩnh có những ưu điểm sau: • Chỉ ra lỗi tại vị trí chính xác trong chương trình • Dễ dàng thực hiện bởi những chuyên gia kiểm định chất lượng phần mềm hiểu rõ về mã nguồn • Khoảng thời gian ngắn từ lúc phát hiện tới khi sửa lỗi • Có thể tự động hóa nhanh (thông qua các bộ công cụ hỗ trợ ví dụ: SOOT, Astree, TVLA,.) • Lỗi được phát hiện sớm trong qui trình phát triển phần mềm nên chi phí sửa lỗi thấp.
Tuy nhiên, điểm yếu của kỹ thuật này xuất hiện khi tại một câu lệnh xuất hiện những tham chiếu, ràng buộc nằm ngoài phạm vi suy luận biểu trưng của chương trình. Hạn chế này là bản chất của việc phân tích tĩnh - không chạy với dữ liệu cụ thể. Một số điểm yếu không khắc phục được: • Mất thời gian nếu phải thực hiện bằng tay • Việc tự động hóa chỉ hướng vào một ngôn ngữ lập trình (ví dụ: SOOT chỉ kiểm tra mã nguồn chương trình viết bằng ngôn ngữ Java) • Thiếu nhân lực có thể hiểu và phân tích được chương trình • Có thể sinh ra nhiều lời cảnh báo lỗi không chính xác • Không phát hiện được lỗi chỉ xuất hiện khi chạy chương trình (run-time er- ror). Các công nghệ phân tích chương trình tĩnh Những kỹ thuật phân tích chương trình tĩnh đã và đang thu hút nhiều nghiên cứu trên thế giới, hiện có nhiều kỹ thuật nhưng tựu chung có thể phân theo 4 nhóm chính như sau: z 11 Thứ nhất, kỹ thuật phân tích chương trình tĩnh dựa trên phân tích luồng dữ liệu (data flow analysis) [11, 15].
Phân tích luồng dữ liệu là một quá trình thu thập thông tin về dữ liệu trong các đoạn mã đó được thực thi trong thực tế trong chương trình mà không cần phải chạy đoạn mã đó. Tuy nhiên, phân tích luồng dữ liệu không sử dụng thao tác dựa trên ngữ nghĩa. Phân tích luồng dữ liệu là một cách rất hiệu quả và khả thi trong việc phát hiện lỗi chương trình và tối ưu hóa trong các trình biên dịch. Thứ hai, nhóm kỹ thuật liên quan tới xấp xỉ ngữ nghĩa được gọi là diễn giải trừu tượng (abstract interpretation) [5, 6].
Kỹ thuật diễn giải trừu tượng dựa trên nguyên tắc xấp xỉ ngữ nghĩa của chương trình khi kiểm tra đối chiếu sự thỏa mãn đặc tả. Kỹ thuật này trích ra từ một ngữ nghĩa chuẩn (standard semantics) được một ngữ nghĩa trừu tượng đã xấp xỉ và tính toán được (approximate and computable abstract semantics). Quá trình chuyển này không hoàn toàn tự động mà có thể cần sự tương tác với người dùng. Trong thực tế, kỹ thuật diễn giải trừu tượng có một thành phần là bộ sinh (generator) ngữ nghĩa trừu tượng đọc mã nguồn chương trình và tạo ra các ràng buộc hoặc hệ các phương trình cần được giải bởi máy tính thông qua một thành phần khác là bộ giải (solver).
Một phương pháp phổ biến là dùng hàm lặp khi giải. Việc tìm nghiệm thông qua hàm lặp có hạn chế về mặt thời gian (phương pháp không hội tụ sau vô hạn lần lặp). Các kỹ thuật liên quan tới việc tăng tốc hội tụ cũng được nghiên cứu. Thứ ba, nhóm kỹ thuật liên quan tới mô hình được gọi là kỹ thuật kiểm chứng mô hình (Model checking) [4].
Mô hình (model) của một hệ thống là một cách biểu hiện ở mức trừu tượng cao hơn của hệ thống bằng cách lược bỏ những phần quá chi tiết mà vẫn giữ lại những thông tin cần thiết về hệ thống đang được xem xét. Trong lĩnh vực phần mềm, kiểm chứng mô hình là cách kiểm tra xem liệu mô hình của một hệ thống (phần cứng hay phần mềm) thỏa mãn một tính chất nào đó hay không. Những đặc tả tính chất đó thường là những tính chất an toàn như khả năng không tồn tại những khóa chết (deadlock) hoặc rơi vào những trạng thái nguy hiểm tạo sự cố cho hệ thống. Nếu một hệ thống không thoả mãn một tính chất thì kiểm chứng mô hình sẽ đưa ra phản ví dụ với một xâu các trạng thái và sự kiện liên quan bắt đầu từ trạng thái ban đầu tới trạng thái lỗi của mô hình.
Cuối cùng, kỹ thuật phân tích biểu trưng (symbolic analysis) [18]. Kỹ thuật này là phân tích tĩnh mã nguồn tĩnh, xây dựng các luồng rẽ nhánh trong chương trình dựa trên các nút. Tại các nút tương ứng sẽ là tập hợp các ràng buộc (con- z 12 straints) của dữ liệu, biến, tham số. Tại nút khởi tạo chương trình, tập hợp các ràng buộc là rỗng.
Càng đi sâu xuống các nhánh nhỏ, tại các nút con, tập hợp ràng buộc sẽ được tạo ra từ tập hợp ràng buộc tại nút ngay phía trên cộng với điều kiện giữa các biến số để có thể rẽ từ nút trên vào nút dưới trong luồng chảy chương trình. Điểm đặc biệt của kỹ thuật này là các tham số hoàn toàn được thể hiện bằng ký tự biểu trưng, chứ không phải giá trị cụ thể. Ý tưởng của phương pháp này là để kiểm thử một nhánh trong chương trình, điều kiện tiên quyết là dữ liệu tại đầu vào phải thỏa mãn tập hợp các ràng buộc tại nút bắt đầu nhánh đó. Việc giải các ràng buộc gắn với một nút được thực hiện bởi các bộ công cụ sẵn có gọi là giải ràng buộc (constraint solver) dựa trên SMT (Satisfiability Modulo Theories) hay SAT (Satisfiability Testing).
Hai nhóm đầu tập trung vào việc nâng cao chất lượng phần mềm tại mức mã nguồn, trong khi hai nhóm sau xử lý phần mềm tại mức trừu tượng cao hơn – mô hình. Luận văn sẽ tập trung vào xu thế thứ nhất, đó là kiểu phân tích luồng dữ liệu dựa trên đồ thị luồng dữ liệu. Đồ thị luồng điều khiển Đồ thị luồng điều khiển (Control Flow Graph-CFG) là một đồ thị có hướng, trong đó các nút (node) tương ứng là các điểm (point) chương trình và các cạnh thể hiện cho luồng điểu khiển. Một CFG luôn luôn có một điểm của đầu vào, ký hiệu là entry, và một điểm của đầu ra, ký hiệu là exit.
Ngoài ra, nếu v là một nút trong CFG thì những ký hiệu pred(v) là tập các nút kế trước (predecessor) và succ(v) là tập các nút kế sau (successor). CFG cho các lệnh • Các lệnh cơ bản Các lệnh đơn giản mà CFG có thể khởi tạo liên quan đến. Những CFG cơ bản trong ngôn ngữ lập trình Java như là các phép gán (id = E;), output (printf(E);), lệnh return (return;), và khai báo biến (ví dụ int f;) được môt tả trong Hình 1.1 bên dưới: z 13 id = E printf(E) return E int id Hình 1.1: CFG cho các lệnh cơ bản. • Các lệnh tuần tự Cho chuỗi lệnh tuần tự S 1 S 2, ta loại bỏ các nút exit của lệnh S 1 và nút entry của lệnh S 2 và gắn các lệnh lại với nhau (Hình 1.2: CFG cho các lệnh tuần tự.
• Các lệnh cấu trúc điều khiển Cấu trúc điều khiển được minh họa bởi đồ thị quy nạp: Các lệnh if, if-else E E S S1 S2 if(E) S; if(E) S1; else S2; Hình 1.3: CFG cho các lệnh if, if-else. z 14 Các lệnh while, for E1 E2 E S S E3 while(E) S; for(E1; E2; E3;) S; Hình 1.4: CFG cho các lệnh while, for. Ví dụ CFG của một chương trình Sử dụng các cách xây dựng CFG cho từng lệnh ở trên, ta xây dựng CFG cho một ví dụ chương trình hàm tính giai thừa viết bằng ngôn ngữ Java: int iterative(int n) { int f;// khai báo biến (f là kiểu int) int uu_f; f = 1; uu_f = 0;// biến này không là biến sống while (n > 0){ f = f*n; n = n - 1; } return f; } Và được biểu diễn thành CFG như sau: z 15 int f int uu_f f=1 uu_f = 0 n>0 f = f*n n=n-1 return f Hình 1.5: CFG của chương trình tính giai thừa. Lý thuyết Dàn Dàn Trong kỹ thuật phân tích chương trình tĩnh của luận văn, các phân tích sử dụng cấu trúc toán học là Dàn (Lattices) [16], tập các thuộc tính (ví dụ: tập các biến, biểu thức,.trong chương trình) cần thiết cho mỗi phân tích tĩnh trong chương trình.
Định nghĩa Dàn Một thứ tự bộ phận (partial order) là một cấu trúc toán học: L = (S , ⊑), với S là một tập và ⊑ là quan hệ hai ngôi trên tập S , thỏa mãn các điều kiện sau: z 16 • Phản xạ: ∀x ∈ S : x ⊑ s • Phản xứng: ∀x, y ∈ S : x ⊑ y ∧ y ⊑ x ⇒ x = y • Bắc cầu: ∀x, y, z ∈ S : x ⊑ y ∧ y ⊑ z ⇒ x ⊑ z Biểu diễn Dàn thông qua biểu đồ Hasse Cho Dàn L = (S , ⊑) là tập có thứ tự bộ phận, biểu đồ Hasse của Dàn L bao gồm: • Một tập hợp các điểm trong mặt phẳng tương ứng 1-1 với S, gọi là các đỉnh. • Một tập hợp các cung nối một số cặp đỉnh có quan hệ thứ tự bộ phận. Ví dụ, biểu diễn Dàn (2{x,y,x} , ⊆) (Hình 1.6: Biểu đồ Hasse biểu diễn Dàn. Cận trên, cận dưới Cho X ⊆ S.
Ta nói rằng y ∈ S là một cận trên của X, ký hiệu X ⊑ y, nếu ∀x ∈ X : x ⊑ y.