ĐẠi học quốc gia hà NỘi trưỜng đẠi học công nghệ Trần Bình Dương sinh ca kiểm thử tham số HÓa cho chưƠng trình java khóa luận tốt nghiệP ĐẠi học hệ chính quy ngành: Công Nghệ Thông Tin

2.3. Sinh dữ liệu kiểm thử cho PUT

1: T = newSET();// khởi tạo cây thực thi tượng trưng

2: S = chiến lược tìm kiếm;

3: while(T chưa được thăm hết){

//chọn được đỉnh n chưa được thăm bằng chiến lược S

4: m = n = S(T);

5: pc = true;

6: while (m ≠ T.root){

7: pc = pc m.constraint;

8: m = m.parent;

9: }

inputs = solve(pc);

11: execute(inputs);//inputs đưa tới Test Executor để thực thi

12: expand(n);//chọn đỉnh n để mở rộng tiếp

13: if(có lỗi thực thi)

14: reportError();

15: marked(n);// đánh dấu đỉnh n đã được thăm

}

Hình 10: Thuật toán sinh dữ liễu kiểm thử

Với Pex[30] thì các ràng buộc đường đi thu gom được không phải là dạng công thức logic đơn thuần như ta đã trình bày ở trên mà là dạng công thức logic bậc một (first-order logic fomulas)[2]. Chính nhờ việc xây dựng ràng buộc dạng này mà Pex có thể sử dụng một SMT solver (Z3) để xử lý các ràng buộc đó. Pex sinh dữ liệu kiểm thử cho PUT bằng việc xây dựng và quản lý các cây thực thi cục bộ (intraprocedural execution trees).

Ví dụ 2.5:


void TestAbs(int p,int q){

int m = abs(p);

int n = abs(q);

if(m > n && p > 0)

assertfalse;

}

Để hiểu rõ hơn về ràng buộc mà Pex xây dựng ta xét ví dụ 2.5 ở trên. Hàm TestAbs gọi một hàm khác là hàm abs. Các cây thực thi cục bộ tương ứng với mỗi hàm được minh họa trong Hình 11. Các cạnh của cây được gán nhãn bởi các ràng buộc và các đỉnh (node) của cây đại diện cho sự thực thi của một câu lệnh trong chương trình sao cho đường đi từ đỉnh gốc (root) của cây tới đỉnh lá (leaf) tương ứng với một đường đi thực thi cục bộ (intraprocedural path). Hình 11(a) là một phần của cây thực thi cục bộ tương ứng với hàm abs minh họa cho việc gọi hàm abs với giá trị x=1. Với cây thực thi cục bộ này ta làm quen với khái niệm là đỉnh treo (dangling node). Đỉnh treo là đỉnh đại diện cho đường đi chưa được thực thi. Đỉnh treo giống như đỉnh mới được tạo ra mà được đánh dấu là chưa được thăm như ta đã trình bày trong phần trước. Với kỹ thuật thực thi tượng trưng động[13, 19], việc thám hiểm có thể đạt tới đích (đỉnh treo) cho trước bằng thám hiểm lười (lazy exploration) và cố gắng tránh những đường đi mà không đạt tới đích bằng thám hiểm tin cậy (relevant exploration). Giả sử rằng ta gọi hàm TestAbs với p=1 và q=1. Sự thực thi này sẽ đi theo nhánh true của câu lệnh if đầu tiên trong hàm abs (đỉnh 3) cũng như nhánh false của câu lệnh if trong TestAbs (đỉnh 10). Hình 11(a) và (b) biểu thị cho cây thực thi cục bộ của hàm abs và TestAbs trong trường hợp này. Ta muốn sinh đầu vào cho hàm TestAbs để có thể thực thi câu lệnh xác nhận (đỉnh 11). Kỹ thuật này có thể tìm ra đầu vào để việc thực thi đạt tới đích (đỉnh 11) mà không cần phải thám hiểm các đường đi chưa được thám hiểm trong hàm mức thấp hơn (hàm abs).

Hình 11: Các cây thực thi cục bộ tương ứng với hàm abs và TestAbs

Ràng buộc cục bộ (local path constraint) của một đỉnh n trong cây thực thi cục bộ T_f của hàm f được định nghĩa bằng ràng buộc đường đi của đường đi w từ đỉnh vào (entry node) của hàm f tới câu lệnh đại diện bởi n. Ràng buộc đường đi của đỉnh n (localpc(n)) biểu thị bởi các ký hiệu đầu vào của ƒ

localpc(n):= lpc_n D_g()

với mỗi g() xuất hiện trong lpc_n

Trong đó lpc_n là biểu thức kết hợp của ràng buộc trên các cạnh của đường đi w từ gốc của cây thực thi cục bộ tới đỉnh n và D_g() đại diện cho kết quả (function sumary) của hàm g được gọi bởi ƒ với đầu vào mà xuất hiện trong lpc_n.

Khi hàm ƒ gọi hàm g trong thực thi tượng trưng thì giá trị trả về của lời gọi tới hàm g là một đầu vào tượng trưng của ƒ. Giá trị trả về của lời gọi tới hàm g được biểu thị bởi g() với là các đối số mà giá trị biểu thị bởi các ký hiệu đầu vào của ƒ. Nếu giá trị trả về được sử dụng trong câu lệnh rẽ nhánh của f thì g() xuất hiện trong ràng buộc đường đi. Ký hiệu hàm g sẽ được hiểu như ký hiệu hàm chưa định nghĩa (uninterpreted function)[2] bởi bộ xử lý ràng buộc. Hàm chưa định nghĩa này được thông dịch bởi một dạng định đề (axiom) x. g(x) = E[x], trong đó E[x] là một biểu thức liên quan tới biến x. Như ví dụ ở trên thì hàm abs có thể được định nghĩa như sau:

x. abs(x) = ITE(x > 0, x, ITE(x = 0, 100,−x)), (ITE biểu thị cho if-then-else).

Ta sử dụng definition-predicate D_g cho mỗi ký hiệu hàm để đại diện cho giá trị trả về của lời gọi hàm. Ta định nghĩa D_g bằng định đề (axiom) δ_g như sau:

δ_g= .. D_g() V localpc(l) Λ ret(l)

leaf l in T_g

trong đó ret(l)= G_l nếu l là đỉnh treo và ret(l)=Ret_g(l) trong trường hợp khác. Ret_g(l) đại diện cho giá trị trả về của g, đó là một biểu thức biểu thị bởi , trên đường đi cục bộ đã được thám hiểm hết đại diện bởi đỉnh treo . Với mỗi đỉnh treo d thì G_d là một biến logic duy nhất đại diện cho d. Quay lại ví dụ trên, TestAbs thực thi với p=1,q=1 thì ràng buộc đường đi cục bộ của đỉnh n được gán nhãn 11 sẽ như sau:

localpc(n):=abs(p) > abc(q) Λ p > 0 Λ D_abs(p) Λ D_abs(q)

Với đầu vào trên thì chỉ đường đi với x > 0 mới được thám hiểm trong abs, có một đỉnh treo d (đỉnh 2) đại diện cho nhánh của câu lệnh điệu kiện mà chưa được thám hiểm. D_abs sau đó được định nghĩa bởi định đề δ_abs :

δ_abs= D_abs(x)  ITE((x > 0, abs(x) = x, G_d)

Nếu tất cả các đường đi của abs đều được thám hiểm (Hình 11(b)):

δ_abs= D_abs(x)  (x ≤ 0 Λ x = 0 Λ abs(x) = 100)

hay δ_abs = ITE(x ≤ 0, ITE(x = 0, abs(x) = 100, abs(x) = −x),abs(x) = x)