Khóa luận Sinh ca kiểm thử tham số hóa cho chương trình java

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Trần Bình Dương SINH CA KIỂM THỬ THAM SỐ HÓA CHO CHƯƠNG TRÌNH JAVA KHÓA LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công Nghệ Thông Tin HÀ NỘI - 2009 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Trần Bình Dương SINH CA KIỂM THỬ THAM SỐ HÓA CHO CHƯƠNG TRÌNH JAVA KHÓA LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công Nghệ Thông Tin Cán bộ hướng dẫn: TS. Trương Anh Hoàng i LỜI CẢM ƠN Lời đầu tiên em xin được gửi lời cảm ơn chân thành tới TS. Trương Anh Hoàng, người thầy đáng kính đã tận tình hướng dẫn em trong suốt thời gian thực hiện khóa luận này. Em cũng muốn bày tỏ lòng biết ơn đến các thầy cô giáo trường Đại học Công Nghệ - Đại học Quốc Gia Hà nội, đặc biệt là các thầy cô trong khoa công nghệ thông tin đã tận tình dạy dỗ và tạo mọi điều kiện học tập thuận lợi cho em trong suốt bốn năm học qua. Cuối cùng, em xin gửi lời cảm ơn tới gia đình đình em. Nếu không có tình yêu, sự ủng hộ và động viên từ gia đình thì em sẽ không thể hoàn thành khoá luận và có được những kết quả như ngày hôm nay. Hà nội, 05/2009 Sinh viên Trần Bình Dương ii TÓM TẮT NỘI DUNG Kiểm thử đơn vị tham số hóa còn đang là một khái niệm mới mẻ đối với nhiều nhà phát triển phần mềm. Kiểm thử đơn vị tham số hóa đang dần đóng một vài trò hết sức quan trọng trong phát triển phần mềm. Khóa luận này ra đời chính là để nghiên cứu về phương pháp kiểm thử mới này và ứng dụng nó cho mục đích kiểm thử các chương trình Java. Nội dung khóa luận tập trung vào việc áp dụng khả năng của một nền kiểm chứng Java bytecode mã nguồn mở rất hiệu quả và phổ biến hiện nay là Java PathFinder để xây dựng một hệ thống hỗ trợ kiểm thử đơn vị tham số hóa cho mục đích kiểm thử các chương trình Java. Kết quả của khóa luận là đã xây dựng được một hệ thống để thực thi các ca kiểm thử đơn vị tham số hóa viết cho các chương trình Java đơn giản. Bên cạnh đó, khóa luận cũng đã trình bày một cách sâu sắc về kiểm thử đơn vị tham số hóa và những kỹ thuật phức tạp đằng sau phương pháp kiểm thử mới này cũng như một số nghiên cứu liên quan. Qua đó khóa luận kết thúc bằng việc phác thảo một số hướng có thể phát triển tiếp để hệ thống này xử lý được các kiểu dữ liệu phức tạp hơn. iii MỤC LỤC LỜI CẢM ƠN .....................................................................................................................i TÓM TẮT NỘI DUNG.....................................................................................................ii MỤC LỤC..........................................................................................................................iii CÁC KÝ HIỆU VIẾT TẮT .............................................................................................v DANH MỤC HÌNH VẼ ...................................................................................................vi Chương 1: Kiểm thử đơn vị tham số hóa ......................................................................3 1.1. Kiểm thử phần mềm .................................................................................................3 1.2. Kiểm thử đơn vị........................................................................................................4 1.3. Kiểm thử đơn vị tham số hóa...................................................................................6 1.3.1. Khái niệm...........................................................................................................6 1.3.2. Mối quan hệ giữa UT và PUT ..........................................................................7 1.3.3. Kiểm thử đơn vị tham số hóa với Pex ..............................................................8 1.3.4. Các mẫu kiểm thử tham số hóa ........................................................................9 1.3.5. Lựa chọn đầu vào kiểm thử với Pex...............................................................10 Chương 2: Sinh dữ liệu kiểm thử tự động cho PUT ..................................................12 2.1. Thực thi tượng trưng ..............................................................................................13 2.1.1. Những khái niệm cơ bản .................................................................................13 2.1.2. Thực thi tượng trưng tĩnh................................................................................14 2.1.3. Thực thi tượng trưng động ..............................................................................17 2.2. Xây dựng ràng buộc ...............................................................................................23 2.2.1. Lưu trữ giá trị tượng trưng..............................................................................24 2.2.2. SE với các kiểu dữ liệu nguyên thủy..............................................................25 2.2.3. SE với đối tượng..............................................................................................28 2.2.4. SE với các lời gọi phương thức ......................................................................30 2.3. Sinh dữ liệu kiểm thử cho PUT .............................................................................31 Chương 3: Sinh ca kiểm thử tham số hóa với JPF.....................................................36 3.1. Kiến trúc của JPF ...................................................................................................36 3.2. Symbolic JPF..........................................................................................................40 3.2.1. Bộ tạo chỉ thị....................................................................................................40 3.2.2. Các thuộc tính ..................................................................................................41 3.2.3. Xử lý các điều kiện rẽ nhánh ..........................................................................42 3.2.4. Ví dụ.................................................................................................................43 3.2.5. Kết hợp thực thi cụ thể và thực thi tượng trưng ............................................47 iv 3.3. Sinh PUT với Symbolic JPF ..................................................................................48 3.4. Mở rộng Symbolic JPF ..........................................................................................53 3.4.1. Các phương pháp cũ........................................................................................53 3.4.2. Hướng mở rộng ...............................................................................................54 KẾT LUẬN.......................................................................................................................58 TÀI LIỆU THAM KHẢO ................................................................................................1 v CÁC KÝ HIỆU VIẾT TẮT CFG Control Flow Graph DSE Dynamic Symbolic Execution JPF Java PathFinder PC Path Condition PUT Parameterized Unit Test SE Symbolic Execution SET Symbolic Execution Tree TIS Test Input Selector UT Unit Test vi DANH MỤC HÌNH VẼ Hình 1: Mối quan hệ giữa UT và PUT...............................................................................8 Hình 2 : Cây thực thi tượng trưng ....................................................................................16 Hình 3: Cây thực thi tượng trưng được quản lý riêng.....................................................22 Hình 4 : Hệ thống kiểm thử tổng quát..............................................................................24 Hình 5: Gán giá trị tượng trưng cho tham số đầu vào.....................................................26 Hình 6: Thực thi tượng trưng với câu lệnh gán ...............................................................27 Hình 7: Thực thi tượng trưng với câu lệnh rẽ nhánh.......................................................28 Hình 8: Khởi tạo đối tượng làm đầu vào cho chương trình............................................29 Hình 9. Sinh ra các ràng buộc liên quan tới đối tượng ...................................................30 Hình 10: Thuật toán sinh dữ liễu kiểm thử ......................................................................32 Hình 11: Các cây thực thi cục bộ tương ứng với hàm abs và TestAbs ..........................34 Hình 12: Kiến trúc JPF......................................................................................................37 Hình 13: Bộ sinh lựa chọn trong JPF ...............................................................................39 Hình 14. Bộ tạo chỉ thị trong JPF .....................................................................................40 Hình 15. Trạng thái chương trình thực thi trong Symbolic JPF .....................................41 Hình 16: Bùng nổ việc thực thi tượng trưng trong Symbolic JPF..................................48 Hình 17: Kiến trúc hệ thống cài đặt .................................................................................49 Hình 18. Một ví dụ với hệ thống cài đặt ..........................................................................52 1 MỞ ĐẦU Trong nền kinh tế hiện nay, ngành công nghiệp phần mềm giữ vai trò hết sức quan trọng. Với một số nước có nền công nghệ thông tin phát triển thì ngành công nghiệp phần mềm có khả năng chi phối cả nền kinh tế. Tuy nhiên để đảm bảo chất lượng cho các phần mềm là một thách thức không nhỏ trong ngành công nghiệp phần mềm. Việc phát hiện và khắc phục các lỗi cho các phần mềm là một công việc đòi hỏi nhiều nỗ lực và chi phí trong phát triển phần mềm. Với những lĩnh vực ứng dụng ngày càng mở rộng của phần mềm hiện nay thì chất lượng phần mềm càng được quan tâm hàng đầu. Trong kỹ nghệ phần mềm thì kiểm thử chính là phương pháp dùng để phát hiện các lỗi của phần mềm. Trong đó kiểm thử đơn vị là giai đoạn đầu tiên trong quy trình kiểm thử. Kiểm thử đơn vị là một công việc bắt buộc trong phát triển phần mềm. Theo nghiên cứu của Micorosoft thì có tới 79% các nhà phát triển phần mềm phải viết các ca kiểm thử đơn vị để thực hiện việc kiểm thử phần mềm mức đơn vị. Rõ ràng kiểm thử đơn vị là một công việc nặng nhọc làm mất nhiều thời gian và chi phí trong phát triển phần mềm. Do đó có một phương pháp kiểm thử đơn vị mới đã ra đời giúp cải thiện phương pháp kiểm thử đơn vị truyền thống đó là kiểm thử đơn vị tham số hóa. Với kiểm thử đơn vị tham số hóa công sức giành cho việc kiểm thử phần mềm mức đơn vị đã được giảm đi đáng kể. Kiểm thử đơn vị tham số hóa giúp việc phát hiện các lỗi của phần mềm đạt hiệu quả cao hơn do đó nâng cao chất lượng của phần mềm. Kiểm thử đơn vị tham số hóa còn là một phương pháp kiểm thử đơn vị còn rất mới và nó mới chỉ được áp dụng trong môi trường .NET. Vì vậy việc nghiên cứu về kiểm thử đơn vị tham số hóa và ứng dụng nó là một nhu cầu cấp bách. Và khóa luận này ra đời chính là vì mục đích này. Nội dụng chính của khóa luận gồm 3 chương: Chương 1: Trình bày tổng quan về kiểm thử và làm rõ bản chất của kiểm thử đơn vị tham số hóa thông qua công cụ Pex của Microsoft. Chương 2: Nghiên cứu về phương pháp sinh dữ liệu làm đầu vào kiểm thử cho các ca kiểm thử đơn vị tham số hóa. Trong chương này ta cũng sẽ trình bày về một hệ thống kiểm thử tổng quát nhất dùng để thực thi các ca kiểm thử đơn vị tham số hóa viết cho ngôn ngữ Java. 2 Chương 3: Trong chương này ta sẽ nghiên cứu về một nền (framework) kiểm chứng Java bytecode mã nguồn mở rất phổ biến hiện nay đó là Java PathFinder và áp dụng khả năng của nó để xây dựng một nền thực thi các ca kiểm thử tham số hóa viết cho những chương trình Java đơn giản. Đồng thời ta cũng đề xuất giải pháp để có thể mở rộng Java PathFinder cho mục đích hoàn thiện nền kiểm thử mà ta đã xây dựng. 3 Chương 1: Kiểm thử đơn vị tham số hóa 1.1. Kiểm thử phần mềm Để đảm bảo một hệ thống phần mềm hoặc các thành phần của phần mềm làm việc như mong muốn là một thách thức lớn trong ngành công nghiệp phần mềm. Các phần mềm lỗi gây ra những tổn thất về kinh tế cũng như những hậu quả nghiêm trọng khác tùy thuộc vào lĩnh vực mà phần mềm được sử dụng. Do đó cần phải phát hiện và khắc phục các lỗi của phần mềm trước khi đem chúng vào sử dụng. Có các phương pháp khác nhau để phát hiện lỗi của phần mềm bao gồm kiểm tra mô hình (model checking)[4], các kỹ thuật phân tích tĩnh (static analysis)[24] và kiểm thử (software testing)[1]. Các kỹ thuật phân tích chương trình tĩnh thường đưa ra nhiều cảnh báo (warnings) không tương ứng với các lỗi thực sự. Các kỹ thuật kiểm thử phát hiện ra các lỗi thực sự nhưng thường không phát hiện ra được tất cả các lỗi do chỉ phân tích một số sự thực thi trong chương trình. Trong kiểm tra mô hình, một mô hình của hệ thống được tạo ra để hỗ trợ phân tích mọi sự thực thi có thể trong mô hình. Kiểm tra mô hình có thể kiểm chứng được rằng mô hình của hệ thống hoạt động chính xác trong tất cả trường hợp có thể. Kiểm tra mô hình phân tích hết mọi khía cạnh thực thi của chương trình và chỉ ra những sự vi phạm nhưng không chứng minh được chương trình sẽ được thực thi chính xác mà không có lỗi. Hạn chế của kiểm tra mô hình đó là không gian trạng thái của mô hình thường quá lớn do đó việc thám hiểm tất cả các trạng thái không phải lúc nào cũng thực hiện được. Kiểm thử chính là kỹ thuật được sử dụng phổ biến nhất để phát hiện và khắc phục các lỗi của phần mềm nhằm đảm bảo chất lượng của phần mềm. Chi phí giành cho việc kiểm thử chiếm khoảng 50% tổng chi phí trong phát triển phần mềm. Kiểm thử là một tiến trình quan trọng trong kỹ nghệ phần mềm. Kiểm thử đơn vị chính là bước đầu tiên trong quy trình kiểm thử đó. Có các kỹ thuật kiểm thử khác nhau được sử dụng như kiểm thử hộp trắng (white-box testing), kiểm thử hộp đen (black-box testing), kiểm thử hộp xám (gray-box testing). Các kỹ thuật kiểm thử đó được dựa trên 2 loại kiểm thử đó là kiểm thử chức năng (funcional testing) và kiểm thử cấu trúc (structured testing). Kiểm thử chức năng là loại kiểm thử dựa trên đặc tả chức năng của hệ thống, nó phát hiện các sai sót về chức năng mà không quan tâm tới cài đặt. 4 Kiểm thử cấu trúc là loại kiểm thử có nghiên cứu mã nguồn bằng việc phân tích thứ tự thực hiện các lệnh. 1.2. Kiểm thử đơn vị Kiểm thử đơn vị là một cộng việc quan trọng trong kỹ nghệ phần mềm. Kiểm thử đơn vị thường được áp dụng để kiểm tra việc cài đặt của các lớp hoặc phương thức. Để thực hiện việc kiểm thử đơn vị, các lớp kiểm thử được tạo ra. Các lớp kiểm thử này gồm các phương thức kiểm thử. Các phương thức kiểm thử là các phương thức không tham số có kiểu trả về là void chứa trong các lớp kiểm thử để kiểm tra các khía cạnh cài đặt khác nhau của chương trình. Mỗi phương thức kiểm thử trong các lớp kiểm thử biểu thị cho một ca kiểm thử đơn vị (UT). Có thể chia một phương thức kiểm thử ra làm 3 phần: Các giá trị đầu vào, dãy các lời gọi phương thức, và sự xác nhận (assertions). Kiểm thử thất bại nếu bất cứ sự xác nhận nào bị vị phạm hoặc có một ngoại lệ (exception) xảy ra. Ví dụ 1.1: Ta xét một phương thức kiểm thử được viết trong nền kiểm thử VSUnit. public void TestArrayList() { // exemplary data int capacity = 1; object element = null; // method sequence ArrayList list = new ArrayList(capacity); list.Add(element); // assertions Assert.IsTrue(list[0] == element); } Phương thức kiểm thử TestArrayList bắt đầu bằng việc gán giá trị 1 cho biến capacity và giá trị null cho biến element như là các giá trị đầu vào kiểm thử. Sau đó nó thực hiện một dãy các lời gọi phương thức, trước tiên là khởi tạo một đối tượng ArrayList với kích cỡ là capacity không chứa phần tử nào. ArrayList là một mảng động với kích cỡ có thể thay đổi. Tiếp theo nó chèn một đối tượng là element vào mảng. Và cuối cùng là xác nhận xem phần tử đầu tiên của mảng có bằng đối tượng vừa được chèn vào hay không. Việc cài đặt nhiều phương thức kiểm thử không đảm bảo rằng sẽ kiểm tra được hết mọi khía cạnh thực thi của chương trình. Với các chương trình có nhiều đường đi thực thi khác nhau thì việc thiếu xót các UT để kiểm tra một vài đường đi thực thi trong chương trình là điều thường xuyên xảy ra. Khi người lập trình thay đổi mã cài đặt của chương trình được kiểm thử thì nếu như các phương thức kiểm thử không được 5 cập nhật theo thì sẽ dẫn đến việc nhiều đường đi thực thi của chương trình sẽ không được kiểm thử. Các nền kiểm thử hỗ trợ viết các UT theo các cách khác nhau. Tuy nhiên, đa phần các nền kiểm thử đều cung cấp những dịch vụ (service) như sau: + Cung cấp thuộc tính để chỉ định các phương thức như là các UT. + Phát hiện và thực thi tự động các UT + Một runner với khả năng báo cáo (reporting). Một runner có thể là ứng dụng dòng lệnh (console) hoặc là giao diện tích hợp. Như trong nền kiểm VSUnit[29] cho môi trường .NET. Ta sử dụng thuộc tính [TestClass] để chỉ định một lớp là lớp kiểm thử, và [TestMethod] để chỉ định một phương thức như là một phương thức kiểm thử. Ngoài ra còn có các thuộc tính khác như [ExpectedException] để chỉ định phương thức kiểm thử ném ra ngoại lệ của một kiểu ngoại lệ cụ thể nào đó. Ví dụ 1.2: Giả sử có một lớp LuhnAlgorithm được cài đặt như sau: public static class LuhnAlgorithm { public static bool Validate(string number){ if (number == null) throw new ArgumentNullException(""); foreach (var c in number) if (!Char.IsDigit(c)) throw new ArgumentException(""); return false; } } Ta có thể viết một lớp kiểm thử chứa các UT để thực hiện việc kiểm thử lớp LuhnAlgorithm: [TestClass]// lớp chứa các unit test public class LuhnAlgorithmTest { [TestMethod] [ExpectedException(typeof(ArgumentNullException))] public void Test1() { LuhnAlgorithm.Validate(null); } [TestMethod] [ExpectedException(typeof(ArgumentException))] public void Test2() { LuhnAlgorithm.Validate("K50"); } 6 [TestMethod] public void Test3() { LuhnAlgorithm.Validate(“123”); } } Khi thực thi phương thức kiểm thử Test1 thì ngoại lệ ArgumentNullException được ném ra. Khi thực thi phương thức kiểm thử Test2 thì ArgumentException được ném ra. Rõ ràng là mỗi phương thức kiểm thử ở trên chỉ có thể kiểm tra việc thực thi của lớp LuhnAlgorithm theo một nhánh đi cụ thể. Thực thi cả 3 phương thức kiểm thử ở trên ta sẽ kiểm tra được tất cả các trường hợp thực thi của lớp LuhnAlgorithm. Với một chương trình có nhiều đường đi thì ta cần viết các UT khác nhau để kiểm tra sự thực thi của chương trình theo các đường đi đó. Tuy nhiên, với những chương trình có nhiều đường đi thực thi khác nhau thì việc viết các UT như thế đòi hỏi nhiều thời gian và công sức để tính các giá trị đầu vào thích hợp và khó có thể kiểm tra hết được sự thực thi của chương trình theo tất cả các đường đi. 1.3. Kiểm thử đơn vị tham số hóa Có rất nhiều các nền kiểm thử khác nhau như JUnit[33] cho Java, NUnit[34], VSUnit[29] cho .NET để thực thi các ca kiểm thử đơn vị. Tuy nhiên các nền kiểm thử này không hỗ trợ việc sinh tự động các ca kiểm thử đơn vị. Việc viết các ca kiểm thử đơn vị để thực thi tất cả các đường đi của một chương trình là một công việc nặng nhọc. Giải pháp để giảm công sức cho việc này đó là sử dụng ca kiểm thử đơn vị tham số hóa. Kiểm thử đơn vị tham số hóa[7, 11, 12] là phương pháp mới trong kiểm thử phần mềm. Kiểm thử đơn vị tham số hóa giúp cải thiện nỗ lực trong việc phát triển phần mềm. Về bản chất nó chính là sự mở rộng của phương pháp kiểm thử đơn vị truyền thống. 1.3.1. Khái niệm Các UT truyền thống là các phương thức kiểm thử không tham số. Ta có thể mở rộng các UT đó bằng cách cho phép truyền vào tham số cho các phương thức kiểm thử. Các ca kiểm thử tham số hóa (PUT) là sự mở rộng của các UT truyền thống. Các PUT là các phương thức kiểm thử cho phép nhận các giá trị đầu vào kiểm thử khác nhau thông qua tham số đầu vào. 7 PUT được hiểu ở 2 khía cạnh: + PUT là sự đặc tả về hành vi bên ngoài của chương trình. Nếu như mỗi UT kiểm tra sự thực thi của chương trình với những giá trị đầu vào được chọn trước và xác nhận kết quả của lần thực thi đó có như mong đợi. Nói cách khác, mỗi UT biểu thị cho một hành vi thực thi cụ thể của chương trình. UT chỉ cung cấp các giá trị đầu vào cụ thể cho chương trình và xác nhận kết quả thực thi của chương trình với những đầu vào cụ thể đó mà không quan tâm tới quá trình thực thi của chương trình với những giá trị đó diễn ra như thế nào. Vì thế, UT biểu thị cho hành vi bên ngoài của chương trình. PUT cũng xác nhận về hành vị thực thi của chương trình nhưng được mở rộng cho tất cả các giá trị đầu vào có thể. Sự xác nhận (assertion) của PUT biểu thị cho các hành vi bên ngoài của chương trình. Ở khía cạnh này, PUT giống như sự đặc tả hộp đen (black-box) cho lớp được PUT kiểm thử. + Sự lựa chọn các đầu vào kiểm thử cho PUT dẫn đến việc phân tích chương trình được kiểm thử. Việc phân tích này cần tìm ra các giá trị sao cho khi chương trình được thực thi với các giá trị đó thì có nhiều dòng lệnh được chạy (code coverage)[5]. Nói cách khác, các giá trị cần được lựa chọn sao cho PUT có thể kiểm tra được các đường đi thực thi khác nhau của chương trình. Và mỗi UT có thể được sinh ra từ PUT bằng cách gọi PUT với mỗi đầu vào cụ thể được chọn. Ở khía cạnh này, PUT là kiểm thử hộp trắng (white-box). Từ đặc tả về PUT, ta có thể phát biểu vấn đề kiểm thử như sau: Cho một chương trình P gồm các câu lệnh S, cần tính toán một tập hợp các đầu vào (inputs) I sao cho với tất cả các câu lệnh cần thực thi s trong S, tồn tại đầu vào i trong I để P(i) thực thi s. 1.3.2. Mối quan hệ giữa UT và PUT Với mỗi chương trình có mã nguồn ta có thể viết các PUT để mô tả các hành vi thực thi của nó. Tuy nhiên, nếu đã có các UT được viết thì ta có thể tái cấu trúc mã cài đặt các UT đó để biến chúng thành các PUT. Ngược lại, từ các PUT ta có thể sinh lại các UT bằng cách truyền các giá trị cụ thể làm đầu vào cho PUT. Các nền kiểm thử đơn vị khác nhau hỗ trợ viết các UT theo các cách khác nhau. Do đó các PUT cũng cần được viết sao cho có thể sinh ra các UT tương ứng với các nền kiểm thử đó. 8 Hình 1: Mối quan hệ giữa UT và PUT 1.3.3. Kiểm thử đơn vị tham số hóa với Pex Pex[30] là công cụ mạnh mẽ hỗ trợ việc viết và thực thi các ca kiểm thử tham số hóa cho môi trường .NET. Ví dụ 1.3: Ca kiểm thử tham số hóa sử dụng Pex : Cũng như với UT, ta có thể viết các lớp kiểm thử chứa các ca kiểm thử tham số hóa. Với sự hỗ trợ của Pex ta có thể thực thi các ca kiểm thử tham số hóa đó. Tuy nhiên không giống việc thực thi các lớp kiểm thử chứa các UT, Pex chỉ thực thi được một ca kiểm thử tham số hóa trong mỗi lần chạy. [PexMethod] // exemplary data public void PutArrayList(ArrayList list, object element) { // assumptions PexAssume.IsTrue(list != null); // method sequence int len = list.Count; list.Add(element); // assertions PexAssert.IsTrue(list[len] == element); } Ca kiểm thử tham số hóa ở trên là sự mở rộng của UT trong ví dụ 1.1. Rõ ràng các giá trị đầu vào của UT trong ví dụ 1.1 là các giá trị cụ thể đã được chuyển thành các tham số đầu vào của phương thức. Nếu như UT trong ví dụ 1.1 kiểm thử phương thức Add của lớp ArrayList ở khía cạnh là khi chèn một đối tượng có giá trị null vào một ArrayList rỗng thì đối tượng được chèn vào trở thành phần tử đầu tiên của ArrayList. Thì với ca kiểm thử tham số hóa ở trên phương thức Add được kiểm thử với những đối tượng và ArrayList khác. Các ArrayList làm đầu vào kiểm thử có thể là ArrayList không chứa phần tử nào hoặc ArrayList đã chứa một số phần tử, hoặc ArrayList đã chứa đủ số phần tử so với kích cỡ được cấp phát thì khi chèn một đối tượng object có giá trị là null hay các giá trị khác thì đối tượng được chèn vào trở thành phần tử cuối cùng của ArrayList. 9 PUT có thể sử dụng các giả thuyết (assumptions) để giảm kích cỡ miền giá trị của tham số đầu vào. Các tham số đầu vào có giá trị thỏa mãn giả thuyết này mới được xem xét làm đầu vào kiểm thử. Như với PUT ở trên thì chỉ các ArrayList khác null mới được lựa chọn làm đầu vào kiểm thử. Khi Pex thực thi ca kiểm thử tham số hóa ở trên sẽ sinh ra Test Suite gồm 2 VSUnit UT. Đồng thời Pex cũng báo cáo về kết quả xác nhận của ca kiểm thử tham số hóa ở trên. [TestMethod] public void TestAddNoOverflow() { PutArrayList(new ArrayList(1), new object()); } [TestMethod] public void TestAddWithOverflow() { PutArrayList(new ArrayList(0), new object()); } Với ca kiểm thử tham số hóa này phương thức Add của lớp ArrayList được kiểm thử với tất cả các trường hợp thực thi có thể xảy ra. Thuộc tính [PexClass] của Pex để xác định một lớp kiểm thử là lớp chứa các ca kiểm thử tham số hóa. Thuộc tính [PexMethod] để chỉ định một phương thức kiểm thử là ca kiểm thử tham số hóa. Ta muốn viết một lớp kiểm thử chứa các ca kiểm thử tham số hóa cần sử dụng thuộc tính [PexClass] và [PexMethod] để viết các ca kiểm thử tham số hóa. 1.3.4. Các mẫu kiểm thử tham số hóa Viết các ca kiểm thử tham số hóa là một nghệ thuật. Để viết các ca kiểm thử tham số hóa hiệu quả, ta cần thực sự hiểu về mã cài đặt của chương trình mà ta muốn kiểm thử. Pex hỗ trợ nhiều mẫu kiểm thử tham số hóa khác nhau[15]. Các mẫu được sử dụng nhiều nhất đó là mẫu AAA (Triple-A) và AAAA: + Với mẫu AAA (Arrange, Act, Assert) PUT được tổ chức thành 3 phần:  Arrange: khởi tạo giá trị các biến sẽ sử dụng  Act: dãy các lời gọi phương thức  Assert: sự xác nhận + Với mẫu AAAA, một giả thuyết (Assume) được thêm vào để giới hạn miền giá trị của các tham số đầu vào. 10 Ví dụ 1.4: Mẫu kiểm thử tham số hóa AAAA [PexMethod] void AssumeActAssert(ArrayList list, object item) { // assume PexAssume.IsNotNull(list); // arrange var count = list.Count; // act list.Add(item); // assert Assert.IsTrue(list.Count == count + 1); } 1.3.5. Lựa chọn đầu vào kiểm thử với Pex Thêm tham số vào UT cải thiện đặc tả về hành vi mong muốn nhưng lại mất đi các ca kiểm thử cụ thể. Ta cần những giá trị thực sự cho các tham số đầu vào để sinh lại các ca kiểm thử cụ thể. PUT sẽ không thể thực thi nếu không có các giá trị cụ thể được truyền vào cho các tham số đầu vào của PUT. Để có thể sinh các đầu vào cụ thể cho PUT. Pex cần phải phân tích chương trình mà PUT kiểm thử. Có 2 kỹ thuật phân tích chương trình đó là phân tích tĩnh và phân tích động: + Phân tích tĩnh (static analysis): Kiểm chứng một tính chất nào đó của chương trình bằng việc phân tích tất cả các đường đi thực thi. Kỹ thuật này coi các cảnh bảo (violations) là các lỗi (error). + Phân tích động (dynamic analysis): Kiểm chứng một tính chất bằng việc phân tích một số đường đi thực thi. Đây là một kỹ thuật phân tích động hỗ trợ việc phát hiện ra các lỗi (bugs) nhưng không khẳng định được rằng có còn những lỗi khác hay không. Các kỹ thuật này thường không tìm ra được tất cả các lỗi. Pex cài đặt một kỹ thuật phân tích chương trình bằng cách kết hợp cả hai kỹ thuật phân tích chương trình ở trên gọi là thực thi tượng trưng động[14, 25]. Về bản chất Pex là một công cụ hỗ trợ kỹ thuật kiểm thử hộp trắng (white-box testing). Tương tự như kỹ thuật phân tích chương trình tĩnh, Pex chứng minh được rằng một tính chất được kiểm chứng trong tất cả các đường đi khả thi. Pex chỉ báo cáo (reporting) về các lỗi thực sự như với kỹ thuật phân tích chương trình động. 11 Pex sử dụng khả năng của bộ xử lý ràng buộc Z3[31] kết hợp với các lý thuyết toán học khác như hàm chưa định nghĩa, lý thuyết mảng, bit-vetor[2] để giải quyết ràng buộc sinh ra trong quá trình thực thi tượng trưng động và sinh ra các đầu vào kiểm thử cụ thể cho PUT. 12 Chương 2: Sinh dữ liệu kiểm thử tự động cho PUT Trong kiểm thử phần mềm, các ca kiểm thử thường được tạo ra thủ công do đó gây tốn kém trong chi phí phát triển phần mềm và làm kéo dài thời gian để hoàn thành một phần mềm. Có các phương pháp khác nhau hỗ trợ việc sinh tự động các ca kiểm thử một cách có hệ thống giúp giảm chi phí cho việc kiểm thử phần mềm. Một trong những phương pháp đơn giản nhất để sinh tự động các ca kiểm thử đó là kiểm thử ngẫu nhiên (random testing)[5]. Với kiểm thử ngẫu nhiên các đầu vào cho hệ thống được sinh ngẫu nhiên. Để thực hiện, một luồng các bits được sinh ngẫu nhiên để thể hiện cho các giá trị của tham số đầu vào. Giả sử với một hàm nhận tham số đầu vào có kiểu string thì chỉ cần sinh ngẫu nhiên một luồng các bits để thể hiện giá trị cho một chuỗi. Kiểm thử ngẫu nhiên có ưu điểm là dễ dàng sinh các đầu vào ngẫu nhiên và hệ thống kiểm thử ngẫu nhiên không yêu cầu nhiều tài nguyên bộ nhớ lúc thực thi. Nhưng hạn chế của nó là kiểm tra cùng một hành vị thực thi của chương trình nhiều lần với những đầu vào khác nhau và chỉ có thể kiểm tra được một số trường hợp thực thi của chương trình. Thêm vào đó, kiểm thử ngẫu nhiên khó xác định được khi nào việc kiểm thử nên được dừng lại và nó không biết tại điểm nào không gian trạng thái đã được thám hiểm hết. Để xác định khi nào việc kiểm thử dừng lại thì hệ thống kiểm thử ngẫu nhiên được kết hợp với các adequacy criterion [5]. Giả sử adequacy criterion là bao phủ lệnh (statement coverage)[5] thì việc kiểm thử chỉ dừng lại khi tất cả các câu lệnh của chương trình được thực thi ít nhất một lần. Một phương pháp khác đang rất phổ biến giúp khắc phục được hạn chế của kiểm thử ngẫu nhiên đó là thực thi tượng trưng[6]. Thực thi tượng trưng chính là việc xây dựng các ràng buộc dựa vào các giá trị tượng trưng và giải quyết các ràng buộc đó để sinh ra các giá trị làm đầu vào chương trình mà có thể thực thi chương trình theo các đường đi thực thi khác nhau. Ý tưởng chính của thực thi tượng trưng đó là thực thi một chương trình với những giá trị tượng trưng. Có hai cách tiếp cận đối với thực thi tượng trưng đó là cách tiếp cận dựa trên phân tích tĩnh và phân tích động chương trình. Việc lựa chọn các đầu vào kiểm thử cho PUT liên quan tới vấn đề sinh dữ liệu kiểm thử tự động. Sinh dữ liệu kiểm thử tự động là một lĩnh vực nghiên cứu rất rộng trong kiểm thử phần mềm. Có rất nhiều các kỹ thuật khác nhau[8, 10, 18] được sử dụng để sinh dữ liệu kiểm thử tự động. Tuy nhiên với PUT thì các dữ liệu làm đầu vào kiểm thử cần được chọn lựa làm sao để PUT có thể kiểm tra được sự thực thi của 13 chương trình theo tất cả các đường đi có thể. Hơn nữa số lượng các đầu vào kiểm thử cho PUT là tối thiểu. Việc sinh dữ liệu để có thể kiểm tra được sự thực thi một chương trình theo tất cả các đường đi có thể với các dữ liệu đó là một vấn đề phức tạp và không phải lúc nào cũng thực hiện được trên thực tế. Thực chất của vấn đề sinh dữ liệu kiểm thử tự động cho PUT là việc xây dựng ràng buộc và xử lý ràng buộc. Các ràng buộc được xây dựng sao cho chúng có thể biểu thị cho các đường đi thực thi trong một chương trình. Và giải quyết các ràng buộc đó sẽ sinh ra các dữ liệu mà chương trình có thể thực thi với các dữ liệu đó để đi theo các đường đi khác nhau trong chương trình. 2.1. Thực thi tượng trưng 2.1.1. Những khái niệm cơ bản Một chương trình P có thể xem xét như một hàm, P : S→ R , trong đó S là tập hợp các đầu vào (input) có thể và R là tập hợp các đầu ra (output) có thể. S có thể được biểu diễn bởi vector I=(x1,…,xk,…,xn), trong đó xk là tham số đầu vào thứ k của P với k  N. Một bộ giá trị i=(d1,...,dk,…,dn) biểu thị cho một đầu vào của P, i  S, trong đó dk là các giá trị cụ thể sao cho dk  Dxk với Dxk là miền giá trị của tham số đầu vào xk. Sự thực thi của chương trình P với đầu vào i  S được biểu thị bởi P(i). Biểu đồ luồng điều khiển (CFG) của một chương trình P là một bộ G=(N, E, s, e), trong đó G là một đồ thị có hướng, với N là tập hợp các nút (node), E = {(n,m) | n,m  N} là tập hợp các cạnh, s là nút vào và e là nút ra, s và e là duy nhất. Mỗi nút được định nghĩa như một khối cơ bản (basic block) là một dãy liên tục các chỉ thị(câu lệnh) sao cho luồng điều khiển khi đi vào nút và ra khỏi nút không bị ngưng lại (halt). Điều này có nghĩa là nếu bất cứ câu lệnh nào của block được thực thi thì toàn bộ block được thực thi. Mỗi cạnh của CFG nối 2 nút với nhau và được gán nhãn với một biểu thức điều kiện rẽ nhánh. Nếu cạnh không được gán nhãn có nghĩa là điều kiện luôn đúng. Một đường đi (path) cụ thể là dãy các nút: p=(p1, p2,…,pn) với pn là nút cuối của đường đi p và (pi,pi+1)  E (1 < i < n-1). Nếu tồn tại i  S sao cho sự thực thi P(i) đi theo đường đi p thì p gọi là đường đi khả thi, ngược lại p là đường đi không khả thi. Một đường đi bắt đầu tại nút vào và kết thúc tại nút ra gọi là đường đi đầy đủ, nếu kết thúc tại nút không phải là nút ra thì gọi là đường đi không đầy đủ (path segment). Một chương trình P cũng có thể xem gồm tập hợp các câu lệnh (statements) là thành phần nhỏ nhất trong một chương trình mà có thể được thực thi riêng rẽ. Bằng việc thực thi một câu lệnh chương trình có thể chuyển đổi trạng thái thực thi của nó từ 14 trạng thái hiện thời tới trạng thái mới. Một đường đi thực thi của chương trình P là một dãy các câu lệnh mà có thể được thực thi theo thứ tự từ điểm bắt đầu của chương trình. Đoạn đường đi đầu tiên (path prefix) có độ dài n của đường đi thực thi p là một dãy bao gồm n câu lệnh đầu tiên của p. Do đó việc sinh dữ liệu kiểm thử cho PUT là việc sinh một tập hợp tối thiểu các đầu vào i Є S sao cho có thể thực thi tất cả các đường đi trong CFG của chương trình được PUT kiểm thử. 2.1.2. Thực thi tượng trưng tĩnh Ý tưởng chính của thực thi tượng trưng (SE)[6] là thực thi chương trình với các giá trị tượng trưng (symbolic values) thay vì các giá trị cụ thể (concrete values) của các tham số đầu vào. Với mỗi tham số đầu vào một giá trị tượng trưng được đưa ra để kết hợp với nó. Mỗi biến trong chương trình P mà giá trị của nó phụ thuộc vào giá trị của các tham số đầu vào thì trong quá trình thực thi tượng trưng một giá trị tượng trưng sẽ được tính toán để kết hợp cùng với nó. Mỗi giá trị tượng trưng biểu thị cho một tập hợp các giá trị cụ thể mà một biến hoặc một tham số đầu vào có thể nhận. Kết quả trả về của một chương trình được thực thi tương trưng nếu có cũng được biểu thị bởi biểu thức của các giá trị tượng trưng. Giá trị tượng trưng của biến x có thể được biểu thị bởi: (a). Một ký hiệu đầu vào(input symbol). (b). Một biểu thức kết hợp giữa các giá trị tượng trưng bởi các toán tử. (c). Một biểu thức kết hợp giữa giá trị tượng trưng và giá trị cụ thể bởi toán tử. Một ký hiệu đầu vào biểu thị cho giá trị tượng trưng của một tham số đầu vào lúc bắt đầu thực thi chương trình. Các tham số đầu vào khác nhau của P được biểu thị bởi các ký hiệu đầu vào khác nhau. Các toán tử (operator) là các phép toán như cộng (+), trừ (), nhân (*), chia (/). Nếu giá trị của một biến x không phụ thuộc vào các giá trị đầu vào thì không có giá trị tượng trưng nào được tính toán để kết hợp với nó. Giá trị tượng trưng cuả các biến và các tham số đầu vào được cập nhật như các giá trị cụ thể của nó trong quá trình thực thi. Gán một giá trị cụ thể từ một biến tới biến khác dẫn đến giá trị tượng trưng cũng được sao chép nếu biến được gán tới một biến khác có một giá trị tượng trưng. 15 Giả sử với một câu lệnh gán x=e, nếu e là một tham số đầu vào, thì giá trị tượng trưng được gán cho x sẽ có dạng (a). Nếu e là một biểu thức tính toán gồm các toán hạng. Các toán hạng đó có thể là biến, tham số đầu vào hoặc hằng thì giá trị tượng trưng của biến x sẽ là một biểu thức tượng trưng dạng (b) nếu mỗi toán hạng trong biểu thức có một giá trị tượng trưng kết hợp với nó, hoặc là một biểu thức tượng trưng dạng (c) nếu có toán hạng là hằng số hoặc không có giá trị tượng trưng kết hợp với nó. Giá trị cụ thể của một hằng hoặc một biến cũng được sử dụng trong biểu thức tượng trưng nếu như hằng hoặc biến đó không có giá trị tượng trưng kết hợp với nó. Trạng thái của một chương trình được thực thi tương trưng bao gồm các giá trị của các biến trong chương trình, điều kiện đường đi (PC) và biến đếm chương trình (program counter). Biến đếm chương trình xác định chỉ thị (câu lệnh) tiếp theo sẽ được thực thi. Mỗi PC là một biểu thức kết hợp bởi các ràng buộc mà các giá trị đầu vào chương trình cần thỏa mãn để chương trình được thực thi theo đường đi tương ứng với PC đó. Mỗi ràng buộc là một biểu thức tượng trưng dạng x o y trong đó x là giá trị tượng trưng, y là giá trị tượng trưng hoặc giá trị cụ thể và o  {≤, ≠, =, , ≥}. Các ràng buộc đó chính là biểu thức của điều kiện rẽ nhánh và biểu thức phủ định của điều kiện rẽ nhánh tương ứng với nhánh true và nhánh false. Tại mỗi câu lệnh rẽ nhánh, các ràng buộc được tạo ra. Các ràng buộc này được biểu thị bởi biểu thức của các giá trị tượng trưng hay biểu thức của giá trị tượng trưng và giá trị cụ thể phụ thuộc vào biến xuất hiện trong biểu thức điều kiện của câu lệnh rẽ nhánh có giá trị tượng trưng được tính toán để kết hợp với nó hay không. Trong quá trình thực thi tượng trưng, việc chương trình được thực thi theo một đường đi cụ thể nào đó không phụ thuộc vào các giá trị cụ thể của các biến và các tham số đầu vào. Tại các điểm rẽ nhánh, cả hai nhánh ra sẽ được xem xét để điều hướng sự thực thi hiện thời đi theo. SE chủ yếu liên quan tới việc thực thi hai loại câu lệnh đó là câu lệnh gán (assignment statments) và câu lệnh rẽ nhánh. Tại các câu lệnh gán thì giá trị tượng trưng của các biến chương trình cũng như các tham số đầu vào có liên quan tới câu lệnh gán đó được cập nhật. Tại các câu lệnh rẽ nhánh, chương trình sẽ được điều hướng để thực thi theo cả hai nhánh. Và hai ràng buộc đường đi tương ứng với hai nhánh sẽ được tạo ra. Một ràng buộc là biểu thức điều kiện tại câu lệnh rẽ nhánh. Còn ràng buộc kia là phủ định của biểu thức điều kiện rẽ nhánh. Các ràng buộc này sẽ được cập nhật vào điều kiện đường đi tương ứng với các nhánh đó. Đồng thời các PC này sẽ được đánh giá để xác định đường đi tương ứng với PC đó có khả thi. Nếu PC được đánh giá trở thành false thì SE sẽ quay lui và chỉ thực thi theo nhánh khả 16 thi. Các PC được tạo ra bằng cách thu gom các ràng buộc trên các đường đi tương ứng và giải quyết các ràng buộc này sẽ sinh ra các giá trị cụ thể cho các tham số đầu vào. Để mô tả sự thực thi tượng trưng một chương trình. Một cây thực thi tượng trưng (SET) được đưa ra để biểu thị cho các đường đi thực thi trong quá trình thực thi tượng trưng một chương trình. Các nút biểu thị cho các trạng thái của chương trình được thực thi tượng trưng và các cạnh biểu thị cho sự chuyển đổi trạng thái từ trạng thái này sang trạng thái khác. Ví dụ 2.1: public void Swap(int x, int y){ 1: if (x > y) { 2: x = x + y; 3: y = x - y; 4: x = x - y; 5: if (x - y > 0) 6: assert(false); } Hình 2 : Cây thực thi tượng trưng Cây thực thi tượng trưng (Hình 2) biểu thị cho việc thực thi tượng trưng hàm Swap. Bắt đầu thực thi tượng trưng hàm Swap bằng cách gán giá trị tượng trưng cho các tham số đầu vào x và y lần lượt là X và Y, đồng thời khởi tạo PC là true. Tới câu lệnh rẽ nhánh 1, cả hai nhánh đi của chương trình đều chọn để thực thi với các giá trị tượng trưng. Tại câu lệnh này, biểu thức điều kiện rẽ nhánh và biểu thức phủ định của điều kiện rẽ nhánh được thêm vào PC theo các nhánh tương ứng. Trong thực thi tượng 17 trưng, nếu điều kiện rẽ nhánh được thêm vào PC thì PC đó tương ứng với PC của nhánh mà điều kiện rẽ nhánh nhận giá trị true. Sau khi thực thi câu lệnh 1, hàm Swap tiếp tục được thực thi theo nhánh mà điều kiện rẽ nhánh ở câu lệnh 1 nhận giá trị true. Khi thực thi các câu lệnh gán 2, 3, 4 thì giá trị của các biến được cập nhật với giá trị mới. Khi tới câu lệnh rẽ nhánh 5, thêm 2 nhánh đi mới được xem xét để thực thi với các giá trị tượng trưng. PC tiếp tục được cập nhật theo các nhánh tương ứng. Tại đây, PC được cập nhật với điều kiện rẽ nhánh ở 5 trở thành false do không tồn tại bộ giá trị nào thỏa mãn PC. Vì vậy hàm Swap chỉ thực thi theo nhánh mà PC được cập nhật với biểu thức phủ định của điều kiện rẽ nhánh tại 5. Và câu lệnh 6 sẽ không bao giờ được thực thi. Tại mỗi điểm rẽ nhánh, PC được cập nhật và một bộ xử lý ràng buộc được sử dụng để xác định nhánh tương ứng với PC đó có khả thi hay không để điều hướng việc thực thi hiện thời đi theo nhánh đó . Nếu PC được đánh giá tới false thì SE sẽ quay lui và chỉ thực thi chương trình theo nhánh mà PC được đánh giá tới true. 2.1.3. Thực thi tượng trưng động Thực thi tượng trưng động[14, 25] là kỹ thuật thực thi tương trưng dựa trên phân tích chương trình động. Thực thi tượng trưng động chính là sự kết hợp giữa thực thi cụ thể và thực thi tượng trưng. Trong thực thi tượng trưng động, chương trình được thực thi nhiều lần với những giá trị khác nhau của tham số đầu vào. Bắt đầu bằng việc chọn những giá trị tùy ý cho các tham số đầu vào và thực thi chương trình với những giá trị cụ thể đó. Với những giá trị cụ thể này thì chương trình sẽ được thực thi theo một đường đi xác định. Thực thi chương trình với các giá trị cụ thể của tham số đầu vào và thu gom các ràng buộc trong quá trình thực thi theo đường đi mà sự thực thi cụ thể này đi theo, đồng thời suy ra các ràng buộc mới từ những ràng buộc đã thu gom được. Tại các câu lệnh rẽ nhánh, biểu thức điều kiện rẽ nhánh sẽ được đánh giá phụ thuộc vào các giá trị cụ thể của các tham số đầu vào. Nếu biểu thức điều kiện rẽ nhánh nhận giá trị là True thì biểu thức của điều kiện rẽ nhánh sẽ được thu gom vào ràng buộc của PC và được ghi nhớ, đồng thời phủ định của điều kiện rẽ nhánh sẽ được sinh ra và được thêm vào một PC tương ứng với nhánh còn lại mà sự thực thi cụ thể đó không đi theo. Một bộ xử lý ràng buộc (Constraint Solver) sẽ được sử dụng để giải quyết các ràng buộc mới sinh ra này để sinh ra các giá trị cụ thể của tham số đầu vào. Ngược lại, nếu là False thì biểu thức phủ định của điều kiện rẽ nhánh sẽ được thu gom 18 vào ràng buộc của PC tương ứng với nhánh đi mà sự thực thi hiện thời đang đi theo và được ghi nhớ. Đồng thời điều kiện rẽ nhánh sẽ được sinh ra và thêm vào PC tương ứng với nhánh đi còn lại mà sự thực thi hiện thời không đi theo. Các giá trị mới được sinh ra của các tham số đầu vào sẽ tiếp tục được thực thi và quá trình này sẽ được lặp lại cho tới khi chương trình được thực thi theo tất cả các đường đi. Do các chương trình được thực thi với những giá trị cụ thể nên có thể thấy rằng tất cả các đường đi phân tích được trong quá trình thực thi tượng trưng động đều là các đường đi khả thi. Thuật toán 2.1: DSE S : Tập hợp tất cả các câu lệnh của chương trình P S : Tập con của S (s S) I : Tập hợp các đầu vào của P P(i): Thực thi chương trình với đầu vào i  I, sao cho s được thực thi J : Tập hợp các đầu vào của P được thực thi (J={i | P(i)}) C(i): Ràng buộc thu gom được từ việc thực thi P(i), hay còn gọi là điều kiện đường đi C’(i): Điều kiện đường đi suy ra từ C(i) Bước 0: J:= {} (tập rỗng) Bước 1: Chọn đầu vào i không thuộc J (dừng lại nếu không có i nào được tìm ra) Bước 2: Output i Bước 3: Thực thi P(i); ghi nhớ điều kiện đường đi C(i), suy ra C’(i) Bước 4: Đặt J := J  i Bước 5: Quay lại bước 1 Ví dụ 2.2: 0:void DSE(int[] a) 1:{ 2: if (a == null) return; 3: if (a.length > 0) 4: if (a[0] == 123456789) 5: throw new Exception("bug"); 6:} Solve (c): Biểu thị cho việc xử lý ràng buộc c. Hàm DSE bắt đầu được thực thi với giá trị tùy ý của tham số đầu vào. Giá trị tùy ý này thường được chọn là giá trị mặc định tương ứng với kiểu của tham số đầu vào. Ở đây giá trị null được chọn, sau đó thực thi hàm DSE với giá trị null này. Khi tới câu lệnh rẽ nhánh 2, điều kiện a==null được thỏa mãn do đó ràng buộc C(i):(a==null) được ghi nhớ. Ràng buộc C’(i) được suy ra bằng cách lấy phủ định của điều kiện rẽ nhánh, C’(i): (a!=null). Solve (C’(i)) suy ra được a={}. 19 Tiếp tục thực thi chương trình với giá trị a={}. Với a={} khi tới câu lệnh rẽ nhánh 3, biểu thức a.length > 0 nhận giá trị false, ràng buộc C(i): (a!=null) && !(a.length >0) được ghi nhớ. Ràng buộc C’(i):(a!=null && a.length > 0) được sinh ra, solve (C’(i)) ta được giá trị mới của tham số đầu vào là {0}. Tiếp tục thực thi hàm DSE với giá trị a={0}. Với giá trị a={0} khi đi tới câu lệnh rẽ nhánh 4, thì biểu thức điều kiện rẽ nhánh nhận giá trị false đo đó ràng buộc C’(i):( a!=null && a.length>0 && a[0]!=123456789) được ghi nhớ. Điều kiện C’(i): (a!=null && a.length>0 && a[0]==123456789) được sinh ra, solve (C’(i)) ta được giá trị a={12345678}. Đến đây thì không còn đường đi nào của hàm DSE mà chưa được thực thi và qua trình thực thi sẽ được dừng lại. Bảng 1: Ví dụ về thực thi tượng trưng động Ràng buộc C’(i) Input i Ràng buộc được ghi nhớ C(i) null a = = null a!=null {} a!=null && !(a.length>0) a!=null&& a.length>0 {0} a!=null && a.length>0 && a[0]!=123456789 a!=null && a.length>0 && a[0]!=123456789 {123456789} a!=null && a.length>0 && a[0]!=123456789 Một số hệ thống sinh kiểm thử tự động cài đặt DSE bằng cách khởi tạo một cây thực thi tương trưng để biểu thị các đường đi thực thi khác nhau. Nếu như có thể xây dựng được một cây thực thi tượng trưng đầy đủ thì có thể sinh ra các giá trị đầu vào sao cho có thể đạt được sự bao phủ luồng điều khiển (CFG coverage)[5] ở mức cao. Với những hệ thống này, mã nguồn chương trình cần được sửa đổi để cho phép thực thi tượng trưng được thực hiện dọc theo việc thực thi cụ thể. Chương trình được thực thi với những giá trị ngẫu nhiên với một chiều sâu (depth) định trước của SET. Chiều sâu được sử dụng để giúp cho việc thực thi một chương trình được dừng lại trong trường hợp chương trình có vòng lặp vô tận hoặc các hàm đệ quy. Khi chương trình bắt đầu được thực thi thì một cây thực thi tương trưng tương ứng cũng được khởi tạo. Trong quá trình thực thi, các giá trị tượng trưng của các biến sẽ đươc tính toán và các ràng buộc đường đi sẽ được sinh ra từ các giá trị tượng trưng đó. Với mỗi ràng buộc được sinh ra thì SET sẽ được thêm vào một đỉnh (node) tương ứng với ràng buộc đó. Việc xây dựng SET tiến hành trong suốt quá trình thực thi. Có thể xem mỗi lần thực thi là mỗi lần duyệt một đường đi của SET. Formatted: Indent: First line: 0 pt Formatted: Indent: First line: 0 pt Formatted: Indent: First line: 0 pt Formatted: Indent: First line: 0 pt Formatted: Indent: First line: 0 pt 20 Khi các câu lệnh rẽ nhánh được thực thi, các đường đi trong SET cũng được mở rộng theo các nhánh đó. Với những giá trị cụ thể việc thực thi sẽ đi theo một nhánh cụ thể. Nhánh còn lại mà sự thực thi cụ thể đó không đi theo sẽ có một đỉnh mới được tạo ra và được đánh dấu là chưa được thăm. Đỉnh mới được tạo ra sẽ lưu các ràng buộc tương ứng với nhánh mà đỉnh đó được thêm vào. Sau mỗi lần thực thi, một đỉnh mà chưa được thăm trong SET sẽ được chọn và ràng buộc đường đi tương ứng với đoạn đường đi từ đỉnh gốc (root) của SET tới đỉnh được chọn đó sẽ được thu gom và ràng buộc đường đi này sẽ được đưa tới một bộ xử lý ràng buộc (Constraint Solver) để xử lý. Nếu ràng buộc đường đi này không thỏa mãn, một đỉnh khác của SET mà chưa được thăm sẽ được chọn, còn nếu ràng buộc đường đi này thỏa mãn thì bộ xử lý ràng buộc sẽ sinh ra các giá trị đầu vào cụ thể cho lần thực thi tiếp theo. Khi các đỉnh tương ứng với các nhánh trong SET đều được thăm hết thì thuật toán sẽ tạm dừng (terminate). Và các giá trị đầu vào cụ thể được sinh ra cùng với những thông tin phân tích được trong mỗi lần thực thi (method summary) sẽ được sử dụng để sinh ra các UT và cho mục đích báo cáo. Các giá trị đầu vào cụ thể được trả về sau mỗi lần chạy được kết hợp với các thông tin về lỗi phát hiện được nếu lần thực thi đó chương trình ngưng lại vì một ngoại lệ chưa được xử lý, hoặc vì một lỗi nào đó. Ví dụ 2.3: Thực thi tượng trưng với phương thức nhận đầu vào là đối tượng Ta xét một phương thức nhận 2 tham số đầu vào, một tham số là đối tượng SimpleList và một tham số có kiểu int: Class SimpleList { public int value ; public List next ; .../* other methods */ } 21 1: void Simple(SimpleList o, int x){ 2: x=x+5; 3: if(x > 0) 4: o.value=x; 5: else 6: o=null; 7: if(o.next==o) 8: error(); 9:} Với những phương thức nhận tham số đầu vào có kiểu đối tượng thì kỹ thuật khởi tạo lười[29] được sử dụng trong việc thực thi tượng trưng phương thức đó. Giả sử các giá trị ngẫu nhiên được chọn là x=-10, o=null. Các giá trị tượng trưng được gán tương ứng tới các tham số đầu vào cùng với những giá trị cụ thể được chọn ở trên. S(x)=sym, R(o)=obj1. Thực thi chương trình với giá trị của các tham số đầu vào được chọn ngẫu nhiên này. Sau khi thực thi câu lệnh 2, giá trị tượng trưng của x là S(x)=sym+5, giá trị cụ thể của nó cũng được tính toán (x = -5). Tới câu lệnh rẽ nhánh 3, với giá trị x= -5 thì điều kiện rẽ nhánh được đánh giá tới false. Ràng buộc S(x)=sym+5 <= 0 lưu vào đỉnh tương ứng của SET cho nhánh mà sự thực thi cụ thể đi theo và được đánh dấu là đã được thăm, đồng thời một đỉnh mới đại diện cho nhánh còn lại được tạo ra và ràng buộc sym+5 > 0 được lưu vào đỉnh này, đỉnh mới được tạo ra được đánh dấu là chưa được thăm. Đến câu lệnh 7 thì một ngoại lệ NullPointerException được ném ra và việc thực thi sẽ dừng lại. Cây thực thi tượng trưng được xây dựng tương ứng với lần chạy này (Hình 3(a)). Đỉnh mới được tạo ra của SET mà chưa được thăm được chọn để thu gom ràng buộc trên nhánh tương ứng với đỉnh chưa được thăm đó. Ràng buộc thu gom được là sym+5 > 0. Giải quyết ràng buộc này ta được một giá trị cụ thể của x giả sử là x=0. Do không có ràng buộc liên quan tới đối tượng l được tạo ra nên giá trị của nó sẽ được khởi tạo với phương thức khởi tạo mặc định cho lần thực thi tiếp theo. Sau khi khởi tạo đối tượng o và giải quyết ràng buộc, chương trình tiếp tục được thực thi với các giá trị đầu vào mới này đó là x=0, o=new simpleList(). Đỉnh chưa 1 void Simple(SimpleList o, int x){ 2 x=x+5; 3 if(x > 0) 4 o.value=x; 5 else 6 o=null; 7 if(o.next==o) 8 error(); 9} 22 được thăm tương ứng với nhánh thực thi này tạo ra từ lần thực thi trước trong SET sẽ được chọn để mở rộng. Đến câu lệnh 4, trường value của đối tượng o được truy cập lần đầu tiên. Một giá trị tượng trưng sẽ được kết hợp với nó, và giá trị tượng trưng này được cập nhật do giá trị của trường đó được gán với giá trị của biến x. Tới câu lệnh 7, một đối tượng o.next sẽ được khởi tạo lười với một giá trị cụ thể và một giá trị tượng trưng kết hợp với nó, o.next=new simpleList(), R(o.next)=obj2. Tại câu lệnh rẽ nhánh này, 2 ràng buộc tương ứng với 2 nhánh được tạo ra obj1=obj2, và obj1≠obj2. Ràng buộc obj1≠obj2 tương ứng với nhánh mà sự thực thi cụ thể hiện thời đang đi theo. Với ràng buộc obj1=obj2 thì một đỉnh mới được tạo ra tương ứng với nhánh mà sự thực thi cụ thể hiện thời không đi theo để lưu ràng buộc obj1=obj2 và đỉnh mới này được đánh dấu là chưa được thăm. Cây thực thi tượng trưng tương ứng với lần thực thi này được biểu thị trong Hình 3(b). Sau khi lần chạy này kết thúc đỉnh mới được tạo ra này lại được chọn để mở rộng và ràng buộc thu gom được trên đường đi chứa đỉnh này là S(x)=sym+5 > 0 && obj1=obj2 && S(o.value)= sym+5. Ràng buộc đối tượng obj1=obj2 được giải quyết bằng phép gán tham chiếu giữa 2 đối tượng mà các giá trị tượng trưng này đại diện, o.next=o. Đối tượng o lúc này được khởi tạo và giá trị của trường value được gán với giá trị sinh ra từ việc giải quyết ràng buộc. Cây thực thi tương trưng tương ứng với lần thực thi chương trình với các giá trị đầu vào mới sinh ra này được biểu thị trong Hình 3(c). Hình 3: Cây thực thi tượng trưng được quản lý riêng 23 2.2. Xây dựng ràng buộc Các công cụ như Pex[30], CUTE[9] được cài đặt dựa trên kỹ thuật thực thi tượng trưng động. Tuy nhiên, cần có cơ chế để cho phép một chương trình có thể thực thi tượng trưng. Để thực thi tượng trưng một chương trình thì mã nguồn của chương trình đó cần được sửa đổi (instrumented) để hỗ trợ việc thực thi tượng trưng. Với một số công cụ như JCUTE[9] thì các chương trình Java được chuyển đổi thành một dạng ngôn ngữ có cấu trúc đơn giản hơn và thêm vào các phần mã hỗ trợ việc thực thi tượng trưng với ngôn ngữ trung gian này. Dạng ngôn ngữ trung gian thường được sử dụng cho ngôn ngữ Java đó là Jimple[17]. Bảng 2 dưới minh họa việc mã nguồn Java được chuyển thành dạng mã Jimple. Bảng 2. Minh họa việc chuyển đổi từ mã nguồn Java sang mã Jimple Mã nguồn Java Mã Jimple void call(int x){// bắt đầu hàm begin x = input; if (x > 0) { x = 1; } else { x = -1; } y = x + y; if (x <= 0) goto L1; x = 1; if (true) goto L2; L1: x = -1; L2: y = x + y; switch (c) { case 1: x = x + 1; break; case 2: x = x - 1; break; default: x = 0; break; } x = x + c; if (c != 1) goto L1; x = x + 1; if (true) goto L3; L1: if (c != 2) goto L2; x = x - 1; if (true) goto L3; L2: x =0; L3: x = x + c; sum = i = 0; while (i < 10) { sum = sum + i; i++; } i = sum; sum = 0; i = 0; L1: if (i >= 10) goto L2; sum = sum + i; i = i + 1; if (true) goto L1; L2: i = sum; } // kết thúc hàm End Việc chuyển đổi mã Java sang mã có cấu trúc đơn giản hơn giúp quá trình thêm các phần mã hỗ trợ việc thực thi tượng trưng dễ dàng hơn. Tuy nhiên, các công cụ như thế cần sử dụng các cộng cụ và các nền (framework) khác để giúp chuyển lại các mã trung gian đó về dạng Java chuẩn. Giả sử với mã Jimple ở trên sau khi đã thêm vào các 24 phần mã hỗ trợ thực thi tượng trưng thì công cụ Soot[17] được sử dụng để chuyển chúng về dạng Java bytcode chuẩn. Việc thực thi tượng trưng một chương trình được biểu thị bằng cây thực thi tượng trưng. Do đó một số hệ thống cài đặt thực thi tượng trưng xây dựng và quản lý cây thực thi tượng trưng riêng để mô tả quá trình thực thi tượng trưng một chương trình. Và các ràng buộc trên các đường đi của cây thực thi tượng trưng được quản lý sẽ được thu gom và giải quyết bởi bộ xử lý ràng buộc để sinh ra các đầu vào kiểm thử. Cộng cụ Pex cũng xây dựng và quản lý cây thực thi tượng trưng để sinh các đầu vào cho PUT. Ví dụ 2.3 ở trên chính là một minh họa về hệ thống như thế. Hình 4 : Hệ thống kiểm thử tổng quát Kiến trúc tổng quát của hệ thống kiểm thử sử dụng kỹ thuật thực thi tượng trưng được minh họa như Hình 4. Trong đó Test Input Selector (TIS) làm nhiệm vụ quản lý cây thực thi tượng trưng và sinh các đầu vào để Test Executor thực thi chương trình đã được sửa đổi để hỗ trợ việc thực thi tượng trưng với mỗi đầu vào được sinh ra đó. 2.2.1. Lưu trữ giá trị tượng trưng Với các hệ thống kiểm thử mà cài đặt kỹ thuật thực thi tượng trưng ở trên thì cần có các cấu trúc dữ liệu để lưu trữ các giá trị tượng trưng kết hợp với các biến và tham số đầu vào trong quá trình thực thi tượng trưng một chương trình. Nếu kiểu của biến x không phải là kiểu tham chiếu thì giá trị tượng trưng của x biểu thị bởi S(x). S’= S[x → s] biểu thị cho ánh xạ từ biến x tới giá trị tượng trưng s của nó được bổ sung vào S, từ đó S’(x)=s. S’=S-x được sử dụng để biểu thị rằng ánh xạ giữa biến x và giá trị tượng trưng đã được gỡ bỏ. S’(x) trong trường hợp này trả về giá trị cụ thể cho x mà không phải là giá trị tượng trưng. R(o) biểu thị cho giá trị tượng trưng của đối tượng o. R là một ánh xạ giữa đối tượng và giá trị tượng trưng của nó tương tự như S. Ngoài ánh xạ S và R một ánh xạ M cũng được sử dụng. Các ánh xạ S, R, M được cài đặt bằng cấu trúc dữ liệu dạng Map dùng để lưu trữ các cặp giá trị key→value. Địa chỉ bộ nhớ (memory address) là các định danh duy nhất sử dụng như 25 key mà các giá trị tượng trưng có thể ánh xạ tới. Tuy nhiên, trong Java ta không thể truy cập tới các con trỏ và địa chỉ bộ nhớ. Tên của biến được sử dụng là key trong trường hợp kiểu của biến đó không phải là kiểu tham chiếu. Tuy nhiên tên biến thường không phải là duy nhất do đó các ánh xạ được cài đặt bằng việc thêm một biến tượng trưng mới cho mỗi biến cục bộ hoặc mỗi trường của đối tượng trong quá trình sửa đổi mã nguồn của chương trình được kiểm thử. Bằng kỹ thuật phân tích dựa trên kiểu[22] có thể xác định các câu lệnh và các biến liên quan tới các tham số đầu vào để có thể thêm vào phần mã cho chúng để hỗ trợ việc thực thi tượng trưng. Các giá trị tượng trưng được kết hợp với các biến chứ không phải với giá trị của các biến. Trong Java không thể có hai biến có kiểu không phải là kiểu tham chiếu cùng trỏ tới một địa chỉ bộ nhớ. Với một số đối tượng, có thể có nhiều tham chiếu (reference) tới cùng một đối tượng. Tuy nhiên với đối tượng ta cũng có thể dùng các tham chiếu là key. Vì thế ánh xạ R được cài đặt bằng một cấu trúc dữ liệu dạng Map mà ánh xạ một tham chiếu tới một giá trị tượng trưng. Khi một giá trị tượng trưng của một đối tượng được yêu cầu, một tham chiếu tới đối tượng được tìm kiếm trong R và giá trị tượng trưng ánh xạ tới tham chiếu được trả về nếu tham chiếu được tìm thấy. 2.2.2. SE với các kiểu dữ liệu nguyên thủy Để thực thi tương trưng một chương trình thì mã nguồn của chương trình cần được thêm vào các phần mã cho phép việc thực thi tượng trưng. Mỗi câu lệnh trong chương trình đó sẽ được xử lý một lần tại một thời điểm và mã thực hiện việc thực thi tượng trưng sẽ được thêm vào câu lệnh đó nếu cần thiết. Mỗi tham số đầu vào v của chương trình được thay thế bằng một câu lệnh đầu vào tượng trưng getInput(v). Và chương trình sẽ gọi các câu lệnh đầu vào tượng trưng này như là các tham số đầu vào. Mỗi lần trước khi bắt đầu thực thi một lệnh, phần thực thi tượng trưng của chương trình sẽ được khởi tạo. Trong quá trình khởi tạo, một kết nối được thiết lập với bộ lựa chọn dữ liệu kiểm thử (TIS). TIS sinh ra một dãy các giá trị cụ thể để làm đầu vào cho chương trình. Các giá trị đầu vào nhận được từ TIS được lưu vào một bộ nhớ I. I là một ánh xạ cài đặt bởi cấu trúc dữ liệu Map, ánh xạ mỗi tham số đầu vào tới một giá trị đầu vào cụ thể. Nói cách khác bộ nhớ I có thể xem như một dãy các giá trị đầu vào được sắp xếp theo thứ tự. Ví dụ khi câu lệnh đầu vào tượng trưng đầu tiên được thực thi thì giá trị đầu tiên của dãy được sử dụng. Nếu một số tham số đầu vào của chương trình không được thay thế với câu lệnh đầu vào tượng trưng thì chương trình sẽ không được thực thi theo đường đi mong đợi. 26 Mỗi câu lệnh getInput(v) là một phương thức được cài đặt để thực hiện việc gán một giá trị đầu vào cụ thể và giá trị tượng trưng cho tham số đầu vào. Lúc bắt đầu thực thi giá trị tượng trưng của tham số đầu vào được gán bằng một ký hiệu đầu vào duy nhất và nó được đưa tới TIS để giá trị tượng trưng này đại diện cho giá trị đầu vào cụ thể mới. Với các giá trị đầu vào cụ thể, ta cần kiểm tra xem có còn các giá trị cụ thể trong I chưa được chọn để thực thi. Nếu không một giá trị được sinh ngẫu nhiên sẽ được sử dụng. getInput(v) 1: S[v→ si]; // si is a new symbolic value 2: i = i + 1; 3: report(S(v) = si); 4: if (inputNumber є domain(I)) 5: result = I(inputNumber); 6: else 7: result = a random value; 8: inputNumber = inputNumber + 1; 9: return result ; Hình 5: Gán giá trị tượng trưng cho tham số đầu vào Với mọi câu lệnh gán, các giá trị tượng trưng của biến cũng cần được cập nhật với các giá trị mới. Khi một giá trị cụ thể được gán tới một biến, giá trị tượng trưng kết hợp với biến đó được gỡ bỏ nếu có một giá trị tượng trưng như thế tồn tại. Với câu lệnh gán dạng v=v1 nếu v1 có giá trị tượng trưng kết hợp cùng thì chỉ cần sao chép nguyên giá trị tượng trưng của v1 cho v. Trường hợp v=v1 op v2, với op là một phép toán số học thì việc gán là khá phức tạp. Đầu tiên op được kiểm tra xem có được hỗ trợ bởi bộ xử lý ràng buộc đang sử dụng. Nếu op không được hỗ trợ bởi bộ xử lý ràng buộc, việc gán được thực thi cụ thể và giá trị tượng trưng của v được gỡ bỏ. executeAssignment(v, e) 1: match (e) 2: case c: /* c is a contant value */ 3: S = S − v; 4: case v1: /* v1 is a variable */ 5: if (v1 є domain(S)) 6: S = S[v → S(v1)]; 7: else 8: S = S − v; 9: case v1 op v2: 10: if (op {+, −, ∗, /}) 11: S = S − v; 12: else if (v1 Є domain(S) && v2 Є domain(S)) 27 13: S[v → si]; 14: i = i + 1; 15: report(S(v) = S(v1) op S(v2)); 16: else if (v1 Є domain(S)) 17: S[v → si]; 18: i = i + 1; 19: report(S(v) = S(v1) op v2); 20: else if (v2 є domain(S)) 21: S[v → si]; 22: i = i + 1; 23: report(S(v) = v1 op S(v2)); 24: else 25: S = S − v; Hình 6: Thực thi tượng trưng với câu lệnh gán Thực thi tượng trưng cho câu lệnh rẽ nhánh được thực hiện như sau. Trước tiên cần xác định nhánh đi mà thực thi cụ thể đi theo và sau đó một ràng buộc đường đi được lưu trữ tới đỉnh tương ứng của SET (Hình 7). Cần kiểm tra xem các giá trị tượng trưng có được kết hợp với các biến xuất hiện trong biểu thức điều kiện rẽ nhánh hay không. Nếu chỉ có giá trị cụ thể của biến được sử dụng, TIS không cần được thông báo, việc thực thi câu lệnh không ảnh hưởng tới SET mà TIS đang quản lý. Nếu giá trị tượng trưng được sử dụng thì ràng buộc đường đi tương ứng với cả hai nhánh sẽ được đưa tới TIS. Đỉnh thuộc nhánh mà sự thực thi cụ thể hiện thời đi theo sẽ được đánh dấu là đã thăm và đỉnh tương ứng với nhánh còn lại được đánh dấu là chưa được thăm để tiếp tục mở rộng. Chú ý rằng, ở dòng 2 thông tin của nhánh được với tới trong sự thực thi cụ thể hiện thời được lưu vào một bit-vertor. Bit-vertor chứa tất cả lựa chọn biểu thị cho các nhánh đã chọn và được đưa tới TIS khi phương thức report được gọi. Phương thức report làm nhiệm vụ gửi các thông tin về ràng buộc và các lựa chọn tới TIS để khởi tạo các đỉnh của SET tương ứng với ràng buộc đó. Một chương trình có thể có một vòng lặp vô tận, do đó việc thực thi phải dừng ở một chiều sâu định trước. Vòng lặp trong mã nguồn Java được biến đổi thành câu lệnh goto hoặc một lời gọi đệ quy trong ngôn ngữ trung gian Jimple[17]. executeCondition(op v1 v2) 1: branchTaken = evaluate(v1 op v2); 2: constructBranchBitvector(branchTaken); 3: if (v1 є domain(S) && v2 є domain(S)) 4: report(S(v1) op S(v2), branchTaken); 5: else if (v1 є domain(S)) 6: report(S(v1) op v2, branchTaken); 7: else if (v2 є domain(S)) 8: report(S(v2) op v1, branchTaken); 28 Hình 7: Thực thi tượng trưng với câu lệnh rẽ nhánh 2.2.3. SE với đối tượng Trong phần này, ta sẽ trình bày quá trình sửa đổi mã nguồn của chương trình để cho phép thực thi tượng trưng được mở rộng cho chương trình nhận đầu vào là đối tượng. Bảng 3 bên dưới minh họa việc thêm mã hỗ trợ việc thực thi tượng trưng đối với câu lệnh liên quan tới đối tượng. Bảng 3: Sửa đổi chương trình với câu lệnh liên quan tới đối tượng Trước khi sửa đổi Sau khi sửa đổi o = input; o = getSymbolicObject(o); v = o.field; lazyInitialize(o); executeAssignment(v,o.field); v = o.field; o.field = e; lazyInitialize(o); executeAssignment(o.field,e); o.field = e; if o1 op o2 goto l; executeObjectCondition(op,o1,o2); if o1 op o2 goto l; Với các câu lệnh gán sử dụng tham chiếu tới đối tượng thì không cần thêm phần mã để thực thi tượng trưng câu lệnh đó. Việc xử lý với các biến có kiểu tham chiếu và các biến có kiểu không phải là kiểu tham chiếu là khác nhau. Ví dụ với câu lệnh x=5 và y=null, x là biến kiểu integer và y là biến kiểu tham chiếu. Câu lệnh gán thứ nhất thay thế giá trị tại vị trí bộ nhớ mà biến x được lưu trữ. Nếu một giá trị tượng trưng được kết hợp với vị trí bộ nhớ, việc gán ảnh hưởng tới giá trị được lưu trong đó và cũng ảnh hưởng tới giá trị tượng trưng. Câu lệnh gán thứ hai, giá trị của y không phải là một đối tượng mà là một tham chiếu tới một đối tượng. Điều đó có nghĩa là khi y đươc gán bằng null, nó không thay đổi đối tượng nó tham chiếu. Việc gán các tham chiếu tới đối tượng cho một biến không làm thay đổi các giá trị tượng trưng của các đối tượng mà tham chiếu đó trỏ tới. Nói rộng hơn, không thể thay thế hay xóa một đối tượng được lưu trong vùng nhớ heap trong máy ảo java. Việc loại bỏ các đối tượng lưu trong vùng nhớ heap được thực hiện bởi bộ thu gom rác (Garbage Collector) Thực thi tượng trưng với chương trình nhận đầu vào là đối tượng phức tạp hơn rất nhiều so với đầu vào có kiểu không phải là kiểu tham chiếu. Sự khác nhau với đầu vào có kiểu không tham chiếu đó là với đầu vào kiểu không tham chiếu ta có thể dễ dàng gán một giá trị cụ thể tới một biến nhưng với đầu vào kiểu đối tượng thì không có giá trị cụ thể như thế được đưa ra để gán cho biến. TIS ở hệ thống như trên gửi một địa chỉ logic tới đối tượng đầu vào. Một địa chỉ logic là một số tự nhiên sao cho giá trị 0 là một giá trị đặc biệt tương ứng với tham chiếu null (null reference). Khi TIS muốn 2 đối tượng giống nhau. Nó đưa cho chúng 2 địa chỉ logic giống nhau tới ánh xạ I. Ví 29 dụ nếu bộ nhớ I tương ứng với một dãy (1,0,1,2) thì lời gọi 1 và 3 tới phương thức getSymbolicObject (Hình 8) sẽ trả về tham chiếu tới cùng một đối tượng. Lời gọi 2 sẽ đưa ra một tham chiếu null và lời gọi 4 sẽ trả về tham chiếu tới đối tượng khác với các lời gọi trước. Để có thể trả về một tham chiếu tới đối tượng được tạo. Một ánh xạ từ địa chỉ logic tới đối tượng cụ thể được quản lý. Ánh xạ này gọi là M. Phương thức (Hình 8) khởi tạo các đối tượng tượng trưng làm đầu vào cho chương trình. Đầu tiên kiểm tra xem có một giá trị đầu vào được sử dụng tại điểm thực thi hiện hành. Nếu ánh xạ I chứa một giá trị tương ứng với địa chỉ logic của một đối tượng. Nếu địa chỉ logic tương ứng với tham chiếu null thì giá trị null là kết quả trả về. Ngược lại nó kiểm tra (dòng 5) nếu đối tượng yêu cầu đã được khởi tạo bằng việc tìm kiếm một tham chiếu tới đối tượng trong M. Nếu tham chiếu được tìm thấy nó trả về như kết quả còn nếu không một đối tượng mới được tạo và ánh xạ từ địa chỉ logic tới đối tượng vừa được tạo mới được thêm vào M. Một giá trị tượng trưng objj cũng được kết hợp với đối tượng được tạo. Giá trị j là số lần chạy được sử dụng để ngăn chặn các ký hiệu đầu vào giống nhau được sử dụng nhiều lần. Nếu ánh xạ I không chứa một địa chỉ logic để được sử dụng, một đối tượng mới được tạo ra và một giá trị tượng trưng được kết hợp với nó. Chú ý trong trường hợp này, không có địa chỉ logic được ánh xạ tới đối tượng. Và bất cứ đối tượng mới được trả về bởi getSymbolicObject được tạo đơn giản bằng lớp khởi tạo mặc định của đối tượng. Có nghĩa là các trường của đối tượng không được khởi tạo với các giá trị tượng trưng bởi câu lệnh này. getSymbolicObject(o) 1: if (inputNumber Є domain(I)){ 2: l = I(inputNumber); 3: if (l == 0) 4: result = null; 5: else if (l Є domain(M)) 6: result = M(l); 7: else{ 8: result = new object of type o; 9: R = R[result→ objj]; 10: M = M[l → result]; } 11: }else{ 12: result = new object of type o; 13: R = R[result → objj]; } 14: inputNumber = inputNumber + 1; 15: j = j + 1; 16: return result ; Hình 8: Khởi tạo đối tượng làm đầu vào cho chương trình 30 Trong khởi tạo lười các đối tượng vừa được khởi tạo được ghi nhớ để tránh phải khởi tạo nhiều lần. Các trường của đối tượng được khởi tạo như các đầu vào tượng trưng hoặc có thể thêm một phương thức vào lớp của đối tượng và làm việc khởi tạo. Với các đối tượng mà các trường của nó có kiểu dữ liệu nguyên thủy thì các trường đó được khởi tạo với các giá trị tượng trưng. Tuy nhiên, khi đối tượng có cấu trúc phúc tạp, thì đối tượng được khởi tạo bằng việc chỉ định một số trường của đối tượng khởi tạo với giá trị tượng trưng, một số trường phức tạp khác thì khởi tạo với giá trị cụ thể. Phương thức khởi tạo cần truy cập tới các trường public và private của đối tượng. Trong công cụ khác như JCUTE[9] tất cả các đối tượng làm đầu vào được khởi tạo như một tham chiếu null lần đầu tiên chúng gặp phải trong mỗi lần thực thi và chúng được khởi tạo với các giá trị ngẫu nhiên nếu một ràng buộc yêu cầu chúng là khác null. Phương thức (Hình 9) thực hiện việc thực thi tương trưng câu lệnh rẽ nhánh và thu gom ràng buộc với đối tượng. Phương thức này so sánh các tham chiếu tới các đối tượng thay vì giá trị nguyên thủy. Các ràng buộc với đối tượng là o1=o2, o1≠o2, o1=null, o1≠null với o1 và o2 là các đối tượng tượng trưng. Phương thức thực hiện việc so sánh các đối tượng ở một trong các dạng kể trên và xác định nhánh ra của câu lệnh rẽ nhánh mà sự thực thi cụ thể hiện thời đi theo (dòng 2). Phương thức tạo ra ràng buộc dựa vào giá trị tượng trưng của đối tượng. Một tham chiếu null không có một giá trị tượng trưng kết hợp với nó, tham chiếu null được xử lý như một trường hợp đặc biệt (dòng 6 và 8). Các ràng buộc được tạo ra và nhánh mà sự thực thi cụ thể đi theo sẽ được TIS ghi nhớ. executeObjectCondition(op,o1,o2) 1: if (op Є {==,!=} ) 2: branchTaken = evaluate(o1 op o2); 3: constructBranchBitvector(branchTaken); 4: if (o1 Є domain(R) && o2 Є domain(R)) 5: report(R(o1) op R(o2), branchTaken); 6: else if (o1 Є domain(R) && o2 == null) 7: report(R(o1) op null, branchTaken); 8: else if (o2 Є domain(R) && o1 == null) 9: report(R(o2) op null, branchTaken); Hình 9. Sinh ra các ràng buộc liên quan tới đối tượng 2.2.4. SE với các lời gọi phương thức Trong Java, tất cả các đối số đưa tới phuơng thức bởi giá trị. Điều này có nghĩa rằng khi phương thức được gọi với các đối số có giá trị tượng trưng kết hợp với chúng thì các giá trị tượng trưng đó phải được kết hợp với các biến mới trong phương thức được gọi. Khi một phương thức được gọi, tất cả các giá trị tượng trưng của các đối số được đẩy vào (pushed) một ngăn xếp (stack). Và các giá trị của chúng được đọc từ 31 stack tới biến tượng trưng tương ứng tại thời điểm phương thức được gọi bắt đầu việc thực thi. Do khi một phương thức được thực thi tượng trưng thì kết quả thực thi được trả về nhiều lần do các phương thức được thực thi nhiều lần theo các đường đi khác nhau. Vì vậy một ngăn xếp được sử dụng để lưu các giá trị trả về của một phương thức được gọi. Tuy nhiên, với các lời gọi phương thức thì mã nguồn của phương thức được gọi cần được sửa đổi để cho phép thực thi tương trưng thì phương thức đó mới có thể thực thi tượng trưng với các giá trị tượng trưng được kết hợp với các đối số truyền vào phương thức. Vấn đề với các lời gọi phương thức đó là các phương thức được gọi thường không cho phép thực thi tượng trưng như việc gọi các thư viện trong Java, các phương thức mà mã nguồn của nó không sẵn có để ta có thể thêm vào các phần mã cho phép thực thi tượng trưng phương thức đó. Đây chính là hạn chế của phương pháp sửa đổi mã nguồn chương trình để cho phép thực thi tượng trưng chương trình đó. Tuy vậy, hiện nay Sun Microsystems đã công bố mã nguồn của nền Java(Java Platform) qua dự án OpenJDK[32] do đó việc sửa đổi các thư viện chuẩn của Java để hỗ trợ thực thi tượng trưng là điều có thể thực hiện được. 2.3. Sinh dữ liệu kiểm thử cho PUT Trong mục trước, ta đã trình bày về kiến trúc của một hệ thống kiểm thử sử dụng kỹ thuật thực thi tượng trưng động cũng như việc sửa đổi một chương trình để hỗ trợ việc thực thi tượng trưng động. Chương trình sau khi đã được sửa đổi để hỗ trợ thực thi tượng trưng sẽ đươc thực thi với những giá trị cụ thể. Như đã trình bày trong mục 2.1.3, ban đầu chương trình đã sửa đổi để hỗ trợ thực thi tượng trưng sẽ được thực thi với những giá trị được sinh ngẫu nhiên. Khi chương trình bắt đầu được thực thi lần đầu tiên thì một cây thực thi tượng trưng sẽ được khởi tạo và các đỉnh (node) của cây sẽ được sinh ra dựa vào các thông tin tượng trưng (các ràng buộc, giá trị tượng trưng của các đầu vào) thu được. Các đỉnh tương ứng với nhánh đi mà sự thực thi cụ thể đó đi theo sẽ được đánh dấu là đã thăm và các đỉnh mới được sinh ra tương ứng với các nhánh mà sự thực thi cụ thể không đi theo sẽ được đánh dấu là chưa được thăm. Sau khi lần thực thi đó kết thúc, thì TIS cần chọn ra những đỉnh mà được đánh dấu là chưa thăm để thu gom ràng buộc trên nhánh của cây thực thi chứa đỉnh đó và giải quyết ràng buộc đã thu gom được để sinh các giá trị cụ thể làm đầu vào cho lần thực thi tiếp theo. Quá trình sẽ được lặp lại cho tới khi không còn các đỉnh mới của cây thực thi được sinh ra mà được đánh dấu là chưa được thăm. Để có thể chọn ra được các đỉnh mà được đánh dấu là chưa thăm thì TIS cần sử dụng các kỹ thuật tìm kiếm khác nhau 32 như tìm kiếm theo chiều sâu (Depth-First Search), tìm kiếm theo chiều rộng (Breadth- First Search), tìm kiếm kinh nghiệm. Và các ràng buộc trên đoạn đường đi (path prefix) từ đỉnh gốc tới đỉnh được chọn đó sẽ được thu gom và giải quyết. Thuật toán (Hình 10) dưới đây mô tả việc TIS sinh ra các đầu vào cho chương trình dựa trên cây thực thi tượng trưng mà TIS quản lý. 1: T = newSET();// khởi tạo cây thực thi tượng trưng 2: S = chiến lược tìm kiếm; 3: while(T chưa được thăm hết){ //chọn được đỉnh n chưa được thăm bằng chiến lược S 4: m = n = S(T); 5: pc = true; 6: while (m ≠ T.root){ 7: pc = pc  m.constraint; 8: m = m.parent; 9: } inputs = solve(pc); 10: if(isSatisfied(inputs)){//tìm ra được inputs thỏa mãn 11: execute(inputs);//inputs đưa tới Test Executor để thực thi 12: expand(n);//chọn đỉnh n để mở rộng tiếp 13: if(có lỗi thực thi) 14: reportError(); 15: marked(n);// đánh dấu đỉnh n đã được thăm } Hình 10: Thuật toán sinh dữ liễu kiểm thử Tuy nhiên, việc lưu trữ cây thực thi tượng trưng tốn rất nhiều bộ nhớ. Do đó những đỉnh đã được đánh dấu là đã thăm mà không có đỉnh con cần được gỡ bỏ. Với Pex[30] thì các ràng buộc đường đi thu gom được không phải là dạng công thức logic đơn thuần như ta đã trình bày ở trên mà là dạng công thức logic bậc một (first-order logic fomulas)[2]. Chính nhờ việc xây dựng ràng buộc dạng này mà Pex có thể sử dụng một SMT solver (Z3) để xử lý các ràng buộc đó. Pex sinh dữ liệu kiểm thử cho PUT bằng việc xây dựng và quản lý các cây thực thi cục bộ (intraprocedural execution trees). 33 Ví dụ 2.5: Để hiểu rõ hơn về ràng buộc mà Pex xây dựng ta xét ví dụ 2.5 ở trên. Hàm TestAbs gọi một hàm khác là hàm abs. Các cây thực thi cục bộ tương ứng với mỗi hàm được minh họa trong Hình 11. Các cạnh của cây được gán nhãn bởi các ràng buộc và các đỉnh (node) của cây đại diện cho sự thực thi của một câu lệnh trong chương trình sao cho đường đi từ đỉnh gốc (root) của cây tới đỉnh lá (leaf) tương ứng với một đường đi thực thi cục bộ (intraprocedural path). Hình 11(a) là một phần của cây thực thi cục bộ tương ứng với hàm abs minh họa cho việc gọi hàm abs với giá trị x=1. Với cây thực thi cục bộ này ta làm quen với khái niệm là đỉnh treo (dangling node). Đỉnh treo là đỉnh đại diện cho đường đi chưa được thực thi. Đỉnh treo giống như đỉnh mới được tạo ra mà được đánh dấu là chưa được thăm như ta đã trình bày trong phần trước. Với kỹ thuật thực thi tượng trưng động[13, 19], việc thám hiểm có thể đạt tới đích (đỉnh treo) cho trước bằng thám hiểm lười (lazy exploration) và cố gắng tránh những đường đi mà không đạt tới đích bằng thám hiểm tin cậy (relevant exploration). Giả sử rằng ta gọi hàm TestAbs với p=1 và q=1. Sự thực thi này sẽ đi theo nhánh true của câu lệnh if đầu tiên trong hàm abs (đỉnh 3) cũng như nhánh false của câu lệnh if trong TestAbs (đỉnh 10). Hình 11(a) và (b) biểu thị cho cây thực thi cục bộ của hàm abs và TestAbs trong trường hợp này. Ta muốn sinh đầu vào cho hàm TestAbs để có thể thực thi câu lệnh xác nhận (đỉnh 11). Kỹ thuật này có thể tìm ra đầu vào để việc thực thi đạt tới đích (đỉnh 11) mà không cần phải thám hiểm các đường đi chưa được thám hiểm trong hàm mức thấp hơn (hàm abs). int abs (int x){ if( x > 0) return x; else if( x == 0) return 100; else return −x; } void TestAbs(int p,int q){ int m = abs(p); int n = abs(q); if(m > n && p > 0) assertfalse; } 34 Hình 11: Các cây thực thi cục bộ tương ứng với hàm abs và TestAbs Ràng buộc cục bộ (local path constraint) của một đỉnh n trong cây thực thi cục bộ Tf của hàm f được định nghĩa bằng ràng buộc đường đi của đường đi w từ đỉnh vào (entry node) của hàm f tới câu lệnh đại diện bởi n. Ràng buộc đường đi của đỉnh n (localpc(n)) biểu thị bởi các ký hiệu đầu vào fP của ƒ localpc(n):= lpcn  Dg( a ) với mỗi g( a ) xuất hiện trong lpcn Trong đó lpcn là biểu thức kết hợp của ràng buộc trên các cạnh của đường đi w từ gốc của cây thực thi cục bộ tới đỉnh n và Dg( a ) đại diện cho kết quả (function sumary) của hàm g được gọi bởi ƒ với đầu vào a mà xuất hiện trong lpcn. Khi hàm ƒ gọi hàm g trong thực thi tượng trưng thì giá trị trả về của lời gọi tới hàm g là một đầu vào tượng trưng của ƒ. Giá trị trả về của lời gọi tới hàm g được biểu thị bởi g( a ) với a là các đối số mà giá trị biểu thị bởi các ký hiệu đầu vào của ƒ. Nếu giá trị trả về được sử dụng trong câu lệnh rẽ nhánh của f thì g( a ) xuất hiện trong ràng buộc đường đi. Ký hiệu hàm g sẽ được hiểu như ký hiệu hàm chưa định nghĩa (uninterpreted function)[2] bởi bộ xử lý ràng buộc. Hàm chưa định nghĩa này được thông dịch bởi một dạng định đề (axiom)  x. g(x) = E[x], trong đó E[x] là một biểu thức liên quan tới biến x. Như ví dụ ở trên thì hàm abs có thể được định nghĩa như sau: x. abs(x) = ITE(x > 0, x, ITE(x = 0, 100,−x)), (ITE biểu thị cho if-then-else). Ta sử dụng definition-predicate Dg cho mỗi ký hiệu hàm để đại diện cho giá trị trả về của lời gọi hàm. Ta định nghĩa Dg bằng định đề (axiom) δg như sau: 35 δg=  Pg . Pg . Dg( Pg )  V localpc(l) Λ ret(l) leaf l in Tg trong đó ret(l)= Gl nếu l là đỉnh treo và ret(l)=Retg(l) trong trường hợp khác. Retg(l) đại diện cho giá trị trả về của g, đó là một biểu thức biểu thị bởi Pg , trên đường đi cục bộ đã được thám hiểm hết đại diện bởi đỉnh treo . Với mỗi đỉnh treo d thì Gd là một biến logic duy nhất đại diện cho d. Quay lại ví dụ trên, TestAbs thực thi với p=1,q=1 thì ràng buộc đường đi cục bộ của đỉnh n được gán nhãn 11 sẽ như sau: localpc(n):=abs(p) > abc(q) Λ p > 0 Λ Dabs(p) Λ Dabs(q) Với đầu vào trên thì chỉ đường đi với x > 0 mới được thám hiểm trong abs, có một đỉnh treo d (đỉnh 2) đại diện cho nhánh của câu lệnh điệu kiện mà chưa được thám hiểm. Dabs sau đó được định nghĩa bởi định đề δabs : δabs=  Dabs(x)  ITE((x > 0, abs(x) = x, Gd) Nếu tất cả các đường đi của abs đều được thám hiểm (Hình 11(b)): δabs=  Dabs(x)  (x ≤ 0 Λ x = 0 Λ abs(x) = 100) Λ (x ≤ 0 Λ x = 0 Λ abs(x) = −x)Λ (x > 0 Λ abs(x) = x) hay δabs = ITE(x ≤ 0, ITE(x = 0, abs(x) = 100, abs(x) = −x),abs(x) = x) 36 Chương 3: Sinh ca kiểm thử tham số hóa với JPF 3.1. Kiến trúc của JPF JPF[28] là một máy ảo Java (JVM) đặc biệt được sử dụng như một bộ kiểm tra mô hình (model checker) cho Java bytecode. JPF được sử dụng để phát hiện lỗi (bugs) trong các chương trình Java. JPF phân tích tất cả các đường đi thực thi của một chương trình Java để tìm ra sự vi phạm (violations) như deaklock hay các ngoại lệ chưa được xử lý. Khi JPF tìm ra một lỗi thì nó báo cáo về toàn bộ đường đi thực thi mà dẫn tới lỗi được phát hiện. Không giống như các trình gỡ rối (debugger) thông thường, JPF ghi nhớ về mọi bước phân tích dẫn đến một phát hiện lỗi. Có thể sử dụng JPF một cách linh hoạt dưới dạng giao diện dòng lệnh hoặc tích hợp vào trong các môi trường phát triển ứng dụng Java như Netbean, Eclipse. JPF là một ứng dụng Java mã nguồn mở cho phép ta cấu hình để sử dụng nó theo các cách khác nhau và mở rộng nó. Máy ảo JPF được cài đặt tuân theo các đặc tả về máy ảo Java nhưng không giống như các máy ảo Java chuẩn khác máy ảo JPF có khả năng lưu trữ trạng thái (state storing), ghi nhớ trạng thái (state matching) và quay lui trong quá trình thực thi chương trình. Quay lui (backtracking) có nghĩa là JPF có thể phục hồi lại trạng thái thực thi lúc trước để xem có còn những sự lựa chọn thực thi khác. Ghi nhớ trạng thái (state matching) có nghĩa là đánh dấu các trạng thái đã thám hiểm mà không còn cần thiết nữa giúp JPF tránh được những sự thực thi không cần thiết. Trạng thái thực thi của một chương trình bao gồm heap và ngăn xếp tiến trình. Trong khi thực thi JPF kiểm tra mọi trạng thái mới có phải là các trạng thái đã được ghi nhớ. Nếu các trạng thái đã được ghi nhớ JPF sẽ không tiếp tục đi theo đường đi thực thi hiện hành và quay lui tới trạng thái gần nhất mà chưa được thám hiểm. Với những chương trình lớn và phức tạp thì không gian trạng thái trong quá trình thực thi chương trình là rất lớn. Việc lưu trữ và thám hiểm tất cả các trạng thái không phải lúc nào cũng đạt được. JPF sử dụng các kỹ thuật khác nhau để giải quyết vấn đề này đó là các chiến lược tìm kiếm, các kỹ thuật để giảm thiểu số trạng thái chương trình và việc lưu trữ các trạng thái. Có các chiến lược tìm kiếm khác nhau được sử dụng như tìm kiếm theo chiều sâu (Depth-First Search), theo chiều rộng (Breadth-First Search), tìm kiếm kinh nghiệm. 37 Hình 12: Kiến trúc JPF + JPF được thiết kế gồm hai thành phần chính đó là đối tượng máy ảo (VM) và đối tượng tìm kiếm (Search Object). VM là một bộ sinh trạng thái bằng việc thực thi các chỉ thị bytecode. Đối tượng VM có các phương thức chính đó là :  forward():sinh ra một trạng thái mới  backtrack():phục hồi lại trạng thái ngay trước đó  restore(): phục hồi lại một trạng thái tùy ý Search Object là bộ điều khiển của VM. Search Object điều khiển việc thực thi trong JVM. Search Object chịu trách nhiệm chọn lựa trạng thái để VM tiếp tục quá trình thực thi bằng việc điều khiển VM để sinh ra trạng thái tiếp theo (foward) hoặc quay lui về trạng thái đã được tạo lúc trước. Theo mặc định, kỹ thuật tìm kiếm theo chiều sâu được sử dụng. Một kỹ thuật tìm kiếm dựa trên hàng đợi ưu tiên (tìm kiếm kinh nghiệm) cũng được cài đặt và ta có thể cấu hình để sử dụng nó. Phương thức tìm kiếm được cài đặt với một vòng lặp và chỉ dừng lại khi không gian trạng thái đã được thám hiểm hết hoặc tìm ra một sự vi phạm. 38 + Các tính năng mở rộng: Search Listener và VM Listener: Chúng được sử dụng để quan sát việc thực thi bên trong JPF mà không cần cài đặt lại các lớp của VM và Search. Search Listener được đăng ký tới các sự kiện của đối tượng Search: public interface SearchListener { // got the next state void stateAdvanced (Search search); //state was backtracked one step void stateBacktracked (Search search); //a previously generated state was restored void stateRestored (Search search); // JPF encountered a property violation void propertyViolated (Search search); //a search loop was started void searchStarted (Search search); // the search loop was finished void searchFinished (Search search); } và VM Listener được đặng ký tới các sự kiện của đối tượng VM trong quá trình thực thi một chương trình. VMListener được sử dụng để quản lý việc thực thi các chỉ thị bytecode: public interface VMListener { // VM has executed next instruction void instructionExecuted (JVM vm); // new Thread entered run() method void threadStarted (JVM vm); // Thread exited run() method void threadTerminated (JVM vm); // new class was loaded void classLoaded (JVM vm); // new object was created void objectCreated (JVM vm); // object was garbage collected void objectReleased (JVM vm); // garbage collection mark phase started void gcBegin (JVM vm); // garbage collection sweep phase terminated void gcEnd (JVM vm); // exception was thrown void exceptionThrown (JVM vm); // choice generator returned new value void nextChoice (JVM vm); ... } Model Java Interface (MJI): Nếu JNI là giao diện cho phép các ứng dụng Java chạy trong máy ảo Java của môi trường thực thi giao tiếp với các thư viện và ứng dụng 39 viết trong các ngôn ngữ khác như C, C++, Assembly của hệ điều hành bên dưới thì MJI là giao diện cho phép các ứng dụng Java chạy trong máy ảo JPF giao tiếp với máy ảo của môi trường thực thi bên dưới. Nói cách khác, MJI cho phép chuyển hướng việc thực thi một chương trình Java bên trong máy ảo JPF sang máy ảo của môi trường thực thi bên dưới (host JVM) mà JPF đang được chạy trên đó. Bộ sinh lựa chọn (CG): JPF sử dụng CG để đạt tới các trạng thái chương trình mong muốn trong trường hợp có nhiều lựa chọn để từ một trạng thái có thể chuyển sang các trạng thái khác. Các trạng thái chương trình được bao gói trong đối tượng SystemState. Mỗi trạng thái bao gồm trạng thái thực thi hiện thời của VM (KernelState), các đối tượng ChoiceGenerator bao gói các sự lựa chọn cho việc chuyển đổi trạng thái (Transition). Bằng việc thực thi các chỉ thị bytecode chương trình có thể chuyển từ một trạng thái này sang một trạng thái khác. Mỗi trạng thái hiện hành của chương trình được đăng ký bởi một đối tượng ChoiceGenerator chứa các sự lựa chọn và trạng thái hiện hành này có thể chuyển tới trạng thái thực thi tiếp theo bằng việc truy vấn tới các giá trị của đối tượng ChoiceGenerator để lựa chọn dãy chỉ thị bytecode sẽ được thực thi tiếp theo. Hình 13: Bộ sinh lựa chọn trong JPF Bộ tạo chỉ thị (Bytecode Factory): Trong JPF có các lớp biểu thị cho tất cả các chỉ thị bytecode được cài đặt để thông dịch các chỉ thị bytecode đó sử dụng thư viện bcel[30]. InstructionFactory là giao diện cho phép tạo các đối tượng Instruction bao gói việc thực thi các chỉ thị bytecode. Khi một chỉ thị bytecode trong tập tin .class 40 được tải vào trong máy ảo JPF để xử lý thì một đối tượng Instruction sẽ được tạo ra. Nói cách khác, khi một tập tin .class được đọc một mảng các đối tượng Instruction sẽ được tạo ra. Các đối tượng Instruction có phương thức execute() để thực hiện việc thực thi chỉ thị bytecode tương ứng. Chế độ thực thi mặc định trong JPF là chế độ thực thi cụ thể. Với giao diện InstructionFactory, ta có khả năng ghi đè các lớp chỉ thị mà cài đặt việc thông dịch các chỉ thị bytecode để thay đổi chế độ thực thi trong JPF. 3.2. Symbolic JPF Thực thi tương trưng một chương trình Java bằng cách cài đặt một trình thông dịch bytecode đặc biệt. Symbolic JPF là sự mở rộng của JPF bằng cách thông dịch bytecode theo ngữ nghĩa thực thi tượng trưng. Symbolic JPF không đòi hỏi phải sửa đổi chương trình mã nguồn như các cách tiếp cận thực thi tượng trưng một chương trình sử dụng JPF trước đây[16, 20, 26]. Với Symbolic JPF, việc thực thi tượng trưng với các phương thức mà gọi các phương thức khác sẽ được thực hiện dễ dàng. 3.2.1. Bộ tạo chỉ thị Bộ tạo chỉ thị (Instuction Factory) cho phép thay thế và mở rộng ngữ nghĩa thực thi cụ thể của bytecode bằng ngữ nghĩa thực thi tượng trưng. Các thông tin tượng trưng được lưu trữ trong các thuộc tính (attributes) kết hợp với dữ liệu chương trình (fields, stack operands, local variables) và được cập nhật trong quá trình thực thi. Thực thi các chương trình Java đã được biên dịch (.class files) bằng cách thông dịch các chỉ thị bytecode bằng một máy ảo Java (VM). Theo mặc định, VM thông dịch các bytecode theo ngữ nghĩa thực thi cụ thể. VM của JPF cũng dựa trên mô hình ngăn xếp (stack machine) và tuân theo các đặc tả về máy ảo Java. JPF cho phép thay đổi ngữ nghĩa thực thị cụ thể cho bytecode bằng cách sử dụng Instruction Factory. Hình 14. Bộ tạo chỉ thị trong JPF 41 Với mỗi phương thức được thực thi, JPF quản lý một đối tượng đó là MethodInfo. Đối tượng MethodInfo lưu trữ các chỉ thị bytecode như là mảng các đối tượng Instruction. Các đối tượng Instruction được tạo ra từ việc đọc các các bytecode từ tập tin .class tương ứng. JPF xây dựng một số ràng buộc trên lớp Instruction hơn là yêu cầu một phương thức execute(). JPF sử dụng mẫu thiết kế abstract factory[3] để khởi tạo các đối tượng Instruction. Lớp SymbolicInstructionFactory chứa các chỉ thị bytecode theo ngữ nghĩa thực thi tượng trưng. Lớp SymbolicInstructionFactory ủy quyền (delegate) tới lớp cha DefaultInstructionFactory chứa các chỉ thị bytecode theo nghĩa thực thi cụ thể. 3.2.2. Các thuộc tính JPF quản lý các trạng thái chương trình tương tự như máy ảo Java chuẩn. Mỗi trạng thái bao gồm một ngăn xếp lời gọi cho mỗi tiến trình, giá trị của các trường (fields) và thông tin lập lịch. Ngăn xếp lời gọi bao gồm các stack frame tương ứng với các phương thức sẽ được thực thi. Mỗi stack frame lưu trữ thông tin tượng trưng trong các vùng biến cục bộ (local variables) và các toán hạng ngăn xếp (stack operands). Hình 15. Trạng thái chương trình thực thi trong Symbolic JPF Hình 15 minh họa trạng thái của chương trình được thực thi bên trong JPF. Phương thức caller là phương thức đang được thực thi hiện thời. Stack frame tương ứng với phương thức caller nằm trên cùng của ngăn xếp lời gọi. Phương thức caller được thực thi và gọi phương thức callee. Trạng thái chương trình bao gồm heap, stack frame tương ứng với phương thức caller, và stack frame tương ứng với phương thức callee. Giá trị của heap và các stack frame được tạo ra thông qua việc thực thi các chỉ 42 thị bytecode khác nhau. Chỉ thị dup làm nhiệm vụ sao lưu các giá trị giữa các khay toán hạng (operand slots) của stack frame. Chỉ thị istore để sao lưu giá trị giữa vùng biến cục bộ(local variable slots) và vùng toán hạng (operand slots). Chỉ thị putfield và getfield để lấy và thiết lập giá trị cho các trường của đối tượng được lưu trong heap. Chỉ thị invokevirtual để gọi phương thức callee và giá trị trả về sẽ được lưu vào vùng toán hạng của stack frame tương ứng với phương thức caller. Các thuộc tính kết hợp với dữ liệu chương trình được gọi là các thuộc tính khe (slot attributes). Trong symbolic JPF, các thuộc tính được sử dụng để lưu trữ các giá trị tượng trưng và các biểu thức tượng trưng được tạo ra trong quá trình thực thi. Các thuộc tính được tạo ra hoặc truy cập bởi các chỉ thị bytecode thông qua các accessors (phương thức setAttr, getAttr). Các thuộc tính cũng có thể được tạo hoặc truy cập thông qua các listener hoặc native peers. Việc thao tác với các thuộc tính được thực hiện hoàn toàn bên trong JPF bởi các hành động khác nhau. Các hành động đó là thay đổi và lưu trữ các trạng thái chương trình (như dup, istore, putfield và getfield). Các lớp chỉ thị bytecode mà thực hiện việc tạo hoặc thay đổi các thông tin tượng trựng sẽ được ghi đè (override) để thay đổi ngữ nghĩa từ thực thi cụ thể thành thực thi tượng trưng. Các lớp chỉ thị bytecode đó là các chỉ thị rẽ nhánh, tính toán số học, chuyển đổi kiểu… Các chỉ thị bytecode mà chỉ lấy ra hoặc lưu trữ các thông tin tượng trưng sẽ được giữ không đổi theo ngữ nghĩa thực thi cụ thể. 3.2.3. Xử lý các điều kiện rẽ nhánh Thực thi tượng trưng các điều kiện rẽ nhánh liên quan tới việc tạo ra các lựa chọn khác nhau cho việc tìm kiếm của JPF. Việc điều hướng việc thực thi đi theo các nhánh thông qua một bộ sinh lựa chọn mới là PCChoiceGenerator. Một điều kiện đường đi được kết hợp với một lựa chọn được tạo ra bởi PCChoiceGenerator. Điều kiện rẽ nhánh hoặc phủ định điều kiện rẽ nhánh sẽ được thêm vào điều kiện đường đi tương ứng với mỗi lựa chọn. Điều kiện đường đi sẽ được kiểm tra sử dụng một bộ xử lý ràng buộc để xác định việc thực thi theo nhánh tương ứng với điều kiện đường đi đó có khả thi. Nếu điều kiện đường đi không thỏa mãn, JPF sẽ quay lui để đi theo các nhánh khả thi khác. Symbolic JPF sử dụng bộ xử lý ràng buộc choco[27] và Iasolver[30] cho các ràng buộc số học tuyến tính. IAsolver có thể xử lý được cả ràng buộc liên quan tới các hàm toán học phức tạp. Hai bộ xử lý ràng buộc này được tích hợp vào JPF thông qua 43 môt giao tiếp (interface) và ta có thể sử dụng một trong 2 bộ xử lý này để thực thi tượng trưng một chương trình thông qua việc cấu hình. 3.2.4. Ví dụ Như đã trình bày ở trên, chỉ những chỉ thị bytecode liên quan tới việc tạo hoặc thay đổi thông tin tượng trưng sẽ được thay đổi ngữ nghĩa từ thực thi cụ thể thành thực thi tượng trưng. Một trong những chỉ thị như thế là chỉ chị IADD, chỉ thị này thực hiện việc tính tổng của 2 số nguyên. public class IADD extends Instruction {... public Instruction execute(...ThreadInfo th){ 1: int v1 = th.pop(); 2: int v2 = th.pop(); 3: th.push(v1 + v2, false); 4: return getNext(th); } } Đoạn mã ở trên thực hiện việc thông dịch chỉ thị IADD theo ngữ nghĩa thực thi cụ thể. Theo mặc định, JPF gồm các lớp chỉ thị tương ứng với các chỉ thị bytecode được cài đặt để thông dịch bytecode theo ngữ nghĩa thực thi cụ thể. Máy ảo JPF thực hiện việc thông dịch bytecode tương tự như các máy ảo Java chuẩn khác. Các máy ảo Java thông dịch bytecode bằng cách thao tác với phần tử ở đỉnh của ngăn xếp (operand stack) trong stack frame. Có 2 thao tác chính là push và pop: + push: chèn một giá trị lên đỉnh operand stack + pop: lấy giá trị lưu ở đỉnh operand stack đồng thời loại bỏ phần tử đó ra khỏi operand stack. Việc thông dịch chỉ thị IADD theo ngữ nghĩa thực thi cụ thể như sau: lấy lần lượt 2 giá trị lưu ở 2 stack operand trên cùng của operand stack (dòng 1 và 2), sau đó tính tổng của chúng và lưu lại kết quả vào operand stack (dòng 3). Cuối cùng là trả về chỉ thị tiếp theo để thực thi (dòng 4). Đoạn mã cài đặt việc thông dịch chỉ thị IADD theo ngữ nghĩa thực thi tượng trưng trong Symbolic JPF: … public class IADD extends gov.nasa.jpf.jvm.bytecode.IADD { @Override public Instruction execute (...ThreadInfo th) { 1: StackFrame sf = th.getTopFrame(); 2: IntegerExpression sym_v1 = ...sf.getOperandAttr(0); 3: IntegerExpression sym_v2 = ...sf.getOperandAttr(1); 44 4: if(sym_v1==null && sym_v2==null) 5: return super.execute(ss, ks, th); 6: else { 7: int v1 = th.pop(); 8: int v2 = th.pop(); 9: th.push(0, false); 10: IntegerExpression result = null; if(sym_v1!=null) { if (sym_v2!=null) 13: result = sym_v1._plus(sym_v2); else 15: result = sym_v1._plus(v2); } else if (sym_v2!=null) 18: result = sym_v2._plus(v1); 19: sf.setOperandAttr(result); 20: return getNext(th); } } } Ý tưởng của việc thay đổi ngữ nghĩa thực thi của bytecode cũng tương tự như việc sửa đổi (instrument) một chương trình để hỗ trợ việc thực thi tượng trưng. Với các kiểu dữ liệu chuẩn (int, float,…) cần cài đặt các lớp để biểu thị cho kiểu của các biến tượng trưng tương ứng với các kiểu dữ liệu chuẩn đó. Trong Symbolic JPF, IntegerExpression biểu thị cho biểu thức số nguyên tượng trưng. RealExpression biểu thị cho biểu thức số thực tượng trưng. Trong quá trình thực thi tượng trưng, các thông tin tượng trưng được lưu trữ bởi các thuộc tính trong các toán hạng ngăn xếp (stack operand) của ngăn xếp toán hạng (operand stack) tương ứng với stack frame của phương thức đang được thực thi tượng trưng. Việc thực thi chỉ thị IADD theo nghĩa thực thi tượng trưng như sau: Trước tiên, các giá trị tượng trưng lưu trong các thuộc tính của 2 toán hạng ngăn xếp trên cùng được lấy ra (dòng 2 và 3). Việc lấy ra các giá trị tượng trưng lưu trong các thuộc tính không loại bỏ các toán hạng ngăn xếp chứa các thuộc tính đó. Các giá trị tương trưng được biểu thị bằng biểu thức của các giá trị đầu vào tượng trưng. Nếu các giá trị tượng trưng này đều bằng null (dòng 4) thì Symbolic JPF sẽ thực thi chỉ thị IADD theo ngữ nghĩa thực thi cụ thể (dòng 5) . Ngược lại nếu ít nhất một trong 2 giá trị đó khác null, việc thực thi theo nghĩa cụ thể vẫn được thực hiện (dòng 7, 8, 9). Tuy nhiên trong việc thực thi cụ thể này ta không quan tâm tới kết quả của việc tính toán các giá trị cụ thể. Ta cần tính toán các giá trị tượng trưng để kết hợp với thuộc tính tương ứng với kết quả đó. Phương thức _plus thực hiện việc xây dựng một biểu thức tượng trưng mới biểu thị cho kết quả của việc tính tổng của 2 giá trị tượng trưng. Giá trị tượng trưng biểu thị cho tổng của 2 giá trị tượng trưng sẽ được lưu lại vào thuộc 45 tính của kết quả trong toán hạng ngăn xếp (dòng 19). Cuối cùng, chỉ thị tiếp theo được trả về để thực thi (dòng 20). Ví dụ 3.1: Ví dụ này sẽ minh họa việc sử dụng bộ sinh lựa chọn trong việc thực thi tượng trưng với các điều kiện rẽ nhánh. Ta xét chỉ thị rẽ nhánh IF_ICMPEQ, chỉ thị rẽ nhánh này thực hiện việc so sánh giá trị của 2 biến kiểu int trong điều kiện rẽ nhánh có bằng nhau hay không để điều hướng việc thực thi đi theo nhánh mà giá trị trả về của điều kiện rẽ nhánh là true hoặc false. Trong JPF, lớp IfInstruction là lớp trừu tượng cài đặt việc thông dịch các chỉ thị rẽ nhánh if. Lớp này có một phương thức trừu tượng (dòng 2) để nhận giá trị trả về true hoặc false của điều kiện rẽ nhánh. Phương thức trừu tượng này cần được cài đặt tương ứng với mỗi chỉ thị rẽ nhánh if khác nhau. Việc thông dịch các chỉ thị rẽ nhánh if một cách tổng quát như sau: Thực hiện việc đánh giá biểu thức điều kiện rẽ nhánh (dòng 4). Nếu điều kiện rẽ nhánh nhận giá trị true (dòng 5) thì nhảy tới chỉ thị tiếp theo của nhánh tương ứng với điều kiện rẽ nhánh nhận giá trị true (dòng 6). Nếu không thì trả về chỉ thị tiếp theo để thực thi (dòng 8). public abstract class IfInstruction extends Instruction { 1: protected boolean conditionValue; 2: public abstract boolean popConditionValue(ThreadInfo ti); public Instruction execute (... ThreadInfo ti){ 4: conditionValue = popConditionValue(ti); 5: if (conditionValue) 6: return getTarget(); 7: else 8: return getNext(ti); } ... } Với chỉ thị IF_ICMPEQ thì việc đánh giá điều kiện rẽ nhánh được thực hiện như sau. Lấy giá trị của 2 phần tử trên cùng của stack (dòng 1, 2) và trả về kết quả so sánh giữa 2 giá trị đó (dòng 3). Các giá trị này là các giá trị thực do đó điều kiện rẽ nhánh sẽ chỉ nhận một trong hai giá trị là true hoặc false. 46 public class IF_ICMPEQ extends IfInstruction { public boolean popConditionValue (ThreadInfo ti){ 1: int v1 = ti.pop(); 2: int v2 = ti.pop(); 3: return (v1 == v2); } ... } Lớp IF_ICMPEQ bên dưới cài đặt việc thông dịch chỉ thị IF_ICMPEQ theo ngữ nghĩa thực thi tượng trưng. Khi thông dịch chỉ thị rẽ nhánh theo ngữ nghĩa thực thi cụ thể thì việc thực thi chỉ có thể đi theo một trong hai nhánh tương ứng với điều kiện rẽ nhánh nhận giá trị true hoặc false. Thông dịch một chỉ thị rẽ nhánh theo ngữ nghĩa thực thi tượng trưng thì cả 2 nhánh đều được xem xét để điều hướng việc thực thi đi theo. public class IF_ICMPEQ extends gov.nasa.jpf.jvm.bytecode.IF_ICMPEQ { @Override public Instruction execute(SystemState ss,KernelState ks,ThreadInfo ti) { 1: StackFrame sf = ti.getTopFrame(); 2: IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0); 3: IntegerExpression sym_v2 = (IntegerExpression) sf.getOperandAttr(1); // both conditions are concrete 4: if ((sym_v1 == null) && (sym_v2 == null)) { 5: return super.execute(ss, ks, ti); 6: }else{ // at least one condition is symbolic ... 7: ChoiceGenerator cg = new PCChoiceGenerator(2); ... 8: conditionValue = (Integer)cg.getNextChoice()==0 ? false: true; ... 9: int v2 = ti.pop(); 10: int v1 = ti.pop(); ... 11: if (conditionValue) { ... 12