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

thuật thực thi tượng trưng được minh họa như Hình 4. Trong đó Test Input Selector (TIS) làm nhiệm vụ quản lý cây thực thi tượng trưng và sinh các đầu vào để Test Executor thực thi chương trình đã được sửa đổi để hỗ trợ việc thực thi tượng trưng với mỗi đầu vào được sinh ra đó. 2.2.1. Lưu trữ giá trị tượng trưng Với các hệ thống kiểm thử mà cài đặt kỹ thuật thực thi tượng trưng ở trên thì cần có các cấu trúc dữ liệu để lưu trữ các giá trị tượng trưng kết hợp với các biến và tham số đầu vào trong quá trình thực thi tượng trưng một chương trình. Nếu kiểu của biến x không phải là kiểu tham chiếu thì giá trị tượng trưng của x biểu thị bởi S(x). S’= S[x → s] biểu thị cho ánh xạ từ biến x tới giá trị tượng trưng s của nó được bổ sung vào S, từ đó S’(x)=s. S’=S-x được sử dụng để biểu thị rằng ánh xạ giữa biến x và giá trị tượng trưng đã được gỡ bỏ. S’(x) trong trường hợp này trả về giá trị cụ thể cho x mà không phải là giá trị tượng trưng. R(o) biểu thị cho giá trị tượng trưng của đối tượng o. R là một ánh xạ giữa đối tượng và giá trị tượng trưng của nó tương tự như S. Ngoài ánh xạ S và R một ánh xạ M cũng được sử dụng. Các ánh xạ S, R, M được cài đặt bằng cấu trúc dữ liệu dạng Map dùng để lưu trữ các cặp giá trị key→value. Địa chỉ bộ nhớ (memory address) là các định danh duy nhất sử dụng như key mà các giá trị tượng trưng có thể ánh xạ tới. Tuy nhiên, trong Java ta không thể truy cập tới các con trỏ và địa chỉ bộ nhớ. Tên của biến được sử dụng là key trong trường hợp kiểu của biến đó không phải là kiểu tham chiếu. Tuy nhiên tên biến thường không phải là duy nhất do đó các ánh xạ được cài đặt bằng việc thêm một biến tượng trưng mới cho mỗi biến cục bộ hoặc mỗi trường của đối tượng trong quá trình sửa đổi mã nguồn của chương trình được kiểm thử. Bằng kỹ thuật phân tích dựa trên kiểu[22] có thể xác định các câu lệnh và các biến liên quan tới các tham số đầu vào để có thể thêm vào phần mã cho chúng để hỗ trợ việc thực thi tượng trưng. Các giá trị tượng trưng được kết hợp với các biến chứ không phải với giá trị của các biến. Trong Java không thể có hai biến có kiểu không phải là kiểu tham chiếu cùng trỏ tới một địa chỉ bộ nhớ. Với một số đối tượng, có thể có nhiều tham chiếu (reference) tới cùng một đối tượng. Tuy nhiên với đối tượng ta cũng có thể dùng các tham chiếu là key. Vì thế ánh xạ R được cài đặt bằng một cấu trúc dữ liệu dạng Map mà ánh xạ một tham chiếu tới một giá trị tượng trưng. Khi một giá trị tượng trưng của một đối tượng được yêu cầu, một tham chiếu tới đối tượng được tìm kiếm trong R và giá trị tượng trưng ánh xạ tới tham chiếu được trả về nếu tham chiếu được tìm thấy. 2.2.2. SE với các kiểu dữ liệu nguyên thủy Để thực thi tương trưng một chương trình thì mã nguồn của chương trình cần được thêm vào các phần mã cho phép việc thực thi tượng trưng. Mỗi câu lệnh trong chương trình đó sẽ được xử lý một lần tại một thời điểm và mã thực hiện việc thực thi tượng trưng sẽ được thêm vào câu lệnh đó nếu cần thiết. Mỗi tham số đầu vào v của chương trình được thay thế bằng một câu lệnh đầu vào tượng trưng getInput(v). Và chương trình sẽ gọi các câu lệnh đầu vào tượng trưng này như là các tham số đầu vào. Mỗi lần trước khi bắt đầu thực thi một lệnh, phần thực thi tượng trưng của chương trình sẽ được khởi tạo. Trong quá trình khởi tạo, một kết nối được thiết lập với bộ lựa chọn dữ liệu kiểm thử (TIS). TIS sinh ra một dãy các giá trị cụ thể để làm đầu vào cho chương trình. Các giá trị đầu vào nhận được từ TIS được lưu vào một bộ nhớ I. I là một ánh xạ cài đặt bởi cấu trúc dữ liệu Map, ánh xạ mỗi tham số đầu vào tới một giá trị đầu vào cụ thể. Nói cách khác bộ nhớ I có thể xem như một dãy các giá trị đầu vào được sắp xếp theo thứ tự. Ví dụ khi câu lệnh đầu vào tượng trưng đầu tiên được thực thi thì giá trị đầu tiên của dãy được sử dụng. Nếu một số tham số đầu vào của chương trình không được thay thế với câu lệnh đầu vào tượng trưng thì chương trình sẽ không được thực thi theo đường đi mong đợi. Mỗi câu lệnh getInput(v) là một phương thức được cài đặt để thực hiện việc gán một giá trị đầu vào cụ thể và giá trị tượng trưng cho tham số đầu vào. Lúc bắt đầu thực thi giá trị tượng trưng của tham số đầu vào được gán bằng một ký hiệu đầu vào duy nhất và nó được đưa tới TIS để giá trị tượng trưng này đại diện cho giá trị đầu vào cụ thể mới. Với các giá trị đầu vào cụ thể, ta cần kiểm tra xem có còn các giá trị cụ thể trong I chưa được chọn để thực thi. Nếu không một giá trị được sinh ngẫu nhiên sẽ được sử dụng. getInput(v) 1: S[v→ si]; // si is a new symbolic value 2: i = i + 1; 3: report(S(v) = si); 4: if (inputNumber є domain(I)) 5: result = I(inputNumber); 6: else 7: result = a random value; 8: inputNumber = inputNumber + 1; 9: return result ; Hình 5: Gán giá trị tượng trưng cho tham số đầu vào Với mọi câu lệnh gán, các giá trị tượng trưng của biến cũng cần được cập nhật với các giá trị mới. Khi một giá trị cụ thể được gán tới một biến, giá trị tượng trưng kết hợp với biến đó được gỡ bỏ nếu có một giá trị tượng trưng như thế tồn tại. Với câu lệnh gán dạng v=v1 nếu v1 có giá trị tượng trưng kết hợp cùng thì chỉ cần sao chép nguyên giá trị tượng trưng của v1 cho v. Trường hợp v=v1 op v2, với op là một phép toán số học thì việc gán là khá phức tạp. Đầu tiên op được kiểm tra xem có được hỗ trợ bởi bộ xử lý ràng buộc đang sử dụng. Nếu op không được hỗ trợ bởi bộ xử lý ràng buộc, việc gán được thực thi cụ thể và giá trị tượng trưng của v được gỡ bỏ. executeAssignment(v, e) 1: match (e) 2: case c: /* c is a contant value */ 3: S = S − v; 4: case v1: /* v1 is a variable */ 5: if (v1 є domain(S)) 6: S = S[v → S(v1)]; 7: else 8: S = S − v; 9: case v1 op v2: 10: if (op {+, −, ∗, /}) 11: S = S − v; 12: else if (v1 Є domain(S) && v2 Є domain(S)) 13: S[v → si]; 14: i = i + 1; 15: report(S(v) = S(v1) op S(v2)); 16: else if (v1 Є domain(S)) 17: S[v → si]; 18: i = i + 1; 19: report(S(v) = S(v1) op v2); 20: else if (v2 є domain(S)) 21: S[v → si]; 22: i = i + 1; 23: report(S(v) = v1 op S(v2)); 24: else 25: S = S − v; Hình 6: Thực thi tượng trưng với câu lệnh gán Thực thi tượng trưng cho câu lệnh rẽ nhánh được thực hiện như sau. Trước tiên cần xác định nhánh đi mà thực thi cụ thể đi theo và sau đó một ràng buộc đường đi được lưu trữ tới đỉnh tương ứng của SET (Hình 7). Cần kiểm tra xem các giá trị tượng trưng có được kết hợp với các biến xuất hiện trong biểu thức điều kiện rẽ nhánh hay không. Nếu chỉ có giá trị cụ thể của biến được sử dụng, TIS không cần được thông báo, việc thực thi câu lệnh không ảnh hưởng tới SET mà TIS đang quản lý. Nếu giá trị tượng trưng được sử dụng thì ràng buộc đường đi tương ứng với cả hai nhánh sẽ được đưa tới TIS. Đỉnh thuộc nhánh mà sự thực thi cụ thể hiện thời đi theo sẽ được đánh dấu là đã thăm và đỉnh tương ứng với nhánh còn lại được đánh dấu là chưa được thăm để tiếp tục mở rộng. Chú ý rằng, ở dòng 2 thông tin của nhánh được với tới trong sự thực thi cụ thể hiện thời được lưu vào một bit-vertor. Bit-vertor chứa tất cả lựa chọn biểu thị cho các nhánh đã chọn và được đưa tới TIS khi phương thức report được gọi. Phương thức report làm nhiệm vụ gửi các thông tin về ràng buộc và các lựa chọn tới TIS để khởi tạo các đỉnh của SET tương ứng với ràng buộc đó. Một chương trình có thể có một vòng lặp vô tận, do đó việc thực thi phải dừng ở một chiều sâu định trước. Vòng lặp trong mã nguồn Java được biến đổi thành câu lệnh goto hoặc một lời gọi đệ quy trong ngôn ngữ trung gian Jimple[17]. executeCondition(op v1 v2) 1: branchTaken = evaluate(v1 op v2); 2: constructBranchBitvector(branchTaken); 3: if (v1 є domain(S) && v2 є domain(S)) 4: report(S(v1) op S(v2), branchTaken); 5: else if (v1 є domain(S)) 6: report(S(v1) op v2, branchTaken); 7: else if (v2 є domain(S)) 8: report(S(v2) op v1, branchTaken); Hình 7: Thực thi tượng trưng với câu lệnh rẽ nhánh 2.2.3. SE với đối tượng Trong phần này, ta sẽ trình bày quá trình sửa đổi mã nguồn của chương trình để cho phép thực thi tượng trưng được mở rộng cho chương trình nhận đầu vào là đối tượng. Bảng 3 bên dưới minh họa việc thêm mã hỗ trợ việc thực thi tượng trưng đối với câu lệnh liên quan tới đối tượng. Bảng 3: Sửa đổi chương trình với câu lệnh liên quan tới đối tượng Trước khi sửa đổi Sau khi sửa đổi o = input; o = getSymbolicObject(o); v = o.field; lazyInitialize(o); executeAssignment(v,o.field); v = o.field; o.field = e; lazyInitialize(o); executeAssignment(o.field,e); o.field = e; if o1 op o2 goto l; executeObjectCondition(op,o1,o2); if o1 op o2 goto l; Với các câu lệnh gán sử dụng tham chiếu tới đối tượng thì không cần thêm phần mã để thực thi tượng trưng câu lệnh đó. Việc xử lý với các biến có kiểu tham chiếu và các biến có kiểu không phải là kiểu tham chiếu là khác nhau. Ví dụ với câu lệnh x=5 và y=null, x là biến kiểu integer và y là biến kiểu tham chiếu. Câu lệnh gán thứ nhất thay thế giá trị tại vị trí bộ nhớ mà biến x được lưu trữ. Nếu một giá trị tượng trưng được kết hợp với vị trí bộ nhớ, việc gán ảnh hưởng tới giá trị được lưu trong đó và cũng ảnh hưởng tới giá trị tượng trưng. Câu lệnh gán thứ hai, giá trị của y không phải là một đối tượng mà là một tham chiếu tới một đối tượng. Điều đó có nghĩa là khi y đươc gán bằng null, nó không thay đổi đối tượng nó tham chiếu. Việc gán các tham chiếu tới đối tượng cho một biến không làm thay đổi các giá trị tượng trưng của các đối tượng mà tham chiếu đó trỏ tới. Nói rộng hơn, không thể thay thế hay xóa một đối tượng được lưu trong vùng nhớ heap trong máy ảo java. Việc loại bỏ các đối tượng lưu trong vùng nhớ heap được thực hiện bởi bộ thu gom rác (Garbage Collector) Thực thi tượng trưng với chương trình nhận đầu vào là đối tượng phức tạp hơn rất nhiều so với đầu vào có kiểu không phải là kiểu tham chiếu. Sự khác nhau với đầu vào có kiểu không tham chiếu đó là với đầu vào kiểu không tham chiếu ta có thể dễ dàng gán một giá trị cụ thể tới một biến nhưng với đầu vào kiểu đối tượng thì không có giá trị cụ thể như thế được đưa ra để gán cho biến. TIS ở hệ thống như trên gửi một địa chỉ logic tới đối tượng đầu vào. Một địa chỉ logic là một số tự nhiên sao cho giá trị 0 là một giá trị đặc biệt tương ứng với tham chiếu null (null reference). Khi TIS muốn 2 đối tượng giống nhau. Nó đưa cho chúng 2 địa chỉ logic giống nhau tới ánh xạ I. Ví dụ nếu bộ nhớ I tương ứng với một dãy (1,0,1,2) thì lời gọi 1 và 3 tới phương thức getSymbolicObject (Hình 8) sẽ trả về tham chiếu tới cùng một đối tượng. Lời gọi 2 sẽ đưa ra một tham chiếu null và lời gọi 4 sẽ trả về tham chiếu tới đối tượng khác với các lời gọi trước. Để có thể trả về một tham chiếu tới đối tượng được tạo. Một ánh xạ từ địa chỉ logic tới đối tượng cụ thể được quản lý. Ánh xạ này gọi là M. Phương thức (Hình 8) khởi tạo các đối tượng tượng trưng làm đầu vào cho chương trình. Đầu tiên kiểm tra xem có một giá trị đầu vào được sử dụng tại điểm thực thi hiện hành. Nếu ánh xạ I chứa một giá trị tương ứng với địa chỉ logic của một đối tượng. Nếu địa chỉ logic tương ứng với tham chiếu null thì giá trị null là kết quả trả về. Ngược lại nó kiểm tra (dòng 5) nếu đối tượng yêu cầu đã được khởi tạo bằng việc tìm kiếm một tham chiếu tới đối tượng trong M. Nếu tham chiếu được tìm thấy nó trả về như kết quả còn nếu không một đối tượng mới được tạo và ánh xạ từ địa chỉ logic tới đối tượng vừa được tạo mới được thêm vào M. Một giá trị tượng trưng objj cũng được kết hợp với đối tượng được tạo. Giá trị j là số lần chạy được sử dụng để ngăn chặn các ký hiệu đầu vào giống nhau được sử dụng nhiều lần. Nếu ánh xạ I không chứa một địa chỉ logic để được sử dụng, một đối tượng mới được tạo ra và một giá trị tượng trưng được kết hợp với nó. Chú ý trong trường hợp này, không có địa chỉ logic được ánh xạ tới đối tượng. Và bất cứ đối tượng mới được trả về bởi getSymbolicObject được tạo đơn giản bằng lớp khởi tạo mặc định của đối tượng. Có nghĩa là các trường của đối tượng không được khởi tạo với các giá trị tượng trưng bởi câu lệnh này. getSymbolicObject(o) 1: if (inputNumber Є domain(I)){ 2: l = I(inputNumber); 3: if (l == 0) 4: result = null; 5: else if (l Є domain(M)) 6: result = M(l); 7: else{ 8: result = new object of type o; 9: R = R[result→ objj]; 10: M = M[l → result]; } 11: }else{ 12: result = new object of type o; 13: R = R[result → objj]; } 14: inputNumber = inputNumber + 1; 15: j = j + 1; 16: return result ; Hình 8: Khởi tạo đối tượng làm đầu vào cho chương trình Trong khởi tạo lười các đối tượng vừa được khởi tạo được ghi nhớ để tránh phải khởi tạo nhiều lần. Các trường của đối tượng được khởi tạo như các đầu vào tượng trưng hoặc có thể thêm một phương thức vào lớp của đối tượng và làm việc khởi tạo. Với các đối tượng mà các trường của nó có kiểu dữ liệu nguyên thủy thì các trường đó được khởi tạo với các giá trị tượng trưng. Tuy nhiên, khi đối tượng có cấu trúc phúc tạp, thì đối tượng được khởi tạo bằng việc chỉ định một số trường của đối tượng khởi tạo với giá trị tượng trưng, một số trường phức tạp khác thì khởi tạo với giá trị cụ thể. Phương thức khởi tạo cần truy cập tới các trường public và private của đối tượng. Trong công cụ khác như JCUTE[9] tất cả các đối tượng làm đầu vào được khởi tạo như một tham chiếu null lần đầu tiên chúng gặp phải trong mỗi lần thực thi và chúng được khởi tạo với các giá trị ngẫu nhiên nếu một ràng buộc yêu cầu chúng là khác null. Phương thức (Hình 9) thực hiện việc thực thi tương trưng câu lệnh rẽ nhánh và thu gom ràng buộc với đối tượng. Phương thức này so sánh các tham chiếu tới các đối tượng thay vì giá trị nguyên thủy. Các ràng buộc với đối tượng là o1=o2, o1≠o2, o1=null, o1≠null với o1 và o2 là các đối tượng tượng trưng. Phương thức thực hiện việc so sánh các đối tượng ở một trong các dạng kể trên và xác định nhánh ra của câu lệnh rẽ nhánh mà sự thực thi cụ thể hiện thời đi theo (dòng 2). Phương thức tạo ra ràng buộc dựa vào giá trị tượng trưng của đối tượng. Một tham chiếu null không có một giá trị tượng trưng kết hợp với nó, tham chiếu null được xử lý như một trường hợp đặc biệt (dòng 6 và 8). Các ràng buộc được tạo ra và nhánh mà sự thực thi cụ thể đi theo sẽ được TIS ghi nhớ. executeObjectCondition(op,o1,o2) 1: if (op Є {==,!=} ) 2: branchTaken = evaluate(o1 op o2); 3: constructBranchBitvector(branchTaken); 4: if (o1 Є domain(R) && o2 Є domain(R)) 5: report(R(o1) op R(o2), branchTaken); 6: else if (o1 Є domain(R) && o2 == null) 7: report(R(o1) op null, branchTaken); 8: else if (o2 Є domain(R) && o1 == null) 9: report(R(o2) op null, branchTaken); Hình 9. Sinh ra các ràng buộc liên quan tới đối tượng 2.2.4. SE với các lời gọi phương thức Trong Java, tất cả các đối số đưa tới phuơng thức bởi giá trị. Điều này có nghĩa rằng khi phương thức được gọi với các đối số có giá trị tượng trưng kết hợp với chúng thì các giá trị tượng trưng đó phải được kết hợp với các biến mới trong phương thức được gọi. Khi một phương thức được gọi, tất cả các giá trị tượng trưng của các đối số được đẩy vào (pushed) một ngăn xếp (stack). Và các giá trị của chúng được đọc từ stack tới biến tượng trưng tương ứng tại thời điểm phương thức được gọi bắt đầu việc thực thi. Do khi một phương thức được thực thi tượng trưng thì kết quả thực thi được trả về nhiều lần do các phương thức được thực thi nhiều lần theo các đường đi khác nhau. Vì vậy một ngăn xếp được sử dụng để lưu các giá trị trả về của một phương thức được gọi. Tuy nhiên, với các lời gọi phương thức thì mã nguồn của phương thức được gọi cần được sửa đổi để cho phép thực thi tương trưng thì phương thức đó mới có thể thực thi tượng trưng với các giá trị tượng trưng được kết hợp với các đối số truyền vào phương thức. Vấn đề với các lời gọi phương thức đó là các phương thức được gọi thường không cho phép thực thi tượng trưng như việc gọi các thư viện trong Java, các phương thức mà mã nguồn của nó không sẵn có để ta có thể thêm vào các phần mã cho phép thực thi tượng trưng phương thức đó. Đây chính là hạn chế của phương pháp sửa đổi mã nguồn chương trình để cho phép thực thi tượng trưng chương trình đó. Tuy vậy, hiện nay Sun Microsystems đã công bố mã nguồn của nền Java(Java Platform) qua dự án OpenJDK[32] do đó việc sửa đổi các thư viện chuẩn của Java để hỗ trợ thực thi tượng trưng là điều có thể thực hiện được. 2.3. Sinh dữ liệu kiểm thử cho PUT Trong mục trước, ta đã trình bày về kiến trúc của một hệ thống kiểm thử sử dụng kỹ thuật thực thi tượng trưng động cũng như việc sửa đổi một chương trình để hỗ trợ việc thực thi tượng trưng động. Chương trình sau khi đã được sửa đổi để hỗ trợ thực thi tượng trưng sẽ đươc thực thi với những giá trị cụ thể. Như đã trình bày trong mục 2.1.3, ban đầu chương trình đã sửa đổi để hỗ trợ thực thi tượng trưng sẽ được thực thi với những giá trị được sinh ngẫu nhiên. Khi chương trình bắt đầu được thực thi lần đầu tiên thì một cây thực thi tượng trưng sẽ được khởi tạo và các đỉnh (node) của cây sẽ được sinh ra dựa vào các thông tin tượng trưng (các ràng buộc, giá trị tượng trưng của các đầu vào) thu được. Các đỉnh tương ứng với nhánh đi mà sự thực thi cụ thể đó đi theo sẽ được đánh dấu là đã thăm và các đỉnh mới được sinh ra tương ứng với các nhánh mà sự thực thi cụ thể không đi theo sẽ được đánh dấu là chưa được thăm. Sau khi lần thực thi đó kết thúc, thì TIS cần chọn ra những đỉnh mà được đánh dấu là chưa thăm để thu gom ràng buộc trên nhánh của cây thực thi chứa đỉnh đó và giải quyết ràng buộc đã thu gom được để sinh các giá trị cụ thể làm đầu vào cho lần thực thi tiếp theo. Quá trình sẽ được lặp lại cho tới khi không còn các đỉnh mới của cây thực thi được sinh ra mà được đánh dấu là chưa được thăm. Để có thể chọn ra được các đỉnh mà được đánh dấu là chưa thăm thì TIS cần sử dụng các kỹ thuật tìm kiếm khác nhau như tìm kiếm theo chiều sâu (Depth-First Search), tìm kiếm theo chiều rộng (Breadth-First Search), tìm kiếm kinh nghiệm. Và các ràng buộc trên đoạn đường đi (path prefix) từ đỉnh gốc tới đỉnh được chọn đó sẽ được thu gom và giải quyết. Thuật toán (Hình 10) dưới đây mô tả việc TIS sinh ra các đầu vào cho chương trình dựa trên cây thực thi tượng trưng mà TIS quản lý. 1: T = newSET();// khởi tạo cây thực thi tượng trưng 2: S = chiến lược tìm kiếm; 3: while(T chưa được thăm hết){ //chọn được đỉnh n chưa được thăm bằng chiến lược S 4: m = n = S(T); 5: pc = true; 6: while (m ≠ T.root){ 7: pc = pc m.constraint; 8: m = m.parent; 9: } inputs = solve(pc); 10: if(isSatisfied(inputs)){//tìm ra được inputs thỏa mãn 11: execute(inputs);//inputs đưa tới Test Executor để thực thi 12: expand(n);//chọn đỉnh n để mở rộng tiếp 13: if(có lỗi thực thi) 14: reportError(); 15: marked(n);// đánh dấu đỉnh n đã được thăm } Hình 10: Thuật toán sinh dữ liễu kiểm thử Tuy nhiên, việc lưu trữ cây thực thi tượng trưng tốn rất nhiều bộ nhớ. Do đó những đỉnh đã được đánh dấu là đã thăm mà không có đỉnh con cần được gỡ bỏ. Với Pex[30] thì các ràng buộc đường đi thu gom được không phải là dạng công thức logic đơn thuần như ta đã trình bày ở trên mà là dạng công thức logic bậc một (first-order logic fomulas)[2]. Chính nhờ việc xây dựng ràng buộc dạng này mà Pex có thể sử dụng một SMT solver (Z3) để xử lý các ràng buộc đó. Pex sinh dữ liệu kiểm thử cho PUT bằng việc xây dựng và quản lý các cây thực thi cục bộ (intraprocedural execution trees). Ví dụ 2.5: void TestAbs(int p,int q){ int m = abs(p); int n = abs(q); if(m > n && p > 0) assertfalse; } int abs (int x){ if( x > 0) return x; else if( x == 0) return 100; else return −x; } Để 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ộ Tf của hàm f được định nghĩa bằng ràng buộc đường đi của đường đi w từ đỉnh vào (entry node) của hàm f tới câu lệnh đại diện bởi n. Ràng buộc đường đi của đỉnh n (localpc(n)) biểu thị bởi các ký hiệu đầu vào của ƒ localpc(n):= lpcn Dg() với mỗi g() xuất hiện trong lpcn Trong đó lpcn là biểu thức kết hợp của ràng buộc trên các cạnh của đường đi w từ gốc của cây thực thi cục bộ tới đỉnh n và Dg() đạ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 lpcn. Khi hàm ƒ gọi hàm g trong thực thi tượng trưng thì giá trị trả về của lời gọi tới hàm g là một đầu vào tượng trưng của ƒ. Giá trị trả về của lời gọi tới hàm g được biểu thị bởi g() 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 Dg cho mỗi ký hiệu hàm để đại diện cho giá trị trả về của lời gọi hàm. Ta định nghĩa Dg bằng định đề (axiom) δg như sau: δg= .. Dg() V localpc(l) Λ ret(l) leaf l in Tg trong đó ret(l)= Gl nếu l là đỉnh treo và ret(l)=Retg(l) trong trường hợp khác. Retg(l) đại diện cho giá trị trả về của g, đó là một biểu thức biểu thị bởi , trên đường đi cục bộ đã được thám hiểm hết đại diện bởi đỉnh treo . Với mỗi đỉnh treo d thì Gd là một biến logic duy nhất đại diện cho d. Quay lại ví dụ trên, TestAbs thực thi với p=1,q=1 thì ràng buộc đường đi cục bộ của đỉnh n được gán nhãn 11 sẽ như sau: localpc(n):=abs(p) > abc(q) Λ p > 0 Λ Dabs(p) Λ Dabs(q) Với đầu vào trên thì chỉ đường đi với x > 0 mới được thám hiểm trong abs, có một đỉnh treo d (đỉnh 2) đại diện cho nhánh của câu lệnh điệu kiện mà chưa được thám hiểm. Dabs sau đó được định nghĩa bởi định đề δabs : δabs= Dabs(x) ó ITE((x > 0, abs(x) = x, Gd) Nếu tất cả các đường đi của abs đều được thám hiểm (Hình 11(b)): δabs= Dabs(x) ó (x ≤ 0 Λ x = 0 Λ abs(x) = 100) Λ (x ≤ 0 Λ x = 0 Λ abs(x) = −x)Λ (x > 0 Λ abs(x) = x) hay δabs = ITE(x ≤ 0, ITE(x = 0, abs(x) = 100, abs(x) = −x),abs(x) = x) Chương 3: Sinh ca kiểm thử tham số hóa với JPF 3.1. Kiến trúc của JPF JPF[28] là một máy ảo Java (JVM) đặc biệt được sử dụng như một bộ kiểm tra mô hình (model checker) cho Java bytecode. JPF được sử dụng để phát hiện lỗi (bugs) trong các chương trình Java. JPF phân tích tất cả các đường đi thực thi của một chương trình Java để tìm ra sự vi phạm (violations) như deaklock hay các ngoại lệ chưa được xử lý. Khi JPF tìm ra một lỗi thì nó báo cáo về toàn bộ đường đi thực thi mà dẫn tới lỗi được phát hiện. Không giống như các trình gỡ rối (debugger) thông thường, JPF ghi nhớ về mọi bước phân tích dẫn đến một phát hiện lỗi. Có thể sử dụng JPF một cách linh hoạt dưới dạng giao diện dòng lệnh hoặc tích hợp vào trong các môi trường phát triển ứng dụng Java như Netbean, Eclipse. JPF là một ứng dụng Java mã nguồn mở cho phép ta cấu hình để sử dụng nó theo các cách khác nhau và mở rộng nó. Máy ảo JPF được cài đặt tuân theo các đặc tả về máy ảo Java nhưng không giống như các máy ảo Java chuẩn khác máy ảo JPF có khả năng lưu trữ trạng thái (state storing), ghi nhớ trạng thái (state matching) và quay lui trong quá trình thực thi chương trình