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

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 biểu 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 [40]. Bảng 1.3 dƣới minh họa việc mã nguồn Java đƣợc chuyển thành dạng mã Jimple. Bảng 1.3. 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: 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; 36 x = 0; break; } x = x + c; } // 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 biểu 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 tảng 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 phần mã hỗ trợ thực thi biểu trƣng thì công cụ Soot [40] đƣợc sử dụng để chuyển chúng về dạng Java bytcode chuẩn. Lưu trữ giá trị biểu trưng Với các hệ thống kiểm thử mà cài đặt kỹ thuật thực thi biểu trƣng ở trên thì cần có các cấu trúc dữ liệu để lƣu trữ các giá trị biểu 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 biểu 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ị biểu 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ị biểu 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ị biểu 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ị biểu trƣng. R(o) biểu thị cho giá trị biểu trƣng của đối tƣợng o. R là một ánh xạ giữa đối tƣợng và giá trị biểu 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ƣ key mà các giá trị biểu 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 biểu 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 [41] có thể xác định các câu lệnh và các 37 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 biểu trƣng. Các giá trị biểu 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ị biểu trƣng. Khi một giá trị biểu 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ị biểu trƣng ánh xạ tới tham chiếu đƣợc trả về nếu tham chiếu đƣợc tìm thấy. 1.5.5. Thực thi biểu trưng 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ị biểu trƣng kết hợp với chúng thì các giá trị biểu 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ị biểu trƣng của các đối số đƣợc đẩy vào một ngăn xếp. Và các giá trị của chúng đƣợc đọc từ stack tới biến biểu 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 biểu 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 biểu trƣng với các giá trị biểu 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 biểu 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 biểu 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 biểu 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 qua dự án OpenJDK [42] do đó việc sửa đổi các thƣ viện chuẩn của Java để hỗ trợ thực thi biểu trƣng là điều có thể thực hiện đƣợc. Một ví dụ đơn giản về thực thi biểu trƣng trên lời gọi phƣơng thức 38 1:struct point {int x,y,z;}; 2: 3:int main(){ 4:struct point p={0,0,0}; 5:int j, k;//symbolic 6: 7: f(&p, k);//skip 8: if(j>0) 9: if (p.y) 10: bug(); 11: else 12: allgood(); 13: return 0; 14: } (a) (b) 15: void f(struct point *p, int k){ 16: if(k%2) 17: p->z++; 18: 19: if(k>0) 20: p->x++; 21: else 22: p->y++; 23 } (c) Hình 1.11. Thực thi biểu trưng trên lời gọi phương thức Hình 1.11(a) cho thấy điểm vào của chƣơng trình (hàm main()), trong khi Hình 1.11 (c) hiển thị mã không thú vị mà ta muốn bỏ qua ( chức năng f). Khi bắt đầu thực hiện băm nhỏ bằng cách thực hiện chính biểu trƣng. Khi một trạng thái đạt đến lệnh gọi hàm f ở dòng 7, chúng ta tạo trạng thái chụp nhanh bằng cách nhân bản trạng thái hiện tại và bỏ qua lệnh gọi hàm. Trạng thái chụp nhanh đƣợc hiển thị bằng đồ họa trong Hình 1.11 (b), trong đó mỗi hình bầu dục màu xám biểu thị trạng thái thực thi biểu trƣng. Với một ảnh chụp nhanh đƣợc tạo, chúng ta tiếp tục thực hiện ở trạng thái hiện tại. Nhƣng từ thời điểm này, chúng ta phải xem xét rằng một số hƣớng dẫn tải có thể phụ thuộc vào các hiệu ứng phụ của hàm bị bỏ qua f, nghĩa là các vị trí bộ nhớ mà f có thể cập nhật. Trong ví dụ này, các hiệu ứng phụ của f là các vị trí bộ nhớ đƣợc trỏ bởi p.z, p.x và p.y, đƣợc cập nhật ở các dòng 17, 20 và 22 tƣơng ứng. Bằng tính toán các khía cạnh của f bằng cách sử dụng phân tích con trỏ 39 tĩnh bảo thủ [43 - 46] trƣớc khi bắt đầu thăm dò biểu trƣng. Thực hiện bỏ qua các hƣớng dẫn đọc từ phía bên của các hàm bị bỏ qua dƣới dạng tải phụ thuộc. Trên một số đƣờng dẫn, thực thi biểu trƣng không gặp phải nhƣ vậy. Ví dụ: đƣờng dẫn đi theo phía bên kia của nhánh ở dòng 8 không truy cập p.x, p.y hay p.z. Vì vậy không cần thực hiện thêm hành động nào trên các đƣờng dẫn đó và việc thăm dò có thể kết thúc chính xác mà không cần thông qua mã của f. Trên thực tế, trong các chƣơng trình thực thƣờng có đƣờng dẫn mà không phụ thuộc vào các hàm bị bỏ qua, và trong trƣờng hợp này thực thi biểu trƣng ngay lập tức hƣởng lợi từ cách tiếp cận của nghiên cứu này. Đƣờng dẫn không có liên quan đƣợc bỏ qua một cách an toàn, do đó làm giảm sự bùng nổ đƣờng dẫn đƣờng. Tuy nhiên, trên các đƣờng dẫn khác thực thi biểu trƣng gặp phải tải phụ thuộc. Điều này xảy ra với ví dụ đã cho trên đƣờng dẫn khám phá phía sau của nhánh ở dòng 8, khi nó tải giá trị của p.y ở dòng 9. Tại thời điểm này, trạng thái hiện tại cần đƣợc treo cho đến khi các đƣờng dẫn có liên quan trong hàm f khám phá, và trở thành một trạng thái phụ thuộc. Để khôi phục một đƣờng dẫn, chúng ta tạo một trạng thái phục hồi mới kế thừa trạng thái ảnh chụp đƣợc tạo trƣớc khi bỏ qua hàm f ở dòng 7 và bắt đầu thực hiện chức năng một cách biểu trƣng. Trong khi thực thi biểu trƣng ở trạng thái phục hồi, nếu thực thi rẽ nhánh, thì cùng một ngã ba đƣợc thực hiện ở trạng thái phụ thuộc. Hơn nữa, khi ta chạy trạng thái khôi phục, mọi lƣu trữ đến vị trí bộ nhớ đƣợc đọc bởi tải phụ thuộc cũng đƣợc thực hiện ở trạng thái phụ thuộc. Ví dụ: nếu việc thực thi biểu trƣng của f cắt ngang qua nhánh khác tại các dòng 21 - 22, thì giá trị của p.y (vị trí bộ nhớ đƣợc trỏ bởi p-> y) cũng đƣợc đặt thành 1 ở trạng thái phụ thuộc. Nếu trạng thái phục hồi trở lại thành công, trạng thái phụ thuộc đƣợc nối lại thành công. Nếu xảy ra lỗi trong khi thực hiện trạng thái khôi phục (ví dụ: truy cập bộ nhớ không hợp lệ hoặc phân chia theo lỗi 0, có thể xảy ra nếu p-> z đƣợc đặt trong dòng 17 đến 4 / p-> y), trạng thái phụ thuộc tƣơng ứng là chấm dứt. Khi thực thi trạng thái khôi phục, không phải tất cả các đƣờng dẫn có thể tƣơng thích với thực thi mà trạng thái phụ thuộc đạt đƣợc. Ví dụ: nếu dòng 8 đƣợc thay đổi từ if (j> 0) thành if (k> 0), thì trạng thái phụ thuộc sẽ có k> 0 trong PC của nó, khiến trạng thái phụ thuộc không tƣơng thích với đƣờng dẫn trong f trong đó k ≤ 0. Một cách để loại bỏ các đƣờng dẫn không tƣơng thích nhƣ vậy là thực thi tất cả các đƣờng dẫn có thể qua hàm f trong quá trình khôi phục và sau đó lọc các đƣờng dẫn 40 không tƣơng thích với trạng thái phụ thuộc. Tuy nhiên, điều này có khả năng sẽ dẫn đến việc bùng nổ đƣờng dẫn thành một con số lớn. 1.6.6. Ràng buộc xâu và vai trò của giải ràng buộc xâu Mấu chốt của thực thi biểu trƣng đó là khả năng giải ràng buộc và xâu dữ liệu là một kiểu dữ liệu cơ bản nó có trong tất cả các ngôn ngữ lập trình hiện đại và việc sử dụng các phép toán trên xâu là thƣờng xuyên đƣợc thực hiện. Trong các lĩnh vực khác nhau nhƣ phân tích phần mềm, kiểm chứng mô hình, cơ sở dữ liệu, bảo mật web, tin sinh học [47 - 52]. Vì lý do trên việc giải các ràng buộc phức tạp trên xâu là cần hiết và có rất nhiều ứng dụng. Các quan hệ đƣợc định nghĩa trên biến xâu kí tự bao gồm: Độ dài xâu, so sánh xâu, các phép nối, kiểm tra xâu con, cắt xâu, so sánh biểu thức chính quy vv.. Thuật ngữ giải ràng buộc xâu (String Constraint Solving)trong luận án đề cập đến việc mô hình hóa, và giải quyết các biểu thức kết hợp liên quan đến ràng buộc xâu, ta có thể xem nhƣ giải ràng buộc xâu nhƣ là phần giao giữa giải ràng buộc và tổ hợp các từ, trong đó ngƣời dùng sẽ đƣa ra một vấn đề với các biến xâu và một bộ giải ràng buộc xâu sẽ tìm ra một giải pháp phù hợp cho vấn đề đó. Từ những năm 2010 việc giải ràng buộc xâu đã có một số các nghiên cứu quan tâm có kết quả nhất định [51, 52] do nó có vai trò chủ đạo trong các lĩnh vực sinh dữ liệu kiểm thử, kiểm chứng mô hình, và bảo mật web. Trong những năm qua có nhiều hƣớng tiếp cận khác nhau đã đƣợc đƣa ra, nhƣng có ba loại chính: Tiếp cận dựa trên lý thuyết về Otomat: phƣơng pháp này sử dụng một Otomat hữu hạn để biểu diễn giá trị của một biến xâu, nó đƣợc dùng để lƣu trữ, xử lý các phép toán trên xâu. Tiếp cận dựa trên từ: Phƣơng pháp này sử dụng hệ thống của so sánh từ với nhau, chúng sử dụng chủ yếu lý thuyết thỏa mãn (SMT) [53] để giải các ràng buộc xâu. Tiếp cận dựa trên phân tách xâu: Nguyên lý là thực hiện phân tách xâu thành các phần tử liền kề tƣơng đƣơng là các kí tự của xâu. Xâu có thể phân rã thành các số nguyên hoặc bitvector Bảng chữ cái hữu hạn là một tập hữu hạn Σ ={a1,a2 . . . , an} với n>1 các kí hiệu cũng đƣợc gọi là kí tự. Một xâu w hay một tự là một dãy hữu hãn các kí tự thuộc 41 bảng chữ cái Σ, kí hiệu |w| biểu diễn cho độ dại của xâu w( trong luận án này không đề cập đến xâu có độ dài vô hạn). Một xâu rỗng đƣợc biểu diễn bởi ký tự ɛ, gọi tập hữu hạn Σ*là tập tất cả các xâu của bảng chữ cái Σ đƣợc định nghĩa đệ quy nhƣ sau: Xâu rỗng: ɛ ∈ Σ* Nếu kí tự a∈ Σ và w∈ Σ* thì thì wa∈ Σ* Ngoài ra không có gì thuộc Σ* Phép nối của hai xâu v,w∈ Σ* đƣợc biểu diễn bởi v.w, trong luận án này phép lặp n lần xâu w đƣợc biểu diễn bởi wn nó có nghĩa là lặp n lần phép nối xâu w, và w0= ɛ và wn=w. wn-1, n>0. Tƣơng tự ta định nghĩa phép nối của hai tập xâu: cho hai tập V,W⊆ Σ*, ta biểu diễn V.W={v.w | v∈ V ,w ∈ W }, phép lặp trên tập W cũng tƣơng tự đƣợc định nghĩa nhƣ sau: W0={ ɛ} và Wn=W.Wn-1 trong đó n>0. Một tập các xâu L ⊆ Σ đƣợc gọi là một ngôn ngữ nếu nó đƣợc đoán nhận bởi một otomat hữu hạn M và đƣợc ký hiệu là L(M). Một biến xâu chỉ có thể nhận các giá trị thuộc Σ* hoặc tƣơng đƣơng với miền giá trị của một ngôn ngữ của Σ*, ta có thể phân loại biến xâu thành ba cấp độ nhƣ sau: Biến xâu không có giới hạn về độ dài: chúng có thể nhận bất kỳ giá trị nào thuộc Σ*. Biến xâu có giới hạn độ dài: giới hạn đƣợc cho bởi một số nguyên λ, λ > 0 và chúng chỉ có thể nhận các giá trị trong khoảng i ={w ∈ Σ ∗ | |w| ≤ λ}. Biến xâu đƣợc cố định độ dài: cho trƣớc một số nguyên λ, λ > 0, chúng chỉ có thể nhận các giá trị trong Σλ = {w ∈ Σ ∗ | |w| = λ}. Ràng buộc xâu: Ràng buộc xâu là một mối quan hệ thông qua ít nhất một biến xâu. VD: phép nối xâu là một bộ ba ràng buộc xâu. Để đơn giản thay vì kí hiệu (x,y,z) ∈. Luận án này sử dụng hàm kí hiệu z=x.y. Trong phần này chúng ta chỉ xem xét đến ràng buộc xâu bao gồm chỉ có xâu hoặc số nguyên dùng để biểu diễn cho độ dài xâu hoặc phép các phép nối lặp, từ các ràng buộc trong Bảng 1.4, các ràng buộc khác có thể đƣợc suy ra. Bảng 1.4. Mô tả ràng buộc xâu Ràng buộc xâu Mô tả x = y, x ≠ y So sánh bằng, so sánh khác x y So sánh thứ tự logic của hai xâu n=|x| So sánh độ dài xâu với một số nguyên n 42 Ràng buộc xâu Mô tả z=x.y, y=x n Phép nối xâu, phép lặp của 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ự đầ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 43 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. 44 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], CT[5] của nghiên cứu sinh. 2.1. Đặt vấn đề 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. Trƣớc hết, lƣu ý rằng thực thi biểu trƣng đã ngầm lọc ra tất cả các đƣờng thực thi không phụ thuộc vào các biến biểu trƣng đầu vào và những đƣờng dẫn không khả thi trong quá trình giải các ràng buộc. Mặc dù nhƣ vậy, sự bùng nổ đƣờng dẫn vẫn là một trong những thách thức lớn nhất đối với thực thi biểu trƣng. Hiện nay có hai cách tiếp cận chính để giải quyết vấn đề này là ƣu tiên tìm kiếm kinh nghiệm và sử dụng kỹ thuật phân tích tính đúng đắn của chƣơng trình trong quá trình phân tích đƣợc trình bày dƣới đây. Tìm kiếm kinh nghiệm Cơ chế quan đƣợc sử dụng trong các công cụ thực thi biểu trƣng để ƣu tiên đƣờng dẫn khai phá là sử dụng tìm kiếm kinh nghiệm. Hầu hết Heuristic đặt trọng tâm vào vấn đề bao phủ dòng lệnh và bao phủ rẽ nhánh. Nhƣng chúng cũng có thể đƣợc sử dụng để tối ƣu hóa các tiêu chí mong muốn khác. Một cách tiếp cận đặc biệt hiệu quả là sử dụng đồ thị luồng điều khiển. Để điều hƣớng đƣờng gần nhất từ những đƣờng dẫn đã khám phá [17, 55], một cách tƣơng tự trong EXE [17] là ƣu tiên những câu lệnh đã thực thi mà có số lần chạy là ít nhất. Một 45 ví dụ khác với tìm kiếm Heuristic dựa trên khám phá ngẫu nhiên cũng đã đƣợc chứng minh tính hiệu quả [17, 55]. Ý tƣởng chính của phƣơng pháp này là khi bắt đầu chƣơng trình với mỗi câu lệnh rẽ nhánh của thực thi biểu trƣng trong các nhánh khả thi nó sẽ chọn ngẫu nhiên một nhánh để khám phá. Một tiếp cận thành công khác là xen vào kiểm thử ngẫu nhiên và khám phá biểu trƣng. Phƣơng pháp này kết hợp khả năng của kiểm thử ngẫu nhiên để nhanh chóng đến những trạng thái thực thi sâu của chƣơng trình. Với sức mạnh của thực thi biểu trƣng việc kết hợp đƣợc khai phá triệt để những trạng thái trong một vùng lân cận. Gần đây hơn nữa thực thi biểu trƣng còn đƣợc kết hợp với kỹ thuật tìm kiếm tiến hóa. Trong đó hàm mục tiêu đƣợc sử dụng để định hƣớng không gian đầu vào của của các biến [30, 56 - 58]. Ví dụ với công cụ Austin [58] sử dụng tìm kiếm tiến hóa trong tìm kiếm đƣờng thực thi. Trong đó nó sử dụng một hàm mục tiêu phát triển tìm kiếm của không gian dữ liệu kiểm thử đầu vào. Với thực thi biểu trƣng động khai thác tốt đƣợc cả hai lĩnh vực trên, hiệu quả của kiểm thử phần mềm phụ thuộc vào chất lƣợng của hàm mục tiêu. Một vài tiếp cận hứa hẹn khác [30, 56, 57] khai thác thông tin trạng thái thực thi của giá trị cụ thể và thực thi biểu trƣng từ thực thi biểu trƣng động và phân tích tĩnh để cải tiến hàm mục tiêu cho kết quả sinh dữ liệu kiểm thử tốt hơn. Kiểm thử đột biến với các bộ test đầy đủ đƣợc đánh giá bằng cách kiểm tra khả năng xác định khác nhau của đột biến trong chƣơng trình cũng đã kết hợp thành công với thực thi biểu trƣng động [59]. Nhìn chung các phƣơng pháp mới trong việc kết hợp thực thi biểu trƣng và kỹ thuật tìm kiếm kinh nghiệm đã cho những kết quả hứa hẹn. Các nhà khoa học tin rằng những tiến bộ hơn nữa trong lĩnh vực này có thể đóng vai trò quan trọng trong việc giải quyết sự bùng nổ đƣờng dẫn trong thực thi biểu trƣng. Kỹ thuật phân tích tính đúng đắn của chương trình Một cách tiếp cận quan trọng khác cho vấn đề bùng nổ đƣờng dẫn từ phân tích chƣơng trình và kiểm chứng phần mềm nhằm giảm độ phức tạp của đƣờng dẫn thực thi chƣơng trình đó là sử dụng thông qua phân tích tính đúng đắn của chƣơng trình. Cách tiếp cận đơn giản đƣợc sử dụng để giảm số lƣợng đƣờng thực thi chƣơng trình là gộp lại theo hƣớng tĩnh sử dụng biểu diễn bởi cấu trúc lựa chọn, sau đó đƣợc truyền trực tiếp cho bộ giải [35]. Tiếp cận này có thể có hiệu quả trong nhiều trƣờng hợp 46 nhƣng nó không phù hợp khi truyền độ phức tạp cho bộ giải. Nội dung này sẽ đƣợc trình bày ở phần sau. Các kỹ thuật kết hợp cải tiến thực thi biểu trƣng bằng cách sử dụng bộ nhớ đệm và sử dụng lại phân tích của những hàm ở mức thấp trong những tính toán tiếp theo. Ý tƣởng chính của kỹ thuật này đƣợc thể hiện trong các tài liệu [58, 59] là tính toán, tóm tắt hàm đối với mỗi hàm kiểm thử đƣợc mô tả về điều kiện trƣớc và giá trị đầu ra của hàm và sử dụng lại sự tóm tắt này đối với những hàm ở mức cao. Sinh các ca kiểm thử lƣời [62]. Nó là một cách tiếp cận liên quan để tránh sự lặp lại trong khai phá đƣờng dẫn bằng cách tự động cắt tỉa các đƣờng dẫn dƣ thừa trong quá trình khám phá đƣờng dẫn. Kỹ thuật này dựa trên ý tƣởng nếu các đƣờng dẫn đạt đến cùng một điểm và cùng có ràng buộc tƣơng tự với đƣờng dẫn trƣớc đó thì sẽ đƣợc thực thi tƣơng tự đồng thời đƣờng dẫn đó sẽ bị loại bỏ. 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.. Một ví dụ khác là mô hình hóa bộ nhớ với con trỏ. Trong một phạm vị cần giải quyết, DART chỉ đƣợc thực hiện với các giá trị cụ thể, hoặc hệ thống CUTE và CREST chỉ hỗ trợ và thực hiện giải tốt với ràng buộc kiểu đẳng thức và bất đẳng thức trên kiểu dữ liệu con trỏ. Trong các ngôn ngữ khác nhau giống nhƣ EXE [55] hoặc gần đây hơn là KLEE và SAGE [63] thực hiện mô hình hóa con trỏ sử dụng khái niệm liên quan đến mảng, lựa chọn và cập nhật các thành phần bởi lời giải giống nhƣ với STP [35] và Z3 [64]. Việc cân bằng giữa độ chính xác và khả năng mở rộng có thể xác định đƣợc những phƣơng diện khi phân tích mã nguồn và sự thực hiện chính xác giữa các bộ giải ràng buộc khác nhau. Ngoài ra chú ý rằng thực thi biểu trƣng động cho phép điều chỉnh cả khả năng mở rộng và sự chính xác bởi các tùy biến đối với các giá trị cụ thể trong biểu thức biểu trƣng. 47 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 Sinh dữ liệu kiểm thử là một trong các giai đoạn quan trọng và quyết định trong 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. Cơ chế phổ biến nhất và hiệu quả nhất đƣợc sử dụng bởi các nhà thực thi biểu trƣng là tìm kiếm heuristic, với mục tiêu là hƣớng sự bùng nổ chƣơng trình đến những con đƣờng hứa hẹn nhất trong chƣơng trình. Các phƣơng pháp phỏng đoán phổ biến bao gồm tìm kiếm đƣờng dẫn theo ngẫu nhiên [30], tìm kiếm tiến hóa[36] và tìm kiếm tối ƣu hóa phạm vi [55, 65]. Thật không may, tìm kiếm heuristic chỉ làm giảm bớt một phần sự bùng nổ đƣờng dẫn và việc thực thi biểu trƣng vẫn có thể bị mắc kẹt trong các phần không liên quan của mã. Một kỹ thuật hiệu quả khác là cố gắng cắt tỉa các đƣờng dẫn chƣơng trình tƣơng đƣơng [66, 67]. Chẳng hạn, nếu một đƣờng dẫn đến một điểm chƣơng trình với một tập các ràng buộc tƣơng đƣơng với các đƣờng dẫn trƣớc đó đạt đến điểm đó, thì đƣờng dẫn thứ hai (và tất cả các đƣờng dẫn mà nó sẽ sinh ra) có thể bị chấm dứt. Kỹ thuật này tƣơng tự về mặt tinh thần với cách tiếp cận của luận án, nhƣng trực giao, vì nó không làm gì để ngăn chặn việc khám phá các d