Luận văn Phương pháp phân tích mã nguồn và sinh dữ liệu kiểm thử cho các dự án C/C++

g thêm bất phương trình/phương trình về điều kiện giá trị cấp phát cũng như trạng thái bảng biến tabelVar được cập nhật nếu câu lệnh đang phân tích là câu lệnh cấp phát (dòng 11, 12). Nói rõ ràng hơn, nếu biến con trỏ được cấp phát một vùng nhớ có kích thước không xác định (gọi là sizeOfAllocation) thì giá trị vùng nhớ đó phải luôn dương để đảm bảo tính đúng đắn của hệ ràng buộc, tức là sizeOfAllocation>=0. Do đó, bất phương trình sizeOfAllocation >=0 được bổ sung vào hệ ràng buộc PC để đảm bảo nghiệm (hay dữ liệu kiểm thử) không gây lỗi khi thực thi. Trường hợp kế tiếp, nếu câu lệnh stm là khai báo thì bảng biến tableVar bổ sung thêm biến đó vào danh sách biến hiện tại. Đồng thời cập nhật giá trị biến vừa khai báo nếu biến đó được khởi tạo giá trị (dòng 14, 15). Xét trường hợp câu lệnh stm là câu lệnh điều kiện, nếu giá trị câu lệnh stm luôn sai thì hệ ràng buộc luôn vô nghiệm (dòng 16-23). Thuật toán trả về hệ ràng buộc rỗng và kết thúc. Ngược lại, nếu câu lệnh stm luôn có nghiệm, ta bỏ qua câu lệnh đó và không bổ sung vào PC. Trường hợp cuối cùng, câu lệnh stm không thể xác định được tính luận lý, hệ ràng buộc PC lưu thêm câu lệnh điều kiện này. 23 Thuật toán 3.2. Thuật toán xây dựng hệ ràng buộc từ đường thi hành. Nếu câu lệnh stm là câu lệnh đánh dấu phạm vi, ta cập nhật bảng biến như sau (dòng 24-30). Trường hợp stm là dấu mở ngoặc nhọn, tức là bắt đầu thân hàm hoặc 24 thân khối lệnh điều khiển, ta đánh dấu tất cả các biến được khởi tạo từ câu lệnh này trở đi ở mức level + 1 (trong đó level là giá trị cục bộ hiện tại). Chú ý rằng biến toàn cục luôn có giá trị level cục bộ bằng 0 (kí hiệu GLO). Ngược lại, nếu stm là dấu kết thúc thân hàm/thân khối lệnh điều khiển, ta xóa toàn bộ biến trong tableVar ở có giá trị cục bộ cao nhất bởi vì những biến đó đã trở nên vô nghĩa. Sau khi tất cả mọi câu lệnh trong khối lệnh điều khiển được phân tích, hệ ràng buộc PC tiếp tục bổ sung thêm một vài ràng buộc phụ vào để nghiệm tránh gây lỗi khi thực thi (dòng 32-34). Ví dụ, giả sử hiện tại trong PC có một hệ ràng buộc tồn tại phép chia a/b. Để đảm bảo nghiệm không gây lỗi chia cho 0, ta cần bổ sung thêm ràng buộc b!=0 (dòng 33). Ví dụ khác, nếu chỉ số mảng là biểu thức trừu tượng S mà không phải hằng số, ta cần thêm ràng buộc S >= 0 (dòng 32). Thuật toán kết thúc khi mọi câu lệnh trong đường thi hành được phân tích, và hệ ràng buộc phụ được bổ sung; hoặc trong quá trình phân tích một câu lệnh điều kiện luôn sai được phát hiện. Trong trường hợp cuối cùng này, hệ ràng buộc trả về rỗng (vô nghiệm). Ví dụ, xét đường thi hành của đồ thị CFG phủ câu lệnh/nhánh trình bày trong Hình 3.3 đi qua nhánh đúng điều kiện (value[i] != -2 && tcnt < 10) và đi qua nhánh sai điều kiện (vcnt<0) như sau: Begin -> (int tcnt = 0, vcnt = 0, sum = 0, i = 0;) -> (value[i] != -2 && tcnt (vcnt (return sum/vcnt) -> End Hệ ràng buộc tương ứng với đường thi hành trên được mô tả như sau. Trong đó, điều kiện [1] được chuyển thành ràng buộc (1), điều kiện [2] được chuyển thành ràng buộc (2). { (𝑣𝑎𝑙𝑢𝑒[0] ! = −2)𝑎𝑛𝑑 (0 < 10) (𝟏) 0 < 0 (𝟐) 3.3.4. Giải hệ ràng buộc sử dụng bộ giải SMT-Solver Bước giải hệ ràng buộc là bước thứ hai trong hàm has_solution(). Phần này giải quyết bài toán: “Cho một hệ ràng buộc sinh từ đường thi hành, ta cần tìm một nghiệm thỏa mãn hệ ràng buộc này.” Hệ ràng buộc ta sinh từ đường thi hành được biểu diễn dạng trung tố, tuy nhiên các bộ giải SMT-Solver không hỗ trợ giải biểu thức dạng này. Bởi thế, những hệ 25 ràng buộc này cần biến đổi về chuẩn đầu vào SMT-Solver – dạng biểu thức biểu thức chuẩn SMT-Lib. Quy trình xây dựng hệ ràng buộc theo chuẩn SMT-Lib từ hệ ràng buộc biểu diễn ở dạng biểu thức trung tố (infix expression) sinh từ đường thi hành được trình bày trong Hình 3.6. Đầu tiên, hệ ràng buộc được biến đổi về dạng biểu thức hậu tố (postfix expression), sau đó chuyển sang dạng cây (tree expression). Từ cây, ta xây dựng biểu thức chuẩn SMT-Lib bằng cách duyệt cây đó. Hình 3.6. Quy trình xây dựng biểu thức SMT-Lib từ ràng buộc. Hình 3.7 trình bày quá trình xây dựng hệ ràng buộc chuẩn SMT-Lib từ hệ ràng buộc sinh từ kĩ thuật thực thi tượng trưng. Đầu tiên, hệ ràng buộc gốc này được chuyển về dạng biểu thức hậu tố “x 0 > y 1 < || !”. Sau đó, biểu thức hậu tố này được chuyển thành cây cấu trúc. Các đỉnh trong cây có thể tương ứng với một toán tử (operator), hoặc toán hạng (operand). Cuối cùng, cây được chuyển về biểu thức chuẩn SMT-Lib như sau “assert( not (or (> x 0) (< y 1)))”. Từ khóa “not” ứng với phép phủ định. Hình 3.7. Quá trình biến đổi hệ ràng buộc về chuẩn SMTLib. 26 3.4. Biên dịch và thực thi dữ liệu kiểm thử trong môi trường chạy Phần này trình bày hàm execute() tại dòng 10 của thuật toán LDFS. Hàm execute() biên dịch và thực thi dữ liệu kiểm thử (solution) để tính danh sách các câu lệnh thật sự được đi qua. Chú ý rằng, từ một đường thi hành sinh từ đồ thị CFG, một bộ dữ liệu kiểm thử cần được tìm kiếm thỏa mãn đi qua đường thi hành đó. Để tìm được bộ giá trị này, đường thi hành được biểu diễn về hệ ràng buộc bằng cách áp dụng kĩ thuật thực thi tượng trưng. Sau đó, SMT-Solver giải hệ ràng buộc này để sinh dữ liệu kiểm thử đi qua đường thi hành đó. Tuy nhiên, dữ liệu kiểm thử này chưa chắc sẽ đi qua đường thi hành ban đầu bởi vì hai lí do. Thứ nhất, quá trình thực thi tượng trưng là một bước phân tích mã nguồn khá phức tạp và có thể có nhiều sai sót. Thứ hai, trường hợp một câu lệnh chưa được hỗ trợ trong bước quá trình thực thi tượng trưng, hệ ràng buộc chỉ sinh ra từ câu lệnh đầu tiên đến trước câu lệnh hiện tại. Điều đó có nghĩa là, nghiệm của hệ ràng buộc không chắc chắn đi qua đường thi hành ban đầu mà chỉ đi qua một phần. Bởi vì hai lý do này, dữ liệu kiểm thử sinh ra cần được thực thi thật sự trong trình biên dịch để thu thập chính xác danh sách câu lệnh được đi qua. Bộ thực thi dữ liệu kiểm thử của một hàm (test driver) cung cấp cơ chế khởi tạo giá trị các biến truyền vào hàm và chạy chương trình dưới bộ giá trị đó. Về bản chất, bộ thực thi dữ liệu kiểm thử này là một hàm main() – điểm bắt đầu chạy chương trình. Trong hàm main() này, danh sách biến truyền vào hàm được khởi tạo. Sau đó, hàm cần kiểm thử được mô tả lời gọi ở cuối cùng hàm main(). Cuối cùng, bộ thực thi dữ liệu kiểm thử này được đặt trong dự án và chạy tự động. Sau khi bộ thực thi dữ liệu kiểm thử này chạy xong, danh sách các câu lệnh thực thi được thu thập. Kế tiếp, đồ thị CFG của hàm cần kiểm thử được cập nhật trạng thái độ phủ, cũng một trạng thái viếng thăm của các cạnh/câu lệnh/điều kiện con (dòng 11 thuật toán LDFS). Chú ý rằng, nếu độ phủ đồ thị CFG đạt được tại bước này đạt 100% thì quá trình sinh dữ liệu kiểm thử kết thúc. Ngược lại, sinh dữ liệu kiểm thử tiếp tục được sinh ra sao cho đi qua các cạnh/câu lệnh/điều kiện con chưa được viếng thăm. 27 3.5. Tối ưu hóa pha sinh dữ liệu kiểm thử Để tăng tốc thời gian sinh dữ liệu kiểm thử, nhiều kĩ thuật khác nhau được áp dụng có thể kể đến kĩ thuật đơn giản hóa hệ ràng buộc, kĩ thuật biên dịch và thực thi dữ liệu kiểm thử cải tiến. Tư tưởng các kĩ thuật này được trình bày sau đây. 3.5.1. Đơn giản hóa hệ ràng buộc Kích thước của hệ ràng buộc có thể khá lớn, và cấu trúc khá phức tạp làm tăng thời gian giải hệ ràng buộc. Điều đó dẫn đến bài toán tối ưu hệ ràng buộc trước khi sử dụng SMT-Solver để giải hệ ràng buộc đó. Phương pháp đề xuất áp dụng một vài kĩ thuật tối ưu hóa hệ ràng buộc sau đây để giảm thiểu thời gian sử dụng bộ giải SMT- Solver. Trong đó, hai kĩ thuật chính được sử dụng gồm kĩ thuật giải hệ ràng buộc tăng dần và kĩ thuật kiểm tra tính thỏa mãn dựa trên bộ nhớ đệm. Hiện tại, nhiều kĩ thuật tối ưu hệ ràng buộc đã được đề xuất. Kĩ thuật tối ưu đầu tiên đề xuất trong CUTE, EXE, KLEE, và CAUT thu gọn hệ ràng buộc cần giải bằng cách loại bỏ các hệ ràng buộc không cần thiết. Tư tưởng chính của kĩ thuật này là chỉ những hệ ràng buộc liên quan đến hệ ràng buộc phủ định cuối cùng được giải. Kĩ thuật này gọi là kĩ thuật giải hệ ràng buộc tăng dần (incremental solving technique). Kĩ thuật tối ưu hệ ràng buộc thứ hai đề xuất bởi Cristian Cadar và cộng sự được gọi là kĩ thuật kiểm tra tính thỏa mãn dựa trên bộ nhớ đệm (cache-based unsatisfiability check). Kĩ thuật này được áp dụng trong EXE and KLEE. Theo như tư tưởng kĩ thuật này, tất cả các hệ ràng buộc đã được giải đều được lưu lại trong bộ nhớ. Tính luận lý của hệ ràng buộc kế tiếp được xác định nhanh qua đánh giá tập các hệ ràng buộc trước đó. Cụ thể, giả sử trong bộ nhớ lưu hai hệ ràng buộc đã được giải gồm A, B. Trong đó, hệ ràng buộc A có nghiệm, hệ ràng buộc B vô nghiệm. Cho hệ ràng buộc C, tính luận lý hệ ràng buộc này được kiểm tra nhanh như sau. Nếu 𝐴 ⊂ 𝐶 thì hệ ràng buộc C có thể có nghiệm, và nghiệm của A có thể là một phần nghiệm trong C. Nếu 𝐵 ⊂ 𝐶 thì hệ ràng buộc C vô nghiệm, tức hệ ràng buộc C không cần đưa vào bộ giải SMT-Solver để tìm nghiệm. Bên cạnh hai phương pháp chính nêu trên, phương pháp đề xuất áp dụng một vài kĩ thuật đơn giản khác như kĩ thuật đơn giản hóa biểu thức (ví dụ: x+0 > 1 đơn giản hóa thành x >1), kĩ thuật suy biến nhanh giá trị biến (ví dụ: x+1=10 đơn giản 28 hóa thành x=9), kĩ thuật loại bỏ hệ ràng buộc hiển nhiên (ví dụ: x<10, x==5 đơn giản hóa thành x==5), v.v. 3.5.2. Tăng tốc thời gian biên dịch và thực thi dữ liệu kiểm thử Theo như phương pháp truyền thống, sau khi từng bộ dữ liệu kiểm thử sinh ra, một bộ thực thi dữ liệu kiểm thử đó được tạo. Sau đó, bộ thực thi dữ liệu kiểm thử này được biên dịch và chạy để lấy tập câu lệnh đi qua. Vì thế, nếu có n bộ dữ liệu kiểm thử sinh ra thì quá trình biên dịch và chạy được tiến hành n lần. Phương pháp đề xuất tăng tốc thời gian chạy các dữ liệu kiểm thử sinh ra bằng cách xây dựng bộ thực thi dữ liệu kiểm thử tổng quát cho mọi loại giá trị đầu vào. Bởi thế, quá trình biên dịch và chạy nêu trên có thể rút ngắn xuống 1 lần biên dịch và n lần chạy dữ liệu kiểm thử. Hình 3.8. Kĩ thuật tạo bộ thực thi ca kiểm thử tổng quát. Hình 3.8 trình bày quá trình xây dựng bộ thực thi dữ liệu kiểm thử tổng quát. Đầu vào gồm hàm cần kiểm thử đã được chèn câu lệnh đánh dấu (instrumented function) và tệp lưu dữ liệu kiểm thử (test data external file). Đầu ra là mã nguồn bộ thực thi dữ liệu kiểm thử tổng quát cho mọi loại giá trị đầu vào gồm biến kiểu cơ bản (số nguyên, số thực, kí tự), biến mảng, biến con trỏ, biến kiểu dẫn xuất (class, struct). Quá trình tạo bộ mã nguồn tổng quát gồm ba pha như sau. Trong pha đầu tiên, khung xương bộ thực thi dữ liệu kiểm thử được tạo chứa đầy đủ các hàm cần thiết cho hai pha sau (ví dụ: hàm đọc dữ liệu dữ liệu kiểm thử từ tệp, v.v.). Pha thứ hai tạo mã nguồn nạp dữ liệu biến kiểu cơ bản từ tệp lưu dữ liệu kiểm thử dựa trên khung mã nguồn tạo ở pha trước. Pha cuối cùng tạo mã nguồn đọc biến kiểu dẫn xuất từ tệp dữ liệu kiểm thử. Trong pha cuối này, tham số độ sâu depth xác định độ sâu tối đa khi duyệt danh sách liên kết để tránh trường hợp duyệt danh sách liên kết vô hạn. Một biến có tính danh sách liên kết khi biến đó có thuộc tính có kiểu là chính biến đó. 29 Kĩ thuật tăng tốc quá trình thực thi dữ liệu kiểm thử thể hiện ưu điểm rõ ràng khi số lượng bộ dữ liệu kiểm thử thỏa mãn tiêu chí độ phủ đủ lớn. Tất cả mọi dữ liệu kiểm thử sinh ra từ đường thi hành đều được lưu trong một tệp cố định ở ngoài. Sau đó, bộ thực thi dữ liệu kiểm thử tổng quát đọc tệp này để tự động khởi tạo giá trị các biến. 3.6. Xuất mã nguồn kiểm thử theo chuẩn Google Test Google Test4 là một famework được dùng rộng rãi trong các công ty phần mềm C/C++ để viết unit test. Sau khi tập dữ liệu kiểm thử được sinh ra bởi thuật toán LDFS, tập mã nguồn kiểm thử theo chuẩn Google Test được tạo ra tự động. Điều này đặc biệt có ý nghĩa vì lập trình viên không cần tốn thời gian viết unit test với tập dữ liệu kiểm thử. Từ đó chi phí phát triển phần mềm giảm đi, đặc biệt đối với các dự án lớn khi số lượng bộ dữ liệu kiểm thử lên tới hàng chục nghìn, thậm chí hàng trăm nghìn. Cấu trúc của một bộ mã nguồn kiểm thử theo chuẩn framework Google Test như sau. Phần đầu tiên sẽ nạp chỉ thị tiền xử lý header của framework này để có thể sử dụng các hàm hỗ trợ bởi Google Test. Phần thứ hai là danh sách các hàm, trong đó mỗi hàm tương ứng với một bộ dữ liệu kiểm thử. Cụ thể, nếu 3 bộ dữ liệu kiểm thử được sinh ra thì số lượng mã nguồn kiểm thử Google Test cần sinh tự động tương ứng bằng 3. Cấu trúc một hàm gồm ba phần. Phần đầu tiên chứa mã nguồn khởi tạo giá trị các biến với các giá trị lưu trong dữ liệu kiểm thử. Phần thứ hai là lời gọi đến hàm cần kiểm thử. Các tham số truyền vào hàm này là danh sách biến được ở tạo ở phần đầu tiên. Phần cuối cùng là phép so sánh đầu ra mong muốn (expected output) với đầu ra thực tế (real output). 4 https://github.com/google/Google Test 30 CÔNG CỤ VÀ THỰC NGHIỆM Chương này trình bày tổng quan kiến trúc công cụ CFT4Cpp được xây dựng dựa trên phương pháp đề xuất. Bên cạnh đó, thực nghiệm so sánh với KLEE, CAUT, PathCrawler, CREST theo tiêu chí độ phủ và số bộ dữ liệu kiểm thử để chứng minh tính hiệu quả phương pháp. Ngoài ra, thực nghiệm cũng thể hiện tính hiệu quả về tiêu chí thời gian thực thi dữ liệu kiểm thử so với phương pháp thực thi dữ liệu kiểm thử truyền thống. Cuối cùng, kết quả sinh tập dữ liệu kiểm thử kiểm tra tính đúng đắn vòng lặp được trình bày chi tiết trong thực nghiệm. 4.1. Giới thiệu công cụ kiểm thử tự động CFT4Cpp Để chứng minh tính hiệu quả của phương pháp đề xuất, công cụ CFT4Cpp5 được phát triển trên ngôn ngữ Java. Công cụ CFT4Cpp cung cấp một giải pháp sinh dữ liệu kiểm thử tự động khá hiệu quả cho các dự án viết bằng C/C++. Phiên bản hiện tại của CFT4Cpp hỗ trợ chạy trên môi trường Window đã cài sẵn JDK 8 trở lên và trình biên dịch MingW64. Hình 4.1. Kiến trúc công cụ CFT4Cpp. 5 31 Về cơ bản, công cụ có kiến trúc hai tầng gồm tầng Presentation và tầng Business. Tầng Presentation gồm mô-đun chịu trách nhiệm vẽ đồ thị CFG, mô-đun hiển thị cây cấu trúc của dự án đầu vào, và mô-đun xuất biên bản kiểm thử. Tầng Business gồm ba mô-đun chính như sau: tiền xử lý mã nguồn, sinh dữ liệu kiểm thử, và sinh bộ mã nguồn kiểm thử cho từng dữ liệu kiểm thử theo định dạng của Google Test. Tầng Business tương tác với bộ giải SMT-Solver Z3 và trình biên dịch MingW64. Trình biên dịch này được tích hợp sẵn trong DevCpp. Chức năng của công cụ được mô tả qua bài toán sinh dữ liệu kiểm thử cho hàm Divide. Hàm này nhận hai tham số đầu vào x và y. Nếu giá trị y bằng 0, hàm này trả về ngoại lệ std::exception. Ngược lại, hàm Divide trả về giá trị x/y. - Bước 1. Nạp dự án cần phân tích. Đầu tiên, người dùng đẩy dự án C/C++ cần phân tích vào công cụ CFT4Cpp (Hình 4.2). Dự án này có tên Sample_for_R1_2 do TSDV cung cấp để đánh giá tính hoàn thiện của công cụ CFT4Cpp. Công cụ tự động dựng cây cấu trúc dự án (phía bên trái). Khung hiển thị đồ thị dòng điều khiển ở chính giữa. Thông tin mã nguồn hàm đang kiểm thử, cũng như thông tin cấu hình được thể hiện ở khung bên phải. Hình 4.2. Giao diện chính của công cụ CFT4Cpp. 32 - Bước 2. Cấu hình. Trước khi sinh dữ liệu kiểm thử cho hàm Divide, người dùng cần cấu hình đường dẫn đến trình biên dịch MingW64 Hình 4.3. Giao diện bước cấu hình công cụ CFT4Cpp. - Bước 3. Sinh dữ liệu kiểm thử. Sau khi hoàn thành bước cấu hình trình biên dịch, người dùng tiến hành sinh dữ liệu kiểm thử cho hàm Divide (Hình 4.3). Thời gian sinh dữ liệu kiểm thử khoảng 5 giây, và thời gian này có thể nhanh hơn hoặc chậm hơn tùy theo cấu hình máy tính. Công cụ sinh ra hai dữ liệu kiểm thử cho hàm Divide gồm (x, y) = (558, 0), (663, 1). Độ phủ nhánh đạt được bằng 100%. Hình 4.4. Giao diện sinh dữ liệu kiểm thử cho hàm Divide. 33 - Bước 4. Xuất biên bản kiểm thử. Công cụ hỗ trợ người dùng xuất kết quả kiểm thử ra biên bản MS Excel, hoặc xuất mã nguồn kiểm thử cho từng giá trị dữ liệu kiểm thử sinh ở bước 3 (Hình 4.5). Mã nguồn kiểm thử tuân theo chuẩn của framework Google Test. Hình 4.5. Biên bản kiểm thử xuất bởi công cụ CFT4Cpp cho hàm Divide. 4.2. Thư viện hỗ trợ sử dụng trong công cụ kiểm thử tự động CFT4Cpp 4.2.1. Thư viện giải hệ ràng buộc Z3 Thư viện Z36 là một trong những thư viện giải hệ ràng buộc khá mạnh mẽ. Thư viện này hỗ trợ hai môi trường gồm Window và Ubuntu. Để giải hệ ràng buộc, ta chuyển hệ này về biểu thức chuẩn SMT-Lib. Sau đó, biểu thức SMT-Lib này được giải qua dòng lệnh sử dụng Z3. Giả sử biểu thức SMT-Lib này lưu trong D:/constraints.txt lưu tại ổ D, cú pháp gọi bộ giải Z3 như sau: [đường dẫn z3.exe] –smt2 D:/constraints.txt 6 https://github.com/Z3Prover/z3 34 Người dùng có thể giải hệ trực tuyến qua hệ thống Z3 cung cấp sẵn tại link https://rise4fun.com/Z3. Mã nguồn 4.1 minh họa một hệ ràng buộc theo chuẩn SMT- Lib. Hình 4.6 trình bày nghiệm hệ ràng buộc này khi chạy Z3 trên hệ thống trực tuyến nêu trên. Nếu hệ ràng buộc vô nghiệm, hệ thống trả về UNSAT. Ngược lại, hệ thống thông báo SAT cũng với nghiệm thể hiện ở dưới. Trường hợp hệ ràng buộc có vố số nghiệm, Z3 trả về một nghiệm bất kỳ. Trong ví dụ này, Z3 trả về một bộ giá trị ngẫu nhiên (x, y) = (0, -1). (declare-const x Int) (declare-const y Int) (assert (< x 1)) (assert (> x y)) (check-sat) (get-model) Mã nguồn 4.1. Minh họa một hệ ràng buộc theo chuẩn SMT-Lib. Hình 4.6. Minh họa kết quả giải hệ ràng buộc sử dụng Z3. 4.2.2. Thư viện phân tích mã nguồn CDT Cho đến thời điểm hiện tại, nhiều thư viện hỗ trợ khả năng phân tích mã nguồn C/C++ như CDT7, Clang8, v.v. Trong nghiên cứu này, tôi sử dụng thư viện CDT để phân tích cú pháp mã nguồn. 7 https://www.eclipse.org/cdt 8 https://clang.llvm.org 35 Khi đẩy mã nguồn vào CDT, đầu ra là cây AST ứng với mã nguồn đó. Mã nguồn đẩy vào có thể là một hàm, một câu lệnh, một tệp header, v.v. Các đỉnh trong cây AST này chưa có khả năng binding bởi vì thư viện này được sử dụng ngoài Eclipse. Chẳng hạn, ta đẩy vào mã nguồn có câu lệnh x = y + 1. Đầu ra AST ứng với câu lệnh này thể hiện rằng biến x có kiểu là IASTIdExpression mà không thể hiện rõ ràng biến này có khai báo “int x;”. Nếu muốn bắt được thông tin này, ta cần sử dụng thư viện CDT dưới dạng plug-in Eclipse. 4.2.3. Thư viện tính giá trị biểu thức Jeval Thư viện Jeval9 là một thư viện không thể thiếu khi xây dựng công cụ CFT4Cpp. Đầu vào thư viện này là một biểu thức. Đầu ra là giá trị biểu thức đó. Chẳng hạn, với đầu vào là “1+2+3” thì đầu ra Jeval trả về bằng 6. 4.3. Kết quả thực nghiệm Tác giả đã tiến hành thực nghiệm trên công cụ CFT4Cpp với các bộ dữ liệu thực tế để thể hiện tính hiệu quả của phương pháp đề xuất. Bốn công cụ được so sánh gồm KLEE, PathCrawler, CAUT, và CREST. Thực nghiệm được tiến hành trên máy Intel(R) Core(TM) i5-4200U CPU @1.6GHz - 2.3GHz với 4GB bộ nhớ. 4.3.1. So sánh số lượng bộ dữ liệu kiểm thử và độ phủ với KLEE, CAUT, CREST, PathCrawler Bảng 4.1. Thông tin các công cụ so sánh trong thực nghiệm Công cụ Phiên bản Ngôn ngữ hỗ trợ Môi trường hỗ trợ Trình biên dịch Phương pháp sinh KLEE 2016 C Ubuntu Clang EGT CAUT 2014 C Ubuntu GCC DSE CREST 2014 C Ubuntu GCC DSE PathCrawler 2012 C Web-based GCC DSE CFT4Cpp 2017 C/C++ Window MingW DSE 9 36 Bảng 4.1 trình bày các công cụ được so sánh với CFT4Cpp gồm KLEE [2], CAUT [12], PathCrawler [13] và CREST [1]. Công cụ KLEE áp dụng kĩ thuật EGT để sinh dữ liệu kiểm thử thỏa mãn hai tiêu chí gồm độ phủ tối đa và phát hiện các lỗi tiềm ẩn. Các công cụ còn lại sử dụng kĩ thuật kiểm thử tự động định hướng. Để đảm bảo tính khách quan, CFT4Cpp được so sánh với từng công cụ nêu trên với cùng nhóm cấu hình mà các công cụ này hỗ trợ. Bảng 4.2 trình bày thông tin hai nhóm thực nghiệm gồm: nhóm A (KLEE, PathCrawler), và nhóm B (CAUT, CREST). Các thông tin cấu hình gồm: khoảng của biến kí tự, khoảng của biến kiểu số, số phần tử của mảng, số lần lặp tối đa của vòng, và chiến thuật chọn đường thi hành. Nếu một cấu hình của công cụ đánh dấu “-“, tức là công cụ không hỗ trợ cài đặt loại thông tin đó. Chiến thuật chọn đường thi hành được chọn dựa trên bài báo tương ứng của từng công cụ thực nghiệm. Đó là những chiến thuật đã được chính minh tính hiệu quả trong các bài toán thực tế. Cụ thể, KLEE đưa ra khá nhiều chiến thuật chọn đường thi hành khác nhau, nhưng thực nghiệm chỉ ra chiến thuật hiệu quả nhất có tên nurs:md2u. Bảng 4.2. Thông tin cấu hình các ví dụ trong thực nghiệm Nhóm A Nhóm B KLEE PathCrawler CFT4Cpp CAUT CREST CFT4Cpp Khoảng biến kí tự [32..126] Phạm vi kiểu biến Khoảng biến kiểu số [-100..200] Phạm vi kiểu biến Kích thước mảng [0..10] 10 Số lần lặp tối đa - 11 11 - 11 11 Chiến thuật chọn đường thi hành nurs: md2u k-path LDFS pps cfg LDFS Bảng 4.2 mô tả thông tin các ví dụ tiến hành thực nghiệm. Tất cả những ví dụ này được lấy ngẫu nhiên trên github. Kí hiệu CC mô tả độ phức tạp của ví dụ được tính theo công thức Mc-Cabe. Kí hiệu LOC là số dòng mã nguồn theo tiêu chuẩn của Eclipse (không tính số dòng thừa, v.v.). Tất cả các hàm kiểm thử đều có vòng lặp, trừ hàm ArrayCmp. Một vài hàm có đệ quy như reverse, Fibonacci, v.v. 37 Bảng 4.3. Thông tin các hàm kiểm thử về tiêu chí độ phủ và số bộ dữ liệu kiểm thử Hàm Mô tả Hàm Mô tả CC LOC CC LOC uninit_var(int[3],int[3]) 7 12 concatenate(char[],char[]) 3 11 ArrayCmp(int,char*,char*) 4 7 concatenate_string(char*,char*) 3 8 check_prime(int) 4 7 reverse2(char*,int,int) 2 8 check_armstrong(long long) 4 14 copy_string(char*,char*) 2 6 power(int,int) 2 6 string_length(char*) 2 6 print_floyd(int) 3 10 Fibonacci(int) 3 4 find_minimum(int[],int) 3 9 find_maximum(int[],int) 3 9 linear_search1(long[],long,long) 3 6 add_digits(int) 2 6 linear_search2(long*,long,long) 3 6 reverse(long) 2 8 bubble_sort(long[],long) 4 8 Bảng 4.4 trình bày kết quả thực nghiệm của nhóm A gồm hai công cụ KLEE và PathCrawler. Kí hiệu num đại diện số lượng bộ dữ liệu kiểm thử sinh ra. Kí hiệu cov đại diện độ phủ đạt được với số bộ dữ liệu kiểm thử sinh ra đó. Trong tất cả những ví dụ này, CFT4Cpp đều đạt độ phủ tối đa với số bộ dữ liệu kiểm thử ít hơn hẳn so với hai công cụ còn lại. Trong ví dụ đầu tiên uninit_var, cả ba công cụ đều đạt độ phủ tối đa. Tuy nhiên, số bộ dữ liệu kiểm thử do CFT4Cpp sinh ra bằng 5, trong khi đó KLEE sinh tới 27 bộ dữ liệu kiểm thử và PathCrawler sinh lớn hơn 20 bộ dữ liệu kiểm thử. Điều này tương tự với các ví dụ power, print_floyd. Trong nhiều ví dụ, số bộ dữ liệu kiểm thử do KLEE sinh ra khá lớn (kí hiệu n/a). Lý giải cho vấn đề này là do mục tiêu sinh dữ liệu kiểm thử của KLEE không chỉ đạt độ phủ tối đa mà còn phát hiện lỗi. Vì thế, KLEE sẽ kiểm tra mọi trường hợp có thể xảy ra trong mã nguồn. 38 Điều đó dẫn đến số lượng bộ dữ liệu kiểm thử sinh bởi KLEE khá lớn gây khó khăn cho quản lý. Bảng 4.4. Kết quả so sánh công cụ CFT4Cpp với KLEE và PathCrawler No.k Hàm CFT4Cpp KLEE PathCrawler Số bộ dữ liệu kiểm thử Độ phủ Số bộ dữ liệu kiểm thử Độ phủ Số bộ dữ liệu kiểm thử Độ phủ 1 uninit_var 5 100 27 100 >20 100 2 ArrayCmp 3 100 82 100 1 16.67 3 check_prime 3 100 n/a 100 >20 66.67 4 check_armstrong 2 100 n/a 100 5 100 5 power 2 100 > 20 100 >20 100 6 print_floyd 2 100 n/a 100 >20 100 7 find_minimum 2 100 n/a 100 - - 8 linear_search1 2 100 n/a 100 1 25 9 linear_search2 2 100 n/a 100 2 25 10 bubble_sort 2 100 n/a 100 1 16.67 11 concatenate 1 100 n/a 100 - - 12 concatenate_string 1 100 n/a 100 - - 13 reverse2 2 100 8 100 1 50 14 copy_string 2 100 10 100 - - 15 string_length 2 100 10 100 - - 18 Fibonacci 2 100 n/a 100 - - 19 find_maximum 2 100 n/a 100 - - 20 add_digits 2 100 4 100 2 100 21 reverse 2 100 4 100 2 100 39 Điểm thứ hai từ kết quả thực nghiệm trong Bảng 4.4 là công cụ PathCrawler đạt kết quả không tốt trong nhiều ví dụ. Tiêu biểu như ví dụ ArrayCmp, linear_search1, v.v. công cụ đạt được độ phủ khá nhỏ. Thậm chí, trong ví dụ find_minimum, concatenate, v.v. công cụ PathCrawler không thể sinh được dữ liệu kiểm thử (kí hiệu bởi dấu “-“). Về vấn đề đầu tiên, nguyên nhân chính do công cụ PathCrawler chưa xử lý được nhiều trường hợp mã nguồn khi áp dụng kĩ thuật thực thi tượng trưng. Nguyên nhân của vấn đề thứ hai liên quan đến phương pháp kĩ thuật kiểm thử tự động định hướng. Trong phương pháp kĩ thuật kiểm thử tự động định hướng, dữ liệu kiểm thử đầu tiên được sinh ngẫu nhiên, và sau đó được đẩy vào chương trình để chạy. Nếu dữ liệu kiểm thử đầu tiên không chạy được, tức là chương trình có lỗi, quá trình sinh dữ liệu kiểm thử thất bại. Bảng 4.5. Kết quả so sánh công cụ CFT4Cpp với CREST và CAUT No.k Hàm CFT4Cpp CREST CAUT Số bộ dữ liệu kiểm thử Độ phủ Số bộ dữ liệu kiểm thử Độ phủ Số bộ dữ liệu kiểm thử Độ phủ 1 uninit_var 5 100 24 100 11 91.69 2 ArrayCmp 3 100 6 100 4 100 3 check_prime 3 100 5 100 3 83.331 4 check_armstrong 2 100 4 100 3 87.5 5 power 2 100 - - 2 100 6 print_floyd 2 100 - - - - 7 find_minimum 2 100 - - 4 100 8 linear_search1 2 100 3 100 2 100 9 linear_search2 2 100 3 100 2 100 10 bubble_sort 2 100 - - 3 100 11 concatenate 1 100 2 100 - - 40 12 concatenate_string 1 100 2 100 - - 13 reverse2 2 100 3 100 2 100 14 copy_string 2 100 2 100 1 100 15 string_length 2 100 2 100 1 100 18 Fibonacci 2 100 - - - - 19 find_maximum 2 100 - - 4 100 20 add_digits 2 100 2 100 1 100 21 reverse 2 100 2 100 1 100 Bảng 4.5 trình bày kết quả thực nghiệm khi so sánh công cụ CFT4Cpp với hai công cụ CREST và CAUT. Hai công cụ này đều áp dụng kĩ thuật kiểm thử tự động định hướng nên có những điểm yếu như công cụ PathCrawler nêu trên. Hai công cụ CREST và CAUT đều cho kết quả kiểm thử tốt hơn hẳn so với PathCrawler. Thứ nhất, trong ví dụ copy_string, string_length, add_digits, và reverse, công cụ CREST cho độ phủ 100% trong khi số lượng bộ dữ liệu kiểm thử bằng CFT4Cpp. Nguyên nhân chính bởi vì chiến thuật chọn đường thi hành của CREST tốt hơn PathCrawler nên số bộ dữ liệu kiểm thử nhỏ hơn hẳn. Thứ hai, công cụ CAUT thể hiện tính ưu điểm hơn trong các ví dụ copy_string, string_length, add_digits và reverse so với hai công cụ CFTCpp và CREST. Những hàm này đều chứa vòng lặp. CAUT chỉ cần sinh ra đúng một bộ dữ liệu kiểm thử mà vẫn đạt độ phủ tối đa. Lý giải cho vấn đề này là do tính may mắn khi CAUT sinh dữ liệu kiểm thử đầu tiên theo phương pháp ngẫu nhiên. Với dữ liệu kiểm thử đầu tiên “may mắn” này, độ phủ đạt được là 100%. Tuy nhiên, CAUT thất bại khi xử lý các hàm print_floyd, concatenate, v.v. 4.3.2. Sinh dữ liệu kiểm thử vòng lặp Phương pháp đề xuất LDFS ưu tiên sinh dữ liệu kiểm thử lặp khối lệnh điều khiển lặp (while...do, do..while, for) càng nhỏ càng tốt. Cụ thể, tập dữ liệu kiểm thử lặp vòng lặp 1 lần, 0 lần, 2 lần, v.v., đến lặp tối đa n lần được sinh ra theo thứ tự (n là giá trị cấu hình số lần lặp tối đa do người dùng định nghĩa). Một khi tập dữ liệu kiểm thử đạt độ phủ tối đa, quá trình sinh dữ liệu kiểm thử kết thúc mà không quan tâm 41 các lần lặp kế tiếp. Điều đó có nghĩa, tập dữ liệu kiểm thử sinh ra đạt tiêu chí độ phủ cao và số lượng ít. Thực tế, lỗi có thể phát sinh ở vòng lặp khi số lần lặp đủ lớn. Để đảm bảo chất lượng phần mềm, tập dữ liệu kiểm thử thỏa mãn một trong hai điều kiện sau cần được sinh ra gồm (i) độ phủ lớn và số lượng bộ dữ liệu kiểm thử nhỏ, (ii) kiểm thử vòng lặp. Tập dữ liệu kiểm thử thỏa mãn điều kiện đầu tiên được sinh bằng cách áp dụng LDFS. Phần này trình bày thực nghiệm sinh dữ liệu kiểm thử đánh giá chất lượng vòng lặp theo tiêu chí số lần lặp. Bảng 4.6. Sinh dữ liệu kiểm thử vòng lặp Ví dụ Mô tả Vòng lặp CC LOC Loại vòng lặp Vòng lặp kiểm thử Kiểu biên Số lần lặp tối đa Số lần lặp Số bộ dữ liệu kiểm thử Merge1 6 17 Vòng lặp nối tiếp i <3 && j < 3 Biên 6 0,1,2,5,6,7 1 i<3 Biên 3 0,1,2,3,4 1 j<3 Biên 3 0,1,2,3,4 1 check_ subsequence 6 13 Vòng lặp lồng nhau a[c]!= ‘\0’ Không xác định - 0,1,2,30 4 a[c]!=b[d] && b[d]!= ‘\0’ Không xác định - 0,1,2,26 4 find_ frequency 4 6 Vòng lặp đơn s[c]!=’0’ Không xác định - 0,1,2,50 4 Bảng 4.6 trình bày tập dữ liệu kiểm thử để kiểm tra tính đúng đắn vòng lặp. Ba loại vòng lặp sinh dữ liệu kiểm thử gồm vòng lặp đơn, vòng lặp lồng nhau (nested loop) và vòng lặp liên tiếp (concatenated loop). Trong bảng này, CC và LOC tương 42 ứng là độ phức tạp của hàm và số dòng mã nguồn được tính bằng cách sử dụng plugin metrics2∗∗ của Eclipse. Cột Vòng lặp kiểm thử mô tả khối lặp đang cần sinh dữ liệu kiểm thử để kiểm tra tính đúng đắn. Cột Kiểu biên mô tả loại khối lặp đang kiểm tra ở cột Vòng lặp kiểm thử. Nếu vòng lặp đang kiểm thử xác định được biên, số lần lặp tối đa thể hiện ở cột Số lần lặp tối đa, ngược lại đánh dấu “-“. Cột Số lần lặp mô tả số lượng lặp của vòng lặp đang kiểm thử để sinh dữ liệu kiểm thử. Cột cuối cùng Số bộ dữ liệu kiểm thử trình bày số lượng bộ dữ liệu kiểm thử sinh được thành công từ những lần lặp này. Ba ví dụ tiêu biểu ứng với ba loại vòng lặp được trình bày trong bảng. Hàm Merge1 ghép hai mảng thành một mảng tăng dần gồm 3 khối lệnh điều khiển while nối tiếp nhau (xem mã nguồn tại phụ lục). Do đó, tập dữ liệu kiểm thử cho từng khối lệnh điều khiển while được sinh ra để kiểm tra tính đúng đắn của vòng lặp. Xét khối while đầu tiên, điều kiện khối lệnh này xác định được số lần lặp tối đa bằng 6 (i<3 && j < 3, trong đó i, j khởi tạo bằng 0). Do đó, tập dữ liệu kiểm thử thỏa mãn lặp khối while đầu tiên này 0 lần (không lặp lần nào), 1 lần, 2 lần, 5 lần, 6 lần (số lần lặp tối đa), 7 lần (số lần lặp tối đa + 1) được sinh. Trong trường hợp này, chỉ có dữ liệu kiểm thử lặp 5 lần được sinh thành công. Những lần lặp còn lại không thể sinh dữ liệu kiểm thử thỏa mãn. 4.3.3. So sánh thời gian biên dịch và thực thi dữ liệu kiểm thử Bảng 4.7 so sánh thời gian biên dịch và thực thi dữ liệu kiểm thử giữa phương pháp cải tiến và phương pháp truyền thống. Tất cả mọi hàm đầu vào đều chứa biến kiểu dẫn xuất, và thuộc tính của những biến này có kiểu con trỏ. Tiêu chí độ phủ sử dụng trong bảng thực nghiệm này là độ phủ MC/DC. Xét ví dụ tiêu biểu calculateZodiac (mã nguồn ở phụ lục), đầu vào của hàm này là một đối tượng kiểu ngày tháng. Số nhánh thỏa mãn độ phủ điều kiện con trong ví dụ này lên tới 120 nhánh. Áp dụng phương pháp truyền thống, tổng số lần thực thi lên tới 74 lần, tổng thời gian biên dịch và chạy vượt quá 10 phút, độ phủ MC/DC đạt được hơn 90%. Trong đó, hơn nửa thời gian chạy là bước biên dịch 74 bộ thực thi dữ liệu kiểm thử này. Ngược lại, phương pháp cải tiến chỉ tiến hành biên dịch 74 dữ 43 liệu kiểm thử này duy nhất một lần. Kết quả, tổng thời gian biên dịch và chạy rút ngắn xuống 3 lần (còn hơn 267 giây). Bảng 4.7. Bảng so sánh thời gian biên dịch và thực thi dữ liệu kiểm thử giữa kĩ thuật cải tiến và kĩ thuật truyền thống Tên hàm Độ phủ Số lần thực thi Kĩ thuật truyền thống Kĩ thuật cải tiến Tổng thời gian (s) Biên dịch (s) Tổng thời gian (s) Biên dịch (s) calculateZodiac(Date) 90.8 74 656.82 60.15 267.19 2 struct_test1(SinhVien1) 100 4 12.5 76.22 5.62 44.48 class_test1(SinhVien) 75 4 11.92 88.22 4.05 65.19 StackLinkedList::push(Node*) 100 2 6.35 39.53 5.48 24.64 StackLinkedList::pop() 100 3 4.56 81.88 2.13 60.09 StackLinkedList::destroyList() 100 2 3.42 71.36 2.56 55.47 disp(Node*) 100 2 3.45 75.32 2.4 60.42 testDate0(Date) 100 2 23.4 97.39 12.01 94.92 44 KẾT LUẬN Luận văn đã trình bày một phương pháp phân tích mã nguồn và sinh dữ liệu kiểm thử tự động cho các dự án C/C++. Kết quả nghiên cứu của luận văn được hiện thực hóa trong công cụ CFT4Cpp. Tính đúng đắn và hiệu quả của phương pháp đề xuất đã được chứng minh trong thực nghiệm qua các so sánh với KLEE, PathCrawler, CUTE, CREST, CAUT. Hiện tại, kết quả nghiên cứu đã được trình bày trong hai hội nghị gồm NICS 2016 và SoICT 2017. Mục tiêu chính của luận văn hướng đến giải quyết vấn đề sinh dữ liệu kiểm thử đầu tiên trong kiểm thử kĩ thuật kiểm thử tự động định hướng, đề xuất phương pháp sinh tập dữ liệu kiểm thử số lượng nhỏ và đạt độ phủ tối đa. Thứ nhất, để giải quyết vấn đề sinh dữ liệu kiểm thử đầu tiên, phương pháp đề xuất tiến hành phân tích chương trình để sinh bộ dữ liệu kiểm thử đầu tiên thay vì sinh ngẫu nhiên. Bởi thế, quá trình thực thi dữ liệu kiểm thử đầu tiên sẽ gây ít lỗi hơn so với phương pháp sinh ngẫu nhiên, đặc biệt với chương trình thao tác với vùng nhớ như con trỏ, xâu, v.v. Thứ hai, để sinh số lượng bộ dữ liệu kiểm thử nhỏ mà đạt độ phủ tối đa, luận văn đề xuất thuật toán LDFS. Tư tưởng chính của thuật toán LDFS là sinh dữ liệu kiểm thử cho trường hợp càng đơn giản hết mức có thể để giảm thiểu chi phí phân tích mã nguồn mà vẫn đạt độ phủ tối đa. Cụ thể, tập dữ liệu kiểm thử được sinh thỏa mãn lặp vòng lặp tối đa một lần, tức là cả nhánh đúng và sai của câu lệnh điều kiện đều được đi qua. Sau bước này, nếu độ phủ đạt được chưa tối đa, LDFS tiến hành sinh dữ liệu kiểm thử thỏa mãn lặp vòng lặp tối đa 0 lần (tức chỉ đi theo nhánh sai của câu lệnh điều kiện), sau đó lặp 2 lần, 3 lần, v.v. đến số lần lặp tối đa được cấu hình từ trước. Quá trình sinh dữ liệu kiểm thử dừng lại khi độ phủ đạt được là tối đa, hoặc hết thời gian chạy, hoặc LDFS đạt đến số lần lặp tối đa của vòng lặp. Công cụ CFT4Cpp cần được tiếp tục phát triển để ngày càng hoàn thiện hơn. Thứ nhất, CFT4Cpp sẽ được nâng cấp để hỗ trợ đầy đủ cú pháp của các chuẩn C++98, C++03, C++11, và C++14. Để làm được điều này, kĩ thuật phân tích mã nguồn cần được cải tiến. Thứ hai, nhiều trường hợp trong dự án C/C++ cần được xử lý thêm như template, dynamic invocation, overloading, v.v. Thứ ba, thuật toán thực thi tượng trưng chưa giải quyết được vấn đề sử dụng bộ nhớ không tường minh khi sử 45 dụng hàm liên quan bộ nhớ như memmove, strncat. Kĩ thuật thực thi tượng trưng hiện tại chưa mô phỏng đầy đủ và chính xác được thay đổi của các biến khi những câu lệnh kiểu này được gọi. Thứ tư, công cụ cần được cải tiến để sinh dữ liệu kiểm thử cho các độ phủ khác bên cạnh ba độ phủ đã hỗ trợ sẵn gồm độ phủ nhánh, độ phủ câu lệnh và độ phủ MC/DC. Cuối cùng, công cụ hướng tới hỗ trợ nhiều trình biên dịch khác nhau trên các nền tảng khác nhau. 46 PHỤ LỤC // Hàm calculateAge struct Date { int date; int month; int year;}; int calculateZodiac(Date born) { int date1 = born.date; int month1 = born.month; int year1 = born.year; int t; if (((month1 == 3) && (date1 >= 21) && (date1 <= 31)) || ((month1 == 4) && (date1 <= 19))){ t = 1; } else if (((month1 == 4) && (date1 >= 20) && (date1 <= 30)) || ((month1 == 5) && (date1 <= 20))) { t = 2; } else if (((month1 == 5) && (date1 >= 21) && (date1 <= 31)) || ((month1 == 6) && (date1 <= 20))) { t = 3; } else if (((month1 == 6) && (date1 >= 21) && (date1 <= 30)) || ((month1 == 7) && (date1 <= 22))) { t = 4; } else if (((month1 == 7) && (date1 >= 23) && (date1 <= 31)) || ((month1 == 8) && (date1 <= 22))) { t = 5; } else if (((month1 == 8) && (date1 >= 23) && (date1 <= 31)) || ((month1 == 9) && (date1 <= 22))) { t = 6; } else if (((month1 == 9) && (date1 >= 23) && (date1 <= 30)) || ((month1 == 10) && (date1 <= 22))) { t = 7; } else if (((month1 == 10) && (date1 >= 23) && (date1 <= 31)) || ((month1 == 11) && (date1 <= 21))) { t = 8; } else if (((month1 == 11) && (date1 >= 22) && (date1 <= 31)) || ((month1 == 12) && (date1 <= 21))) { t = 9; } else if (((month1 == 12) && (date1 >= 22) && (date1 <= 30)) || ((month1 == 1) && (date1 <= 19))) { t = 10; } else if (((month1 == 1) && (date1 >= 20) && (date1 <= 31)) || ((month1 == 2) && (date1 <= 18))) { t = 11; } else if (((month1 == 2) && (date1 >= 19) && (date1 <= 29)) || ((month1 == 3) && (date1 <= 20))) { t = 12; } else t = -1; return t; } 47 // Hàm Merge1 // Should copy all the elements of ordered arrays t1 and t2 into the ordered array t3 // Link: pathcrawler-online.com void Merge1(int t1[3], int t2[3], int t3[6]) { int i = 0, j = 0, k = 0; while (i < 3 && j < 3) { if (t1[i] < t2[j]) { t3[k] = t1[i]; i++; } else { t3[k] = t2[j]; j++; } k++; } while (i < 3) { t3[k] = t1[i]; i++; k++; } while (j < 3) { t3[k] = t2[j]; j++; k++; } } // Hàm find_frequency // Find frequency of characters in a string // Link: void find_frequency(char s[], int count[]) { int c = 0; while (s[c] != '\0') { if (s[c] >= 'a' && s[c] <= 'z') count[s[c] - 'a']++; c++; } } 48 TÀI LIỆU THAM KHẢO [1]. J. Burnim and K. Sen. 2008. Heuristics for Scalable Dynamic Test Generation. In Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE ’08). IEEE Computer Society, Washington, DC, USA, 443–446. [2]. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI’08). USENIX Association, Berkeley, CA, USA, 209–224. [3]. Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM 56, 2 (Feb. 2013), 82–90. [4]. Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337– 340. [5]. Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed Automated Random Testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’05). ACM, New York, NY, USA, 213–223. [6]. James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (July 1976), 385–394. [7]. Guodong Li, Indradeep Ghosh, and Sreeranga P. Rajan. 2011. KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). Springer-Verlag, Berlin, Heidelberg, 609–615. [8]. George C. Necula, Scott McPeak, Shree Prakash Rahul, and Westley Weimer. 2002. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proceedings of the 11th International Conference on Compiler Construction (CC ’02). Springer-Verlag, London, UK, UK, 213– 228. 49 [9]. Dirk Riehle. 1997. Composite Design Patterns. In Proceedings of the 12th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA ’97). ACM, New York, NY, USA, 218–228. [10]. Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A Concolic Unit Testing Engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE-13). ACM, New York, NY, USA, 263–272. [11]. T. Su, G. Pu, B. Fang, J. He, J. Yan, S. Jiang, and J. Zhao. 2014. Automated CoverageDriven Test Data Generation Using Dynamic Symbolic Execution. In 2014 Eighth International Conference on Software Security and Reliability (SERE). 98–107. [12]. Z. Wang, X. Yu, T. Sun, G. Pu, Z. Ding, and J. Hu. 2009. Test Data Generation for Derived Types in C Program. In 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering. 155–162. [13]. Nicky Williams, Bruno Marre, Patricia Mouy, and Muriel Roger. 2005. PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis. In Proceedings of the 5th European Conference on Dependable Computing (EDCC’05). Springer-Verlag, Berlin, Heidelberg, 281–292 [14]. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. 2008. EXE: Automatically Generating Inputs of Death. ACM Trans. Inf. Syst. Secur. 12, 2, Article 10 (Dec. 2008), 38 pages. D~I HOC QUOC GIA HA NQI TRU"ONG D~I HQC CONG NGHE: ------w ------ C<)NG HOA XA H<)I CHU NGHiA VIE:T NAM D(}c l~p- Tl! do- H~nh phuc *********** Ha N{Ji, ngay .. Z-thang 12 niim 2017 QUYETNGHJ CUA HQI DONG CHAM LU~N VAN TH~C Si Can Clr Quy€t djnh s6 1138/QD-DT, ngay 23 thang 11 nam 2017 cua Hi~u tru6ng truemg D~i hQC Cong ngh~ v€ vi~c thanh l~p H(>i dbng ch~m lu~n van th~c si cua h9c vien Nguy~n Due Anh, H(>i dbng ch~m lu~n van Th~c si da hQp vao 14h, thu 7, ngay 02 thang 12 nam 2017, Phong 309, Nha E3, Truo·ng D~i hQc Cong ngh~- DHQGHN. Ten d€ tai lu~n van: Phuong phap phan tich rna ngufin va sinh dfr li~u ki~m thlr cho cac dl}' an C/C++ Nganh: Cong ngh~ Thong tin Chuyen nganh: Ky thu~t phftn m~m Mas6: Sau khi nghe h9c vien trinh bay tom tAt lu~n van Th~c si, cac phim bi~n d9c nh~n xet, h9c vien tra lai cac cau hoi, H(>i dbng da hQp, trao d6i y ki€n va thfJng nh~t k€t lu~n: 1. V~ tinh cftp thi~t,Jinh th(ri S\f, y nghia ly lu~n va th\fC ti~n CUa d~ tai lu~n van: ...... {)i~ ... k. .... ~ .... v.tl:;, ....... U: ..... ti. .. ~~-~ ...... ~ ....... ll.~ ..... ~ ..... t.:~~ .. ~ ~ {/ '·7~ , .. 2. Vi bB Ct}.C, phuO"ng phap nghien CUU, tai li~U tham khao, ..... CUa lu~n van: .................. ·; ............................................... ) .. ...... ·o ..... ~ ............ ~- ................. ·;~ .................... , ........ ·p .... ~- ........ t~· .. . .. -=: .. /f,£. ... ~·······4····~····~--~·····~······,?16r; ...... ~f;;-]······ ::c:::::flt::::j:::;x.;;::::::::;;p;:::::~::::r::·~~:::::::;x:::;&~~:::::~::::: ~:::::::~-:::::zE/::·:~:::~:::.::J??::::::~:::::::i!1':::::·~:1:::--:::::::::::::::::::::·:::-::: 3. v~ k~t qua nghien cuu: =---ii:~--~----~-~---4···4'. ..... ~~---··;4 ... r-~-f···;£;·~-~·-····~---·· -~······~·-f:··-'·: .. ~ .......................................................................................................................................... . ·············~············;·)·················~··························;·············.:.:.·························/··;1·····················:;································· =--~ .... ,KJ.J..itl ..... h······-N·····w. ...... Oa_ ....... ~ ....... L ................................... . :;:~:::::::ZiJ:::::::~::::::~::::::::i :::z:;i::~:;;:_:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 4. H~n ch~ ciia lu~n van (n~u co): ::::::::;za.:::;;z::::::~:::::::~::::~:::::::L::.t.::::::~:~:::::::::::::::::::::::::::::::::::::::::::: - .......... , ... ~······························f'····························································································r································r······· ~ ...... kk. ...... d.:. ..... ;;~ ...... ~ ....... ~ ...... ~~-······Ld: ...... ~~ . .A ..... ~ ...... ~d?. .... . I , - ;::::c;i,::::;;R;i::·::;.:::;t;i:::::;;.J.:::::~::::::~:::::::;z.::::;;.::::~:::::~&J.:'.:::::: 5. Danh gia chung va k~t lu~n: /) r ... ~ .... Mt!it. .... ~ ... u, ..... ~ ... cX.. .... uJ. ..... ~Y..::_~······~·-··-~····-~~­ .{;/,1.J .... fH:4. .... ~ ..... y~---·~·-······~····· ~-····~································································ :::::-::::::::::::::::::::::::::::::::::.::::::::::::-:::::::::::::::::::::::::::::::::::::::::::1::::::::::::::::::::::::::::::::::::::::::::::::::.:::::::::::::::::::::::::::: Lu~n van d~t f...~ . ./ 10 di€m. Quy€t ngh! nay OUQ"C ... :s:. I .s:: ... thanh vien cua H(>i a6ng nhftt tri thong qua. THU' KY H<)I DONG CHU TJCH H<)I DONG 11 T(Lu i!j /Jr( /-{ ~ ,__ XACNH~~CUACOS6DAOT~O :·r r !~ \ \Tl!'tT '\..T • '·r , , · Ur il ,l r"t.. · ~ ...... l "i "~ "·~ .t - H ~· n h ph U. c BAN NHAN XET PHAN BIEN LUAN VAN THAC Si . . . . HQ va ten can b<) phan bi~n: Le Quang Minh HQC haiTI, hQC vi: Chuyen nganh: May tinh va H~ th6ng tinh toan Co quan cong tac: Vi~n Cong ngh~ thong tin - DHQGHN HQ va ten hQc vien cao hQc: Nguy~n Drrc Anh Ti~n sy Ten d~ tai lu~n van: PhrrO'ng phap phan tich rna nguBn va sinh dfr li~u ki~m thrr cho cac dlf an C/C++ Chuyen nganh: Ky thu~t ph~n rn~rn Ma s6: 60.48.01.03 Y KIEN NH~N XET 1. Tinh cdp thiit, thai Sl:f, y ngh'ia khoa hQC va thvc tiln cita aJ tai lu(jn van. Ngon ngfr l~p trinh C/C++ vfrn la ngon ngfr trong han 70% cac dv an phat tri6n h~ thf>ng nhung, vi v~y vi~c nghien Clru cac ky thu~t ki6rn thtr cho cac dV an tren ngon ngfr C/C++ luon la rn<)t doi hoi d~t ra. Lu~n van nay t~p trung nghien c(ru v~ vfrn d~ phan tich rna ngu6n va sinh ca ki6rn thu tv d<)ng cho cac dv an C/C++, d~ tai nay c6 y nghia thai sv, khoa hQc, phil hqp v6i lu~n van th~c sy chuyen nganh ky thu~t ph~n rnern. 2. Sv khong trung l¢p cua a~ tai nghien ciru so vai cac cong trinh khoa h9c, lucjn win aa cong b6 a trong va ngoai nuac; tinh trung thvc, ro rang va ady au trong trich ddn tai li¢u tham khao. Lu~n van c6 sv t6ng hqp va phat tri6n tir nhi~u ngu6n tai li~u, c6 sv trich dfrn r5 rang. Cach thuc trich dfrn tai li~u nghiern tuc. Khong phat hi~n ra sv trilng l~p v6i cac lu~n van tru6c day. 3. Sv phil hQ'p gifra ten a~ tai vai n9i dung nghien CUu, cung nhu vai chuyen nganh va ma s6 aao tqo. Ten d~ tai va n<)i dung d~ tai phil hqp v6i nhau, phil hqp v6i chuyen nganh va rna s6 dao t~o. 4. D9 tin ccjy va tinh hi?n aqi cita phuang phap nghien CUu aa sir dZJng a~ hoan thanh lucjn van. D~ tai c6 sv trich dfrn tir nhi~u ngu6n tai li~u, cac tai li~u th6 hi~n sv phong phu, c~p nh~t phil hqp v6i llnh vvc cua d~ tai. Pi;. __ c(ru. 5. J(dt qzf(z nglzien cz!·u ;n(li CltLt /(lC giu: dc)ng gop mO'i cho s~r pluit trien chuyen ngc7nh: t/ong gop 1no·i ph~tc v~1 san xuci1. kinh rd. xa h(Ji, an ninh, qubc phong va t/o·i sbng. Y nghza khoa h9c, gia trf vet (19 1 in c4_v czla nhfing kit qua nghien cz'ru. Lu<;ln van trinh bay t6ng quat chung v~ l) thuy~t sinh ca ki~1n thu tg d<)ng d6i v&i dv an C/C++, d€ xuclt cac cai ti~n ti~p c<;ln theo huang sinh ca ki~m thu dftu tien d~ tir d6 se c6 s6 luqng ca ki~1n thu nho nhclt v&i d(> phu t6i da. Cac k~t qua nay da duqc thu nghi~1n va cong b6 trong ky y~u khoa hQc cua 2 H<)i nghi NICS 2016 va SoiCT 2017. 6. Uu aiim va nhu(JC aiim v~ n(Ji dung, bb Cl;lC va hinh thuc cua luqn van. Lu<;ln van nhin chung dap ung cac yeu cftu ca ban cua lu?n van th~c sy nganh Cong ngh~ thong tin, chuyen nganh Ky thu?t phftn m€m, tuy nhien v~n con m<)t s6 di~m nen luu y d~ chinh sua cho hoan thi~n han: - Hinh thuc: Dftu dong cftn thvt vao, khoang each trang phai theo dung quy dinh. Nhi€u cau van chua duqc chau chu6t, cvt lun ho~c khong r5 nghia; - Ten gQi cac chuang nen duqc d~t l~i cho r5 y nghia cua cac chuang, hi~n nay n~u chi nhin vao mvc lvc khong r5 lu?n van lam gi va cai ti~n gi; - Trong lu?n van xuclt hi~n cac tir lu?n an, kh6a lu?n t6t nghi~p, khong r5 la tac gia c6 sv nhftm l~n hay c6 sv copy 6 dau trong qua trinh vi~t lu?n van. 7. Kit luqn chung Lu?n van dap ung duqc yeu cftu cua m<)t lu?n van t6t nghi~p th~c sy, toi de nghi H<)i dbng cho phep hQc vien duqc phep bao v~ tru&c H<)i dbng. Ha N <)i, ngayl. thang 1(tnam lJ)) }- CAN BQ PHAN BI~N TS. Le Quang Minh C<)NG HOA xA H<)I CHU NGHiA VI~T NAM D(}c I~p - Tv do - H~nh phuc ===================== BAN NH~N xET PHAN BI~N LU~N VAN TH~C Si HQ va ten can b{) phan bi~n: Truang Ninh Thu~n HQc ham, hQc vi: PGS.TS Chuyen nganh: CNTT Ca quan c6ng tac: Truemg DH C6ng ngh~ - DHQGHN HQ va ten hQc vien cao hQc: Nguy~n Due Anh Tend~ tai lu~n van: Phuang phap phan tich rna ngu6n va sinh dfr li~u ki~m thu cho cac dv an C/C++ Y KIEN NH~N XET Ki~m thu d6ng vai tro quan trQng trong quy trinh phat tri~n phAn m~m, cho phep ki~m tra cac I6i c6 th~ xay ra trong chuang trinh phAn m~m. M{)t trong cac thach thuc cua vi~c ki~m thu la sinh dfr li~u dAu vao d~ vi~c ki~m thu chuang trinh hi~u qua. Lu~n van nghien Clru v~ phuang phap phan tich rna ngu6n va sinh dfr li~u ki~m thir cho cac d\f an C/C++ la m{)t d~ tai c6 y nghia khoa hQc va thvc ti~n cao. 1. N{)i dung lu~n van bao g6m 5 chuang: Chuang 1 neu phAn d~t vfin d~. Chuang nay nen chuy~n thanh Gi6i thi~u trong d6 c6 phAn d~t vfin d~, gi6i thi~u n{)i dung va cfiu true kh6a lu~n. Chuang 2 gi6i thi~u v~ ca sa ly thuy~t, tac gia trinh bay cac ki~n thuc vS ki~m thu. Chuang 3 trinh bay phuang phap sinh ca ki~m thir tir rna ngu6n chuang trinh C/C++ Chuang 4 gi6i thi~u c6ng C\} h6 trq va thvc nghi~m. Chuang 5 la phAn k~t lu~n cua lu~n van. 2. D6ng g6p cua lu~n van: - Tim hi~u v~ ki~m thu va phan tich rna ngu6n - Xay d\fllg phuang phap sinh ca ki~m thu tir rna chuang trinh C/C++ - Xay dvng c6ng cv sinh ca ki~m thu tv d{)ng 3. H~n ch~ cua lu~n van: - H~n ch~ v~ cfiu true, trinh bay, I6i chinh ta - Chua lam r5 vi~c sinh ca ki~m thu thS nao, hi~u qua cua cac ca ki~m thu sinh ra trong vi~c tim 16i chuang trinh ph~n mSm. 4. KSt lu~n chung: Lu~n van dap irng cac yeu c~u cua m<)t lu~n van th~c sy nganh CNTT, chuyen nganh KTPM. Ha N<)i, ngay 01 thang 12 nam 2017 :xAc NH~N CUA CO QUAN CONG TAC CAN B<) PHAN BI~N _/LI~17~ r'l~ •. / .--" jV'" '/r)