Đặt vấn đề Với sự tiến bộ nhanh chóng của cách mạng công nghệ thông tin và chất liệu chính là phần mềm. Nếu nhƣ trƣớc đây phần mềm máy tính chỉ đƣợc sử dụng để tính toán khoa học kỹ thuật và xử lý dữ liệu thì ngày nay nó đã đƣợc ứng dụng vào mọi mặt của đời sống hàng ngày của con ngƣời. Vì thế con ngƣời ngày càng phụ thuộc chặt chẽ vào các sản phẩm phần mềm và do vậy đòi hỏi về chất lƣợng của các sản phẩm phần mềm ngày càng cao, tức là phần mềm phải đƣợc sản xuất với giá thành thấp, dễ dùng, an toàn và tin cậy đƣợc. Đánh giá chất lƣợng phần mềm thông thƣờng qua các hoạt động phổ biến nhƣ tìm xem phần mềm có lỗi không và có những kỹ thuật nào để phát hiện các lỗi đó.
Việc phát hiện lỗi hay bất cứ vấn đề gì về sản phẩm đều có thể thực hiện ở các mức của quá trình sản xuất phần mềm nhƣ mức phân tích, mức thiết kế và mức lập trình. Ở mức lập trình việc phát hiện lỗi trở nên phức tạp và khó giải quyết hơn. Cụ thể nhƣ bài toán quản lý bộ nhớ. Hiện nay, nhiều hệ thống ngôn ngữ lập trình sử dụng cơ chế quản lý bộ nhớ tự động, tiêu biểu nhƣ Java và C#.
Tuy nhiên, một số ngôn ngữ lập trình truyền thống, đƣợc sử dụng phổ biến trong thực tế nhƣ C, C++ thì vấn đề quản lý bộ nhớ vẫn đƣợc dựa hoàn toàn vào lập trình viên. Liên quan tới bài toán này kỹ thuật phân tích chƣơng trình tĩnh của mảng các kỹ thuật kiểm chứng chƣơng trình là có tính ứng dụng và hiệu quả cao. Và việc áp dụng kỹ thuật phân tích chƣơng trình tĩnh vào trong bài toán quản lý bộ nhớ sẽ là nội dung chính của luận văn này. Giới thiệu phân tích chƣơng trình tĩ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 đó.
Có rất nhiều câu hỏi thú vị liên quan tới chƣơng trình hoặc các điểm (point) riêng lẻ trong chƣơng trình: Chƣơng trình có dừng hay không? Độ lớn có thể của vùng nhớ heap trong quá trình chạy nhƣ thế nào? Đầu ra (output) có thể là gì? Giá trị của sẽ đƣợc đọc trong tƣơng lai? Điểm và có cấu trúc tách rời nhau trong heap? Con trỏ có thể null? Biến đã đƣợc khởi tạo trƣớc đọc hay không? v. TIEU LUAN MOI download : skknchat@gmail.com 8 Theo lý thuyết Rice [9], tất cả các câu hỏi liên quan tới hành vi chƣơng trình là không quyết định đƣợc (undecidable). Việc xử lý vấn đề này luôn đi kèm một số kĩ thuật xấp xỉ nhằm đƣa về bài toán giải đƣợc hoặc để tối ƣu hóa kết quả. 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 sẽ đi sâu tìm hiểu về một bài toán đặc trƣng trong phân tích chƣơng trình tĩnh và các hƣớng giải quyết của bài toán đó. Điểm mạnh và điểm yếu của phân tích chƣơng trình tĩnh Phân tích chƣơng trình tĩnh có một số ƣu điểm sau: Chỉ ra đƣợc chính xác vị trí lỗi trong chƣơng trình. Lỗi đƣợc phát hiện sớm trong quy trình phát triển phần mềm nên chi phí sửa thấp. Tự động hóa nhanh: thông qua các công cụ hỗ trợ nhƣ TVLA, Astree, SOOT, Valgrind … 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.
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: Không phát hiện đƣợc lỗi chỉ xuất hiện khi chạy chƣơng trình(run- time error). Mất thời gian nếu thực hiện bằng tay.
Việc tự động hóa chỉ hƣớng vào một số ngôn ngữ nhất định. Đòi hỏi nhân lực phải có kiến thức về ngôn ngữ lập trình. Có thể sinh ra nhiều lời cảnh báo lỗi không chính xác. Các kỹ thuật 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: 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) [8] [10].
Phân tích luồng dữ liệu là một kỹ thuật thu thập thông tin về tập các giá trị đƣợc tính toán có thể có tại các điểm khác nhau của chƣơng trình. Thông tin thu đƣợc thƣờng đƣợc trình biên dịch sử dụng để tối TIEU LUAN MOI download : skknchat@gmail.com 9 ƣu hóa chƣơng trình. 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. Cách đơn giản để phân tích luồng dữ liệu là thiết lập phƣơng trình luồng dữ liệu cho mỗi nút của đồ thị luồng dữ liệu (DFG – data flow graph) và sử dụng thuật toán điểm cố định để giải hệ phƣơng trình này.
Và một số ứng dụng phổ biển của phân tích luồng dữ liệu là phân tích tính tới đƣợc (reaching definitions), biểu thức có sẵn (available expressions), biểu thức bận rộn (very busy expressions) và phân tích tính sống (liveness analysis) [10] 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) [2] [3]. 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 để tinh chỉnh (refinement) các ánh xạ trừu tƣợng thông qua các tham số đƣa vào, bởi vì có thể đầu tiên tạo ra (là ngữ nghĩa trừu tƣợng từ chƣơng trình ) không thỏa mãn đặc tả , trƣớc hết phải tinh chỉnh chứ không kết luận ngay là không thỏa mãn do tính không hoàn chỉnh (incompleteness) của kỹ thuật diễn giải trừu tƣợng.
Thay vì kiểm chứng đặc tả trên , chúng ta kiểm chứng đối với ngữ nghĩa trừu tƣợng của. Nếu thỏa mãn bởi , do tính đúng đắn của kỹ thuật diễn giải trừu tƣợng, đƣơng nhiên thỏa mãn. Tính ƣu việt của kỹ thuật này là độ phức tạp của nhỏ hơn rất nhiều tùy theo quá trình trừu tƣợng hóa (ánh xạ trừu tƣợng hóa từ vào ) nhƣ thế nào. 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) [5].
Kiểm chứng mô hình là kỹ thuật kiểm tra xem một mô hình của hệ thống có thỏa mãn một tính chất nào đó hay không. Cụ thể hơn, với mô hình và thuộc tính cho trƣớc, kỹ thuật kiểm tra xem thuộc tính có thỏa mãn trong mô hình hay không:. Về mặt thực thi, kiểm chứng mô hình là kỹ thuật tĩnh, nó duyệt qua tất cả các trạng thái, các đƣờng TIEU LUAN MOI download : skknchat@gmail.com 10 thực thi có thể có trong mô hình để xác định tính khả thỏa của. 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 chuỗi 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.
Những tính chất kiểm tra thƣờng là tính sống (liveness properties), tính an toàn (safety properties) nhƣ khả năng không tồn tại 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. Nhóm kỹ thuật này tập trung vào các hệ thống hữu hạn trạng thái hoặc đƣợc giảm xuống còn hữu hạn trạng thái bởi sự trừu tƣợng hóa (abstraction). Cuối cùng, kỹ thuật phân tích biểu trƣng (symbolic analysis) [14]. 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 (constraints) 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. Với tình hình nghiên cứu cơ bản và xu thế công nghệ phần mềm trên thế giới hiện nay tập trung vào các vấn đề lớn nhƣ quy mô và chất lƣợng của các sản phẩm phần mềm, bài toán quản lý bộ nhớ heap là một trong những bài toán phổ biến đặc trƣng trong đảm bảo chất lƣợng phần mềm.
Việc tiến hành nghiên cứu trong lĩnh vực này là cần thiết trong việc nâng cao chất lƣợng nghiên cứu ứng dụng vào thực tế kiểm soát chất lƣợng phần. Do đó, luận văn sẽ tập trung vào nhóm các kỹ thuật liên quan để giải quyết bài toán trên. TIEU LUAN MOI download : skknchat@gmail.com 11 CHƢƠNG 2. LÝ THUYẾT NỀN TẢNG 2.
Nền tảng phân tích ngữ nghĩa của chƣơng trình 2.