Tóm tắt Luận án Một số cải tiến về ràng buộc xâu trong sinh dữ liệu kiểm thử tự động cho thực thi tượng trưng

phép nối xâu y=x -1 Phép đảo ngược xâu y=x[i..j] Lấy về xâu con của xâu x n=find(x,y) n là chỉ số đầu tiên xuất hiện của xâu x trong xâu y y = replace(x, q, q′ ) y có được bằng cách thay thế lần xuất hiện đầu tiên của q bằng q‟ trong x. y = replaceAll(x, q, q′ ) y có được bằng cách thay thế tất cả q bằng q‟ trong x n = count(a, x) n là số lần xuất hiện của kí tự a trong x x ∈ L(R) x thuộc ngôn ngữ chính quy được biểu diễn bởi R x ∈ L(G) x thuộc ngôn ngữ phi ngữ cảnh được biểu diễn bởi G Ví dụ như ràng buộc substring(x,y) có nghĩa là xâu x phải là xâu con của xâu y có thể được định nghĩa tương đương với ràng buộc find(x,y) được định nghĩa trong[54] cũng có thể tham chiếu tương đương với ràng buộc indexOf(y,x). Thứ tự của các kí tự trong xâu cũng tùy biến, trong một cách tiếp cận giải ràng buộc xâu thứ tự đầu tiên trong xâu được bắt đầu là 0 nhưng với một số cách tiếp cận thì nó là 1 khi đó kí tự 6 đầu tiên của xâu lại là x[1] thay vì x[0]. Nói tóm lại mục tiêu của giải ràng buộc xâu nhằm xác định xem có tồn tại các giá trị của các biến xâu có thỏa mãn một biểu thức ràng buộc đã cho hay không và nhiệm vụ này có thể được giải quyết bởi hai phương pháp là lập trình ràng buộc và lý thuyết thỏa mãn. 1.6. Kết luận chƣơng 1 Chương 1 của luận án đã trình bày các khái niệm nền tảng của nghiên cứu bao gồm các kỹ thuật kiểm thử phần mềm, các kỹ thuật cơ bản sinh dữ liệu kiểm thử tự động từ mô hình đang quan tâm. Đồng thời cũng đã đánh giá so sánh các kỹ thuật kiểm thử hộp trắng theo hướng động và tĩnh, chỉ ra các thách thức về kiểm thử phần mềm chưa được giải quyết. Trong đó kỹ thuật thực thi biểu trưng đang là vấn đề có triển vọng nghiên cứu. Các kiến thức nền tảng và tổng quan về kỹ thuật thực thi biểu trưng cũng như các thách thức, các vấn đề chưa được giải quyết cũng được trình bày trong chương này. Các nội dung liên quan đến giải ràng buộc xâu ứng dụng trong sinh tự động các ca kiểm thử sẽ được trình bày trong các chương tiếp theo của luận án. CHƢƠNG 2. THỰC THI BIỂU TRƢNG VÀ MÔ HÌNH HÓA RÀNG BUỘC Trong chương này, các khó khăn của kỹ thực thực biểu trưng sẽ được phân tích đánh giá. Đồng thời, các công cụ mở rộng, cài đặt kỹ thuật thực thi biểu trưng mà nó sẽ được dùng để thực hiện cải tiến kỹ thuật mô hình hóa ràng buộc kiểu xâu cũng được giới thiệu. Ngoài ra, phương pháp mô hình hóa phục vụ cho cài đặt, đánh giá giải ràng buộc xâu và ràng buộc hỗn hợp cũng được trình bày trong chương này. Nội dung chương này được thể hiện trong các kết quả công bố [CT1], [CT2], [CT3] của tác giả. 2.1. Những khó khăn và một vài giải pháp Trong phần này, những khó khăn trong quá trình áp dụng thực thi biểu trưng được thảo luận và một vài giải pháp cho việc giải quyết các thách thức đặt ra được trình bày. 2.1.1. Bùng nổ đường đi Một trong những thách thức quan trọng của thực thi biểu trưng là nó sẽ sinh ra một số lượng lớn các đường thực thi mặc dù chương trình là nhỏ và thường là hàm mũ trong số các câu lệnh rẽ nhánh tĩnh của mã nguồn. Kết quả là trong một khoảng thời gian định trước nó sẽ quyết định khám phá con đường đầu tiên sao cho phù hợp nhất. 2.1.2. Mô hình hóa bộ nhớ Độ chính xác của các câu lệnh của chương trình khi chuyển sang các ràng buộc biểu trưng có ảnh hưởng đáng kể đến độ bao phủ khi thực hiện thực thi biểu trưng cũng như khả năng giải các ràng buộc. Ví dụ khi sử dụng mô hình hóa bộ nhớ mà xấp xỉ để thiết lập độ rộng cho tham biến kiểu Interger có thể có hiệu quả hơn trong thực tế nhưng mặt khác kết quả lại thiếu chính xác trong phân tích mã nguồn. Nó phụ thuộc vào khoảng lựa chọn giá trị tương ứng như lỗi tràn bộ nhớ toán học, cũng có thể gây ra thiếu đường dẫn trong thực thi biểu trưng, hoặc khai phá những đường đi không khả thi vv.. 2 .2. Thực thi biểu trƣng và công cụ mở rộng 2.2.1. Thực thi biểu trưng và kiểm thử phần mềm Kỹ thuật sinh dữ liệu kiểm thử sử dụng thực thi biểu trưng được cài đặt trên ngôn ngữ Java để sinh dữ liệu kiểm thử cho các chương trình. Tuy nhiên, hiệu năng công cụ hiện có còn hạn chế: thời gian thực thi khá lớn. Việc áp dụng thuật toán tối ưu các ràng buộc - biểu diễn các lộ trình thực thi mã nguồn - nhằm giảm thời gian thực thi, nhưng vẫn đảm bảo hiệu quả bao phủ. Giải pháp cải tiến được thử nghiệm trên tập các chương trình Java khác nhau và cho kết quả rất khả quan. Nội dung phần này trình bày về JPF như khả năng kiểm tra của JPF, kiến trúc mức cao của JPF và khả năng mở rộng của JPF. 7 2.2.2. Thực thi biểu trưng trên ngôn ngữ Java Giới thiệu về Java PathFinder (JPF) Ngày nay kỹ thuật thực thi biểu trưng cho phép thực hiện trên nhiều công cụ và ngôn ngữ khác nhau như là DART[36], CUTE[35] là các công cụ cho ngôn ngữ C/C++, hay PEX[36,37] cho các mã nguồn .NET tuy nhiên trong luận án này lựa chọn sử dụng Path Finder cho ngôn ngữ Java. Lý do là Java là ngôn ngữ độc lập với môi trường và có nhiều ứng dụng quan trọng được xây dựng trên nền tảng java, một lý do khác là công cụ JPF là một công cụ mạnh mẽ hỗ trợ cho kỹ thuật thực thi biểu trưng nó cho khả năng mở rộng và có một cộng đồng phát triển rộng rãi. JPF là một bộ kiểm chứng mô hình phần mềm trạng thái tường minh cho Java [68]. Hiểu một cách cơ bản JPF là một máy ảo thực thi chương trình Java không chỉ một lần (giống như các máy ảo thông thường), mà thực thi trong tất cả các nhánh, các đường đi có thể. JPF sẽ kiểm tra các vi phạm thuộc tính như khóa chết hoặc các ngoại lệ không thể bắt được xuyên suốt các đường thực thi tiềm năng. Hình 2.1 mô tả mô hình hoạt động của JPF. Hình 2.1. Mô hình hoạt động của JPF Khả năng kiểm tra của JPF JPF có thể kiểm tra tất cả các chương trình Java. JPF có thể tìm ra các khóa chết hoặc ngoại lệ. Ngoài ra chúng ta có thể tự phát triển mở rộng để kiểm tra các thuộc tính khác. Kiến trúc mức cao của JPF JPF được thiết kế (như Hình 2.3) thành 2 thành phần chính đó là: JVM, và Search. Trong đó, JVM là một bộ sinh trạng thái cụ thể Java. Bằng việc thực hiện các chỉ thị Java bytecode. Search chịu trách nhiệm lựa chọn trạng thái mà JVM nên xử lý, hoặc hướng JVM sinh trạng thái tiếp theo, hoặc yêu cầu JVM quay trở lại một trạng thái trước đó. 8 Hình 2.3. Biểu diễn sơ đồ kiến trúc mức cao của JPF. Các cài đặt chính của Search bao gồm tìm kiếm theo độ sâu (DFSearch) và HeuristicSearch. Trừu tượng hoá: Là quá trình loại bỏ các chi tiết không liên quan đến thuộc tính để có được các mô hình hữu hạn đơn giản đủ để xác minh thuộc tính Trừu tượng hoá dữ liệu: Hàm trừu tượng hoá h biến đổi từ S thành S‟ (Hình 2.4, 2.5) Hình 2.4. Ví dụ về trừu tượng hoá dữ liệu. 9 Hình 2.5. Một ví dụ khác về trừu tượng hoá dữ liệu. Quy trình trừu tượng – sàng lọc dữ liệu (Hình 2.6): Các bước thực hiện: i. Xây đựng mô hình trừu tượng hoá mới ii. Kiểm tra mô hình: + Nếu đạt yêu cầu thì không có lỗi, + Nếu không đạt yêu cầu, kiểm tra các ví dụ truy cập (Các truy cập hợp lệ sẽ có lỗi, các truy cập không hợp lệ sẽ có các gợi ý sàng lọc.) Hình 2.6. Quy trình sàng lọc dữ liệu. Dựa trên các gợi ý sàng lọc, mô hình trừu tượng hoá mới sẽ được xây dựng. Quy trình này dừng trong các trường hợp không có lỗi hoặc có lỗi. Nhược điểm: Mất độ chính xác Khả năng mở rộng của JPF JPF có thể được coi như là một Framework mà tại đó bất kỳ nhà phát triển nào đều có thể mở rộng để phục vụ cho một mục đích cụ thể. JPF cung cấp một cơ chế mở rộng để cho phép thêm vào các chức năng mới mà không phải thay đổi trực tiếp cài đặt của Search hoặc JVM. Với kiến trúc mở rộng linh hoạt, hiện nay đã có một số mở rộng được phát triển cho JPF 10 2.3. Giải các ràng buộc và thực thi biểu trƣng Liên quan đến sinh các ca kiểm thử, hướng tiếp cận dựa trên giải thuật di truyền đã được tìm hiểu trong công trình nghiên cứu CT[1] của nghiên cứu sinh. Tuy nhiên, cách tiếp cận này thể hiện nhiều hạn chế. Mặc dù đã có những tiến bộ đáng kể trong kỹ thuật thực hiện giải các ràng buộc trong những năm gần đây, giúp cho thực thi biểu trưng trở nên thực tế hơn, nhưng việc giải các ràng buộc vẫn là cản trở đáng kể của thực thi biểu trưng. Nó thường chiếm nhiều thời gian trong quá trình thực hiện và là một trong những lý do chính khiến thực thi tượng trưng không mở rộng được với một số loại chương trình mà mã nguồn của nó sinh ra với yêu cầu rất lớn trong việc giải các ràng buộc. Kết quả là cần thiết phải thực hiện tối ưu khi giải các ràng buộc được sinh ra trong quá trình thực thi biểu trưng trong những chương trình thực tế. Hai phương pháp tối ưu được sử dụng bởi các công cụ hiện tại bao gồm: Loại bỏ ràng buộc không liên quan Giải ràng buộc theo phương pháp gia tăng (Increamental Solving) [71] Một trong những tính chất quan trọng của tập các ràng buộc được tạo ra trong quá trình thực thi biểu trưng là nó mô tả biểu diễn cho một tập các nhánh tĩnh từ mã nguồn của chương trình. Trong KLEE tất cả các kết quả truy vấn được lưu vào vùng nhớ đệm ánh xạ tập các ràng buộc và các giá trị cụ thể tìm được tương ứng với ràng buộc đó (trong trường hợp đặc biệt không có lời giải hoặc không thỏa mãn tương ứng với một kí hiệu đặc biệt). 2.4. Ràng buộc hỗn hợp và cải tiến trong giải ràng buộc xâu Trên thực tế, kiểu dữ liệu xâu xuất hiện trong hầu hết các chương trình, đặc biệt là trong những đoạn chương trình hoặc phương thức nhằm “làm sạch” xâu dùng cho dữ liệu đầu vào của các chương trình nhằm kiểm tra tính hợp lệ cũng như phát hiện và loại bỏ các nội dung độc hại. Với một thư viện rộng lớn, kiểu dữ liệu xâu trong ngôn ngữ Java còn ẩn chứa nhiều lỗi. Với mong muốn hoàn thiện khả năng kiểm thử và phát hiện lỗi trên những chương trình Java có sử dụng kiểu dữ liệu xâu, nội dung luận án quan tâm đến việc xác định lỗi để có những phần mềm hoàn thiện hơn. Áp dụng kiểm thử phần mềm sử dụng kiểu dữ liệu xâu nhằm tăng khả năng bao phủ hướng tới nâng cao chất lượng phần mềm. Tại sao thực thi biểu trưng trên kiểu dữ liệu xâu lại khó khăn? Các phép toán xâu là sự trộn lẫn giữa hai miền giá trị, cụ thể là xâu và số nguyên. Ví dụ phép toán lấy kí tự thứ n của xâu. Hiện tại những giải pháp được đưa ra để thực thi biểu trưng cho kiểu dữ liệu xâu nhưng nó mới chỉ dừng lại ở việc chỉ hỗ trợ một tập con các phép toán đó hoặc thường là không có gì đáng kể. Ta thực hiện cách tiếp cận lặp đi lặp lại, trong đó đầu tiên ta thực hiện giải các ràng buộc trên kiểu dữ liệu số nguyên, sau đó sử dụng kết quả đó để giải ràng buộc xâu và nếu nó được thỏa mãn thì công việc được hoàn thành. Mặt khác các ràng buộc kiểu nguyên được thêm vào bổ sung và quá trình này được lặp đi lặp lại. Ý tưởng cốt lõi cho việc mở rộng kỹ thuật thực thi biểu trưng mà nghiên cứu này đề xuất được chỉ ra trong Hình 2.7 dưới đây. 11 Hình 2.7. Đồ thị xâu Tiếp theo, quá trình lặp được thực hiện với hai bước như sau: - Bước 1: Bộ giải ràng buộc hiện thời của JPF được gọi để xử lý các ràng buộc kiểu nguyên, kiểu thực, kiểu logicvà nếu nó giải được chuyển qua bước 2 - Bước 2: Các giá trị cụ thể thu được từ bước 1 được truyền tới cho đồ thị xâu và khi đó bộ giải ràng buộc xâu được gọi để giải chúng. Trong trường hợp này, “bộ giải ràng buộc xâu” có thể là AutomataSolve hay là BitVectorSolve và có thể ràng buộc của đồ thị xâu không thỏa mãn với các giá trị nhận được và nếu thời gian giới hạn còn thỏa mãn ta thực hiện quay lại bước 1 và ràng buộc xâu sẽ được thêm các ràng buộc mới. Solve(PathCondition pc){ 1: StringGraph sg; 2: sg=BuilStringGraph(pc); 3: boolean sat=false; 4: While(!sat and !timeout){ 5: sat=CurrentSolver(pc,sg); 6: if(sat) 7: sat=StringSolver(pc,sg); 8: return sat; } } buildStringGraph(PathCondition pc) { 1: StringGraph sg ; 2: for string or mixed constraint c 2 pc: 3: sg= sg hyperedge(c) 4: return preprocess(pc; sg) } Hình 2.8. Thuật toán giải ràng buộc hỗn hợp Giá trị giới hạn thời gian “timeout” được đưa vào để đảm bảo trong trường hợp sự kết hợp giữa hai bộ giải ràng buộc kiểu xâu và ràng buộc kiểu nguyên vẫn không thể đưa ra được kết luận cuối cùng trong một thời gian cho phép. Khi đó thuật toán vẫn dừng với kết luận ràng buộc trên là không thỏa mãn. 2.4.1. Đồ thị xâu Các loại ràng buộc có thể được phân loại thành ràng buộc kiểu xâu, ràng buộc kiểu nguyên, ràng buộc hỗn hợp kiểu xâu và kiểu nguyên. Trong quá trình cài đặt, ràng buộc kiểu xâu và ràng buộc hỗn hợp được biểu diễn bởi một đồ thị đặc biệt gọi là đồ thị xâu. 12 Định nghĩa: Đồ thì xâu là một loại đồ thị có hướng H=(X, E, Ʊ). Trong đó, tập đỉnh được xác định bởi X=I S với I và S là lai tập rời nhau (I là tập biểu diễn cho các biến kiểu nguyên và S là tập biểu diễn cho các biến kiểu xâu). Tập Ʊ thể hiện cho phép toán trên xâu. Đồng thời, nó cũng thể hiện tập các cạnh gán nhãn có hướng (E = E1 E2 E3 E4) sao cho En= Ʊ X n . Sử dụng đồ thị là phương pháp phổ biến trong lập trình thỏa mãn ràng buộc. Hình 3.1 mô tả ví dụ cho đồ thị xâu tương ứng với ràng buộc: s1.trim().equals(s2)^s1.equals(s3.concat(s2)) 2.4.2. Xây dựng lại ràng buộc Phục vụ cho giai đoạn tiền xử lý, với mỗi ràng buộc xâu hoặc ràng buộc hỗn hợp của điều kiện ràng buộc đường đi, đóng góp vào một cạnh của đồ thị xâu, nó xây dựng lại ràng buộc bởi ràng buộc và giá trị trả về của phép toán được ánh xạ trực tiếp vào các cạnh của đồ thị xâu. Ví dụ: ràng buộc s1.equals(s2) thêm vào cạnh (equals, s1,s2) với những toán tử khác. Giá trị trả về có thể là là kiểu kí tự, kiểu nguyên hoặc kiểu xâu. Một biến phụ được sinh ra và đại diện cho kết quả của phép toán. Biến phụ này được thêm vào như là một đỉnh của đồ thị xâu. Nó cho phép cạnh được thêm vào như là một trường hợp của giá trị trả về. Trong ví dụ được trình bày ở Hình 2.9 dưới đây, vòng tròn mô tả cho đỉnh, dấu chấm và đường thẳng mô tả cho cạnh. Mỗi cạnh được gắn nhãn biểu diễn cho phép toán tương ứng và con số chỉ ra thứ tự của đỉnh đồ thị xâu tương ứng với một ràng buộc. Các biến xâu s1, s2 và s3 xuất hiện như là đỉnh của S với đồ thị này thì Ʊ = {trim, equals, concat}. Phép toán trim sẽ sinh ra một biến phụ s‟ được thêm vào S. Tự bản thân phép toán chính là cạnh (trim, s1, s‟) được gắn nhãn là phần tử trim của Ʊ và nối đỉnh s1 với s‟. Tương tự phép toán concat là ràng buộc thứ hai sinh ra biến phụ s” và cạnh (concat, s3, s2, s”). Cuối cùng hai phép toán equals sẽ tương ứng với hai cạnh còn lại. Khi một đồ thị xâu được xây dựng xong, nó sẽ được tiền xử lý theo hai cách: 1. Xác định một cách đơn giản các ràng buộc nào là không có giá trị thỏa mãn 2. Thêm vào các giá trị được sinh ra bởi bộ giải ràng buộc nguyên vào biểu thức ràng buộc đường đi. 2.4.3. Quá trình tiền xử lý Khi phát hiện những ràng buộc không có giá trị thỏa mãn, quá trình thực thi sẽ tránh được việc mất thời gian cho bộ giải ràng buộc xâu. Một trong những đề xuất là loại bỏ cạnh equals khỏi đồ thị xâu. Với ví dụ như trên, đồ thị xâu được chuyển thành đồ thị xâu được đưa ra ở Hình 2.9 dưới đây. Hình 2.9. Đồ thị sau khi loại bỏ phép toán equals. Và điều này cũng giúp nhanh chóng xác định tập các ràng buộc được biểu diễn trong đồ thị xâu là không có giá trị thỏa mãn. Ví dụ (xem Hình 2.10) sau khi loại bỏ cạnh trong Hình 2.10.(a) đỉnh s1 tự nối với 13 nó bằng cạnh notEquals được chỉ ra trong Hình 2.10.(b) và rõ ràng rằng không tồn tại xâu nào thỏa mãn ràng buộc này. Hầu hết những đề xuất để giải quyết với những trường hợp phép toán là hằng số. Ví dụ: ràng buộc là s1.concat(“xyz”) = ”vwxyz” sẽ dẫn đến việc loại bỏ các cạnh phức tạp và thay thế đỉnh s1 bằng xâu vw. Một ví dụ khác cho ràng buộc s1.startsWith(“abc”).chatAt(0) ≠ „a‟ là không phù hợp và dễ dàng phát hiện. Nếu tình huống này phát sinh trong giai đoạn tiền xử lý, sẽ tránh được khi gọi bộ giải ràng buộc xâu và nhanh chóng trả về giá trị false cho lời gọi. Hình 2.10. Các ràng buộc không thỏa mãn sau khi loại bỏ phép toán equals 2.4.4. Sinh các ràng buộc xâu và kết quả thực hiện Trước khi các ràng buộc được tạo ra, các đỉnh mới được thêm vào đồ thị xâu. Đối với các đỉnh không phải là hằng xâu SiS một biến kiểu nguyên liI được thêm vào để đại diện cho độ dài xâu Si. Hình 3.4 chỉ ra rằng đỉnh mới của đồ thị xâu trong Hình 3.2 được nối với các đỉnh xâu tương ứng bằng các nét đứt. Hình 2.11. Các đỉnh mới đại diện cho độ dài xâu được bổ sung Các ràng buộc khác dựa trên các cạnh được chỉ ra tại bảng 2.1. 14 Bảng 2.1. Xây dựng các ràng buộc cho các phép toán trên xâu. 2.4.5. Giải ràng buộc sử dụng Otomat Các bộ giải ràng buộc là những công cụ nổi tiếng để giải quyết nhiều vấn đề trong thế giới thực như chứng minh định lý và lập lịch thời gian thực. Thực thi biểu trưng để tạo dữ liệu kiểm thử tự động đã được sử dụng trong các công trình CT[2], CT[3]. Nhiều nhà nghiên cứu đã giảm bớt những thiếu sót của các bộ giải ràng buộc có sẵn để cải thiện các ứng dụng trong thực thi biểu tượng nhằm tạo dữ liệu kiểm thử. Dù đã có nhiều cải tiến nhưng các bộ giải ràng buộc vẫn không xử lý hiệu quả với một số loại ràng buộc nhất định. Trong các chương trình máy tính, dữ liệu xâu xuất hiện thường xuyên, đặc biệt là trong phần chương trình hoặc phương thức. Ngôn ngữ Java cung cấp một thư viện lớn các kiểu dữ liệu chuỗi nhưng vẫn còn nhiều lỗi. Trong kiểm thử phần mềm, chúng tôi quan tâm đến việc xác định lỗi. Trong thực thi biểu tượng, các ràng buộc xâu cũng được xem xét trong hầu hết các trường hợp. Otomat hữu hạn đơn định (Deterministic Finite Automaton – DFA) được sử dụng để giải ràng buộc xâu dựa trên các thuật toán cụ thể CT[5]. 2.5. Kết luận chƣơng 2 Chương 2 của luận án đã trình bày các vấn đề liên quan đến thực thi biểu trưng và công cụ mở rộng với vai trò hiệu quả trong sinh tự động các ca kiểm thử. Nội dung chủ yếu liên quan đến thực thi biểu trưng bao gồm các kỹ thuật thực thi biểu trưng khác nhau; ưu, nhược điểm của các kỹ thuật này cùng những xử lý cần thiết để áp dụng thực thi biểu trưng trong quá trình kiểm thử phần mềm. Đồng thời, chương 2 còn nêu những khó khăn khi áp dụng thực thi biểu trưng và một vài giải pháp được nêu ra trong chương này. Các cách tiếp cận mô hình hóa ràng buộc sử dụng đồ thị xâu, xây dựng các ràng buộc trên đồ thị xâu, quy trình tiền xử lý phát hiện các ràng buộc không thỏa mãn cũng được đưa ra trong chương này. Các nội dung trình bày trong chương 2 là các kết quả nghiên cứu từ các công trình CT[1], CT[2], CT[3], CT[5]. CHƢƠNG 3. GIẢI RÀNG BUỘC XÂU Trong chương này, luận án trình bày một đề xuất cải tiến giải ràng buộc xâu trong thực thi biểu trưng dựa trên lý thuyết Otomat và áp dụng trên kiểu dữ liệu xâu kí tự. Kết quả đặt thực nghiệm, đánh giá về xử lý dữ liệu văn bản của mô hình cải tiến với một số mô hình đã có cũng được trình bày trong chương này. Nội dung chương này được thể hiện trong các kết quả công bố [CT4], [CT5], [CT6] của tác giả. Phép toán Java Heper-edge Ràng buộc mới Với mỗi ràng buộc cho đỉnh không là hằng xâu Si S li>0 Sa.charAt(n) charAt,Sa,n,c la≥n Sa.concat(Sb) concat, Sa , Sb, Sx lx=la+lb Sa.indexOf(Sb) indexOf, Sa, Sb,x (x=-1)˅(la≥lb+x) Sa.lastIndexOf(Sb) lastIndexOf, Sa, Sb,x (x=-1)˅(la≥lb+x) Sa.subString(n,k) subString,Sa,n,k,Sx la=n+lx Sa.contains(Sb) contains,Sa,Sb la≥lb 15 3.1. Giải ràng buộc xâu Nhiều ứng dụng phụ thuộc vào việc xử lý kiểu dữ liệu văn bản (text). Do việc sử dụng Internet đã trở nên phổ biến với sự gia tăng của các ứng dụng tương tác (mạng xã hội, chat, quản lý các thông tin nhạy cảm, quan trọng, các thông tin cá nhân) đã khiến cho vấn đề này trở nên quan trọng hơn. Dữ liệu đầu vào của các chương trình được sử dụng trong các câu lệnh truy vấn SQL và được lưu trữ trên các hệ quản trị cơ sở dữ liệu. Điều này cho phép người dùng truy cập trực tiếp vào cơ sở dữ liệu. Lý do là các dữ liệu đầu vào là mở và công khai và nó cũng là mở cho các đối tượng khác. Một số đối tượng có ý định xấu nên việc “làm sạch” đầu vào dưới dạng văn bản là yêu cầu xuất hiện hầu hết trong các dịch vụ web. Phương pháp hiện tại để thực thi biểu trưng mã xâu được chia thành hai nhóm: nhóm thứ nhất dựa trên Otomat [5, 53] và nhóm thứ hai dựa trên Bitvector [7]. 3.2. Bitvector và bộ thỏa mãn SMT (satisfiability modulo theories) 3.2.1. Lý thuyết thỏa mãn SMT Nghiên cứu của luận án này dùng bộ giải ràng buộc SMT Z3 [70] được xây dựng bởi Microsoft. Nghiên cứu này cũng đã xem xét sử dụng CVC[25] nhưng nhận ra rằng nó chậm hơn Z3 bởi vì luận án này sử dụng chuẩn SMT-lib2 cho ràng buộc bitvector. Luận án cũng đã xem xét sử dụng các ký hiệu thay thế cho cách đánh địa chỉ theo byte thay cho bit. Ví dụ a[0:7]=01100010 sẽ được thay là a[0]=‟b‟. Việc giải quyết các ràng buộc bằng bitvector nằm ngoài phạm vi của nghiên cứu này. 3.2.2. Giải ràng buộc xâu dựa trên phương pháp BitVector Xem xét ví dụ với cạnh (contains,Sa,Sb) tương ứng với ràng buộc Sa.contains(Sb), ta giải sử ước lượng hiện tại cho độ dài của Sa và Sb tương ứng là 5,3 kết quả ràng buộc cho cạnh này là: (Sa[0]=Sb[0])˄(Sa[1]=Sb[1]) ˄ (Sa[2]=Sb[2]) ∨((Sa[1]=Sb[0]) ˄ (Sa[2]=Sb[1]) ˄ (Sa[3]=Sb[2]) ∨((Sa[2]=Sb[0])˄(Sa[3]=Sb[1])˄(Sa[4]=Sb[2]) Nếu như nền tảng của bộ giải ràng buộc hỗ trợ kiểu mảng nó có thể đơn giản hóa thành (Sa[0:2]=Sb)∨(Sa[1:3]=Sb) ∨(Sa[2:4]=Sb). Quá trình biên dịch các cạnh của đồ thị xâu sang ràng buộc BitVector được chỉ ra tại cột thứ 2 của bảng 3.1 Bảng 3.1. Xây dựng ràng buộc tương ứng với các phép toán trên xâu. Cạnh Công thức Otomat Ràng buộc bitvector (charAt,sa,n,x) Ma= Ma [n] {x} [*] Sa[n]=x (concat,sa,sb,sx) Ma= Ma substring(Mx,0,la) Mb=Mb subString(Mx,lb, ) Mx=Mx (Ma Mb) (sa=sx[la:0]) (sb=sx[lx:la]) (indexOf, sa,sb,x) Ma= Ma ([x] Mb) Mb [*] Mb=Mb substrings(Ma,x,x+lb) (sa[x+lb:x]=sb) sa[i+lb:i] sb, i,0 i<x) (lastIndexOf, sa,sb,x) Ma= Ma [*] Mb ([x+lb] ] ([*] Mb [*])) Mb= Mb substrings(Ma,x,x+lb) (sa[x+lb:x]=sb) (sa[i+lb:i] s b, , i x<i la-lb) substring(sa,n,sx) Ma= Ma [n] Mx Mx= Mx substring(Ma,n,∞) sa[n+lx:n]=sx substring(sa,n,k,sx) Ma= Ma [n] Mx [*] Mx= Mx substring(Ma,n,k) Sa[n+lx:n]=sx 16 trim(sa,sx) Ma= Ma [„˽‟,*] Mx [„˽‟,*] Mx= Mx trim(Ma) (sx[0] ˽) sx[lx-1] „˽‟) (sa[j]= „˽‟ (sa[i+lx:i]=sx) (sa[k]= „˽‟), i,j,k |(0 i la-lx) (0 j i) (i+lx k<la)) (contains, sa,sb) Ma= Ma [*] Mb [*] Mb= Mb substring(Ma,0,∞) 0 i<la-lb sa[i+lb:i]=sb (endsWith, sa,sb) Ma= Ma [*] Mb Mb=suffises(Ma) sa[la:la-lb]=sb (startsWith, sa,sb) Ma:= Ma Mb [*] Mb:=prefixes(Ma) sa[lb:0]=sb 3.3. Giải ràng buộc xâu dựa trên phƣơng pháp sử dụng OTOMAT Trong thuật toán này, khi các cạnh trong quá trình xử lý các Otomat được sửa đổi lại để phản ánh tác động của ràng buộc, bản chất của sự sửa đổi phụ thuộc vào ràng buộc. Ví dụ, cạnh (contains, sa,sb) tương ứng với ràng buộc sa.contains(sb). 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13 atomatonSolver(PathCondition pc;StringGraph StringGraph sg=(I S,E, Ʊ)) for( các đỉnh si S) Automaton Mi=[li]; W=E while W≠∅ W=W\e for(si kết nối với e) Cập nhật lại Mi dựa vào ràng buộc e; if(Mi=∅) pc=pc freshConstranints(pc:sg); return(false,pc,sg); else if(Mi đã thay đổi) W=W tất cả các cạnh kết nối với si; return checkNegativeEdges(pc;sg;(M1,M2..)); Hình 3.1. Giải ràng buộc xâu dựa trên Otomat Đối với các ràng buộc phủ định như !equals, !constain, !startsWith và !endsWith giả sử rằng hai M1, M2 là hai Otomat tương ứng với hai biến xâu s1,s2 mà ta phải giải ràng buộc s1.!equals(s2) khi đó sẽ có 3 trường hợp: TH1: Cả hai Otomat chỉ đoán nhận duy nhất một từ và khi đó ràng buộc này sẽ thỏa mãn khi hai từ này là không bằng nhau. TH2: Chỉ có một Otomat đoán nhận duy nhất một từ và khi đó ta chỉ việc gỡ bỏ từ đó ra khỏi Otomat còn lại. Trong trường hợp này, ràng buộc cũng sẽ được thỏa mãn. TH3: Trong tất cả các trường hợp khác, ràng buộc được thỏa mãn và không Otomat nào phải thay đổi. Phần chính của thuật toán trong Hình 3.6 mô tả hình thức các bước thực hiện cho việc tìm lời giải cho ràng buộc phủ định. 17 CheckNegativeEdges(pathcondition pc, StringGraph sg, (M1,M2..)) 1: i=1; M‟1=M1; M‟2=M2; M‟k=Mk; 2: while(1≤i<k) 3: if(Mi=∅) 4: Mi=M‟I; 5: i=i-1; 6: else 7: vi=a Mi; 8: Mi=Mi\{a}; 9: for( với mỗi ei E và last(e)=si) 10: if(e là vi phạm với vi) 11: Break;\\ quay lại dòng 2 12: i=i++; 13 return; Hình 3.2. Phương thức giải ràng buộc phủ định Tạo ra sự cập nhật cho ràng buộc: Nếu những ràng buộc xâu được kết luận là không thỏa mãn, khi đó ràng buộc nguyên mới sẽ được thêm vào ràng buộc đường đi. 3.4. Đề xuất giải ràng buộc xâu trong thực thi biểu trƣng Các bước chính thực hiện thực thi biểu trưng bao gồm: Bước 1: Điều kiện ràng buộc đường dẫn sẽ được chuyển đổi sang một định dạng trung gian. Bước 2: Giải hoặc đơn giản hóa định dạng trung gian. Bước 3: Thay thế biến biểu trưng kiểu nguyên bằng các giá trị cụ thể phỏng đoán. Bước 4: Chuyển đổi định dạng trung gian