Tài liệu Kỹ thuật phân tích chương trình tĩnh cho bài toán phân tích hình dạng bộ nhớ Heap

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN QUANG ĐẠI KỸ THUẬT PHÂN TÍCH CHƢƠNG TRÌNH TĨNH CHO BÀI TOÁN PHÂN TÍCH HÌNH DẠNG BỘ NHỚ HEAP LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN Hà Nội – 2015 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN QUANG ĐẠI KỸ THUẬT PHÂN TÍCH CHƢƠNG TRÌNH TĨNH CHO BÀI TOÁN PHÂN TÍCH HÌNH DẠNG BỘ NHỚ HEAP Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƢỜI HƢỚNG DẪN KHOA HỌC: TS. Nguyễn Trƣờng Thắng Hà Nội - 2015 LỜI CAM ĐOAN Tôi xin cam đoan rằng đây là công trình nghiên cứu của tôi trong đó có sự giúp đỡ của Thầy giáo hƣớng dẫn và các đồng nghiệp tại cơ quan. Các nội dung và kết quả nghiên cứu trong luận văn này là hoàn toàn trung thực. Trong luận văn, tôi có tham khảo đến một số tài liệu của một số tác giả đƣợc liệt kê tại mục tài liệu tham khảo. Hà Nội, 03 tháng 07 năm 2015 Học viên Nguyễn Quang Đại LỜI CẢM ƠN Tôi xin chân thành cảm ơn các thầy cô giáo trong Khoa Công nghệ Thông tin, Trƣờng Đại học Công nghệ – Đại học Quốc gia Hà Nội đã tận tình giảng dạy trang bị cho tôi kiến thức, giúp tôi hoàn thành luận văn. Tôi cũng xin đƣợc bày tỏ lòng kính trọng và lời cảm ơn sâu sắc nhất tới TS. Nguyễn Trƣờng Thắng, Phó Viện trƣởng, Viện Công nghệ Thông Tin – Viện Hàn lâm Khoa học và Công nghệ Việt Nam. Thầy đã luôn động viên và hƣớng dẫn tôi hoàn thành luận văn tốt nghiệp. Mặc dù đã cố gắng để hoàn thành luận văn, nhƣng trong phạm vi và khả năng cho phép không thể tránh khỏi những thiếu sót, mong nhận đƣợc sự cảm thông và tận tình chỉ bảo của các thầy cô. Hà Nội, 03 tháng 07 năm 2015 Học viên Nguyễn Quang Đại 1 MỤC LỤC MỤC LỤC ............................................................................................................. 1 DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT ........................................... 3 DANH SÁCH HÌNH VẼ ...................................................................................... 4 MỞ ĐẦU ............................................................................................................... 5 CHƢƠNG 1. GIỚI THIỆU CHUNG .................................................................... 7 1.1. Đặt vấn đề .............................................................................................. 7 1.2. Giới thiệu phân tích chƣơng trình tĩnh .................................................. 7 1.3. Điểm mạnh và điểm yếu của phân tích chƣơng trình tĩnh .................... 8 1.4. Các kỹ thuật phân tích chƣơng trình tĩnh .............................................. 8 CHƢƠNG 2. LÝ THUYẾT NỀN TẢNG ........................................................... 11 2.1. Nền tảng phân tích ngữ nghĩa của chƣơng trình ................................. 11 2.1.1. Lý thuyết giàn ............................................................................ 11 2.1.2. Thuộc tính đóng......................................................................... 13 2.1.3. Phƣơng trình và bất phƣơng trình ............................................. 15 2.1.4. Lý thuyết điểm cố định .............................................................. 16 2.1.5. Các kỹ thuật tăng tốc độ hội tụ widening/narrowing ................ 18 2.2. Kết luận chƣơng .................................................................................. 22 CHƢƠNG 3. PHÂN TÍCH HÌNH DẠNG HEAP .............................................. 23 3.1. Phân tích con trỏ ....................................................................................... 23 3.1.1. Thuật toán Andersen.................................................................... 23 3.1.2. Thuật toán Steensgaard................................................................ 25 3.2. Phân tích con trỏ liên thủ tục .................................................................... 26 3.3. Phân tích hình dạng bộ nhớ heap ............................................................. 27 3.2.1. Kỹ thuật phân tích........................................................................ 29 3.2.2. Đánh giá ....................................................................................... 33 3.3. Kết luận chƣơng ....................................................................................... 33 CHƢƠNG 4. THỰC NGHIỆM .......................................................................... 34 4.1. 2 Tổng quan về Valgrind ........................................................................ 34 4.1.1. Công cụ Memcheck ..................................................................... 35 4.1.2. Biên dịch chƣơng trình với Memcheck ....................................... 37 4.1.3. Lệnh kiểm tra trong Memcheck .................................................. 37 4.2. Phân tích heap của chƣơng trình trong Valgrind ................................ 39 4.2.1. Rò rỉ bộ nhớ ............................................................................... 39 4.2.2. Sử dụng bộ nhớ không đƣợc khởi tạo ....................................... 40 4.2.3. Lỗi sử dụng không đúng giữa malloc/ new/ new[] với free/ delete/ delete[].............................................................................................. 43 4.2.4. Thực nghiệm trên chƣơng trình có mã nguồn lớn..................... 45 KẾT LUẬN ......................................................................................................... 47 TÀI LIỆU THAM KHẢO ................................................................................... 48 PHỤ LỤC A ........................................................................................................ 49 PHỤ LỤC B ........................................................................................................ 51 PHỤ LỤC C ........................................................................................................ 55 3 DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT Ký hiệu Thuật ngữ CFG Control Flow Graph CG Garbage Collection DFG Data Flow Graph SMT Satisfiability Modulo Theories SAT Satisfiability Testing 4 DANH SÁCH HÌNH VẼ Hình 2.1. Biểu đồ Hasse biểu diễn giàn ..................................................... 11 Hình 2.2. Quan hệ thứ tự từng phần là giàn ............................................... 12 Hình 2.3. Quan hệ thứ tự từng phần không phải giàn................................ 12 Hình 2.4. Ví dụ giàn có chiều cao là 4 ....................................................... 13 Hình 2.5. Phép toán cộng giàn ................................................................... 14 Hình 2.6. Phép toán nâng (lift) giàn. .......................................................... 14 Hình 2.7. Phép toán lift của các tập tạo thành giàn. .................................. 14 Hình 2.8. Tính toán điểm cố định trên giàn ............................................... 17 Hình 2.9. Giàn có chiều cao vô hạn ........................................................... 19 Hình 3.1. Quan hệ tƣơng đƣơng giữa các ràng buộc ................................. 26 Hình 3.2. Đồ thị heap ................................................................................. 30 Hình 3.3. Đồ thị hình dạng heap sau vòng lặp ........................................... 32 Hình 4.1. Kết quả ví dụ rò rỉ bộ nhớ trong Memcheck.............................. 40 Hình 4.2. Kết quả ví dụ sử dụng bộ nhớ chƣa đƣợc khởi tạo trong Memcheck sử dụng –track-origins ...................................................................... 42 Hình 4.3. Kết quả ví dụ sử dụng bộ nhớ chƣa đƣợc khởi tạo trong Memcheck không sử dụng –track-origins ........................................................... 43 Hình 4.4. Kết quả ví dụ lỗi sử dụng không đúng giữa malloc/new/new[] với free/delete/delete[] ........................................................................................ 44 5 MỞ ĐẦU Ngày nay với sự phát triển vƣợt bậc của công nghệ thông tin, thì phần mềm có vai trò cốt lõi và ngày càng chiếm vị trí quan trọng không những trong công nghệ thông tin mà còn trong đời sống kinh tế xã hội. Vấn đề chất lƣợng phần mềm (software quality) chắc chắn là mối quan tâm và thách thức đối với xã hội hiện đại ngày càng phụ thuộc vào các dịch vụ do máy tính đem lại này. Liên quan tới đảm bảo chất lƣợng phần mềm, khía cạnh quản lý bộ nhớ cũng rất đƣợc quan tâm. Quản lý bộ nhớ đƣợc chia làm hai giai đoạn chính là phân bổ bộ nhớ theo yêu cầu, và giải phóng khi chƣơng trình không còn sử dụng. 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#. Trong Java, ngƣời lập trình không cần phải chú trọng đến phân bổ và giải phóng bộ nhớ. Khi khối bộ nhớ đƣợc phân bổ không còn đƣợc sử dụng máy ảo Java (Java Virtual Machine) sẽ tự giải phóng bộ nhớ thông qua cơ chế thu dọn rác tự động (Automatic Garbage Collection) [1]. Thu gom rác tự động là quá trình kiểm tra bộ nhớ heap, xác định những đối tƣợng đang đƣợc sử dụng và không đƣợc sử dụng, và xóa những đối tƣợng không đƣợc sử dụng. Chức năng cơ bản của GC (Garbage Collection) là gồm hai bƣớc trừu tƣợng (trong thực tế hai pha này có thế đan xen nhau):  Phát hiện rác (tìm đối tƣợng từ đống rác bằng một cách nào đó)  Cải tạo rác (Cải tạo lại ô nhớ của đối tƣợng rác, khi đó chƣơng trình đang chạy có thể sử dụng ô nhớ này). 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 đặt hoàn toàn vào lập trình viên [6]. Lập trình viên tự động cấp phát bộ nhớ, nhƣng khi một khối không còn cần thiết, họ cần phải trả lại cho hệ thống bằng lời gọi hàm hệ thống nhƣ free(). Hậu quả là nếu ngƣời lập trình quên hoàn trả các vùng đã cấp phát về cho bộ nhớ và lại tiếp tục dùng các lệnh cấp phát, thì càng lúc càng nhiều các phần của bộ nhớ bị chiếm chỗ. Điều này có thể dẫn tới các lỗi liên quan tới bộ nhớ, đặc biệt là khối bộ nhớ khởi tạo tự động bởi con trỏ hay mắc lỗi rò rỉ bộ nhớ (memory leak). Quản lý bộ nhớ là quan trọng và có nhiều khía cạnh nghiên cứu. Các kỹ thuật thu dọn rác là một hƣớng tiếp cận của vấn đề này. Mục tiêu của luận văn này là tìm hiểu về kỹ thuật phân tích chƣơng trình tĩnh, cập nhật những xu hƣớng nghiên cứu trong và ngoài nƣớc về lĩnh vực phân tích chƣơng trình tĩnh, và cải tiến những kỹ thuật này. Cụ thể, luận văn tập trung vào hƣớng tiếp cận là tìm hiểu kỹ thuật phân tích hình dạng bộ nhớ heap của 6 chƣơng trình. Kết quả của kỹ thuật có thể áp dụng trong khâu loại bỏ các đối tƣợng là rác. Kỹ thuật dựa trên lý thuyết ngữ nghĩa chƣơng trình theo các con trỏ. Lý thuyết giàn, ngữ nghĩa điểm cố định cũng sẽ đƣợc sử dụng nhƣ nền tảng của kỹ thuật này. Luận văn có cấu trúc nhƣ sau: Chƣơng 1 giới thiệu tổng quan về phân tích chƣơng trình tĩnh. Trong chƣơng này trình bày định nghĩa kỹ thuật phân tích chƣơng trình tĩnh, ứng dụng, điểm mạnh và điểm yếu của kỹ thuật này. Tiếp đó luận văn trình bày một vài kỹ thuật phân tích chƣơng trình tĩnh phổ biến hiện nay, bài toán và kỹ thuật mà luận văn thực hiện tìm hiểu. Chƣơng 2 trình bày nền tảng ngữ nghĩa của một chƣơng trình Chƣơng 3 trình bày về kỹ thuật phân tích hình dạng bộ nhớ heap. Đƣa ra các bài toán, cách giải quyết và đánh giá. Chƣơng 4 thực nghiệm với công cụ Valgrind Cuối cùng là phần kết luận và tài liệu tham khảo. 7 CHƢƠNG 1. GIỚI THIỆU CHUNG 1.1. Đặ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. 1.2. 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.v.. 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 đó. 1.3. Đ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(runtime 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. 1.4. 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 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 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. 11 CHƢƠNG 2. LÝ THUYẾT NỀN TẢNG 2.1. Nền tảng phân tích ngữ nghĩa của chƣơng trình 2.1.1. Lý thuyết già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à Giàn (Lattices) [10], 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. Một thứ tự bộ phận (Partial order) là một cấu trúc toán học: , trong đó là một tập hợp và là một quan hệ 2 ngôi trên thỏa mãn các điều kiện sau:  Phản xạ:  Bắc cầu:  Phản đối xứng: Biểu diễn giàn thông qua biểu đồ Hasse Cho giàn gồm : là tập có thứ tự bộ phận, biểu đồ Hasse của giàn L bao  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 giàn { (nhƣ hình) hoặc giàn đảo ngƣợc (Giàn đƣợc sắp xếp bởi thứ tự ngƣợc của các tập con và quan hệ hai ngôi đƣợc định } nghĩa là ) { bằng biểu đồ Hasse : Hình 2.1. Biểu đồ Hasse biểu diễn giàn Cho , khi đó , nếu , kí hiệu là , nếu , đƣợc định nghĩa nhƣ sau: 12 đƣợc gọi là một cận trên của , kí hiệu là . Tƣơng tự đƣợc gọi là một cận dƣới của . Cận trên nhỏ nhất của kí hiệu là Tƣơng tự, cận dƣới lớn nhất, kí hiệu là , đƣợc định nghĩa nhƣ sau: Giàn (Lattice) là một quan hệ thứ tự từng phần mà trong đó và tồn tại đối với tất cả . Lƣu ý rằng một giàn có duy nhất một phần tử lớn nhất đƣợc định nghĩa là = S và duy nhất một phần tử nhỏ nhất đƣợc định nghĩa là . Khi xem xét các giàn hữu hạn, yêu cầu ít nhất là tồn tại phần tử lớn nhất và nhỏ nhất và với mỗi cặp phần tử x và y có một cận trên nhỏ nhất kí hiệu là và cận dƣới nhất nhất kí hiệu là . Một quan hệ thứ tự từng phần hữu hạn đƣợc minh họa bởi một biểu đồ trong đó các phần tử là các nút và quan hệ thứ tự là quan hệ bao đóng bắc cầu (transitive closure) các cạnh từ nút thấp lên nút cao hơn. Với cách biểu diễn này các quan hệ thứ tự trong Hình 2.2 đều là giàn. Hình 2.2. Quan hệ thứ tự từng phần là giàn Trong khi các quan hệ thứ tự trong hình 2.3 không phải là giàn. Hình 2.3. Quan hệ thứ tự từng phần không phải giàn Ví dụ mỗi tập hợp hữu hạn phần tử A định nghĩa một giàn , trong đó 13  tồn tại  Với mỗi cặp phần tử . trong có và Chiều cao của một giàn đƣợc định nghĩa là độ dài của đƣờng dẫn dài nhất từ phần tử tới phần tử . Ví dụ tập giàn lớn nhất ở hình 2.4 có chiều cao là 4. Một cách tổng quát giàn có chiều cao là Hình 2.4. Ví dụ giàn có chiều cao là 4 2.1.2. Thuộc tính đóng Nếu tích (product): là những giàn với độ cao hữu hạn, từ đó một phép toán { } với đƣợc định nghĩa là theo từng điểm (point-wise). Với chú ý rằng thể đƣợc tính toán theo từng điểm và nhƣ vậy và có Tƣơng tự ta có, một phép toán cộng (sum): { với và đƣợc cho trƣớc và Chú ý rằng đƣợc minh nhƣ sau: { }} { } khi và chỉ khi và . { }. Phép toán cộng 14 Hình 2.5. Phép toán cộng giàn Nếu giàn là: là một giàn với độ cao hữu hạn, khi đó , độ cao của giàn , minh họa nhƣ sau: Hình 2.6. Phép toán nâng (lift) giàn. Nếu là một tập hữu hạn ( đƣợc minh họa bởi không cần thiết phải là một giàn), khi đó Hình 2.7. Phép toán lift của các tập tạo thành giàn. 15 Và là một giàn có độ cao là 2. Cuối cùng, nếu và đƣợc định nghĩa nhƣ trên, khi đó chúng ta thu đƣợc một giàn ánh xạ (map) với độ cao nhƣ sau: { theo từng điểm thứ tự: có độ cao hữu hạn khi đó } là hữu hạn và . Nếu . 2.1.3. Phương trình và bất phương trình Trong phân tích mã nguồn chƣơng trình, lý thuyết giàn ngữ nghĩa đƣợc sử dụng. Từng nút trong mã nguồn sẽ đƣợc gắn một giá trị ngữ nghĩa (semantic). Ngữ nghĩa của một nút chịu sự ràng buộc trong mối quan hệ với các nút ở trƣớc và sau nó trong mã nguồn chƣơng trình tùy theo ngữ nghĩa của các câu lệnh đối với một thuộc tính cần xem xét. Ví dụ, thuộc tính con trỏ (shape) trong báo cáo này. Những mối quan hệ ràng buộc thể hiện là các hàm (hàm chuyển đổi ngữ nghĩa - semantic transformer [4]) Cho là một giàn với độ cao hữu hạn. Một hệ phƣơng trình đƣợc biểu diễn: với là những biến và là một tập những hàm đơn điệu. Mỗi hệ chỉ có nghiệm nhỏ nhất duy nhất, nghiệm đó đƣợc gọi là điểm cố định nhỏ nhất của hàm đƣợc định nghĩa bởi: Tƣơng tự, có thể giải hệ các bất phƣơng trình: mặt khác, ta có quan hệ x y tƣơng đƣơng với x = x y.Vì vậy, các nghiệm đƣợc duy trì bằng cách viết lại thành hệ phƣơng trình nhƣ sau: 16 đây là một hệ phƣơng trình với các hàm đơn điệu. 2.1.4. Lý thuyết điểm cố định Hàm là đơn điệu khi hợp của hai hàm đơn điệu là một hàm đơn điệu [10]. . Lƣu ý Lý thuyết về điểm cố định nhƣ sau: trong một giàn có chiều cao hữu hạn, mỗi hàm đơn điệu f có duy nhất một điểm cố định nhỏ nhất (least fixed-point) định nghĩa nhƣ sau: ∐ thỏa mãn . Chứng minh lý thuyết này nhƣ sau. Ta có do là phần tử nhỏ nhất. Do f là hàm đơn điệu nên và bằng phép quy nạp ta có . Do đó, ta có chuỗi tăng dần: Do đƣợc giả định là có chiều cao hữu hạn nên sẽ tồn tại mà . Chúng ta định nghĩa và từ , chúng ta thấy là một điểm cố định. Bây giờ giả sử rằng là một điểm cố định khác. Từ dẫn đến , vì f là hàm đơn điệu và bằng quy nạp ta có . Do đó, là điểm cố định nhỏ nhất. Do tính phản đối xứng nên nó là duy nhất. Độ phức tạp tính toán một điểm cố định phụ thuộc vào 3 yếu tố:  Độ cao của giàn, giá trị độ cao của giàn cung cấp biên cho tham số ;  Chi phí tính toán của hàm ;  Chi phí so sánh kết quả có bằng nhau sau mỗi bƣớc lặp. Tính toán một điểm cố định có thể đƣợc minh họa bằng các bƣớc đi lên trong một giàn bắt đầu từ điểm (Hình 2.8)