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

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. Quay lui (backtracking) có nghĩa là JPF có thể phục hồi lại trạng thái thực thi lúc trước để xem có còn những sự lựa chọn thực thi khác. Ghi nhớ trạng thái (state matching) có nghĩa là đánh dấu các trạng thái đã thám hiểm mà không còn cần thiết nữa giúp JPF tránh được những sự thực thi không cần thiết. Trạng thái thực thi của một chương trình bao gồm heap và ngăn xếp tiến trình. Trong khi thực thi JPF kiểm tra mọi trạng thái mới có phải là các trạng thái đã được ghi nhớ. Nếu các trạng thái đã được ghi nhớ JPF sẽ không tiếp tục đi theo đường đi thực thi hiện hành và quay lui tới trạng thái gần nhất mà chưa được thám hiểm. Với những chương trình lớn và phức tạp thì không gian trạng thái trong quá trình thực thi chương trình là rất lớn. Việc lưu trữ và thám hiểm tất cả các trạng thái không phải lúc nào cũng đạt được. JPF sử dụng các kỹ thuật khác nhau để giải quyết vấn đề này đó là các chiến lược tìm kiếm, các kỹ thuật để giảm thiểu số trạng thái chương trình và việc lưu trữ các trạng thái. Có các chiến lược tìm kiếm khác nhau được sử dụng như tìm kiếm theo chiều sâu (Depth-First Search), theo chiều rộng (Breadth-First Search), tìm kiếm kinh nghiệm. Hình 12: Kiến trúc JPF + JPF được thiết kế gồm hai thành phần chính đó là đối tượng máy ảo (VM) và đối tượng tìm kiếm (Search Object). VM là một bộ sinh trạng thái bằng việc thực thi các chỉ thị bytecode. Đối tượng VM có các phương thức chính đó là : forward():sinh ra một trạng thái mới backtrack():phục hồi lại trạng thái ngay trước đó restore(): phục hồi lại một trạng thái tùy ý Search Object là bộ điều khiển của VM. Search Object điều khiển việc thực thi trong JVM. Search Object chịu trách nhiệm chọn lựa trạng thái để VM tiếp tục quá trình thực thi bằng việc điều khiển VM để sinh ra trạng thái tiếp theo (foward) hoặc quay lui về trạng thái đã được tạo lúc trước. Theo mặc định, kỹ thuật tìm kiếm theo chiều sâu được sử dụng. Một kỹ thuật tìm kiếm dựa trên hàng đợi ưu tiên (tìm kiếm kinh nghiệm) cũng được cài đặt và ta có thể cấu hình để sử dụng nó. Phương thức tìm kiếm được cài đặt với một vòng lặp và chỉ dừng lại khi không gian trạng thái đã được thám hiểm hết hoặc tìm ra một sự vi phạm. + Các tính năng mở rộng: Search Listener và VM Listener: Chúng được sử dụng để quan sát việc thực thi bên trong JPF mà không cần cài đặt lại các lớp của VM và Search. Search Listener được đăng ký tới các sự kiện của đối tượng Search: public interface SearchListener {   // got the next state void stateAdvanced (Search search); //state was backtracked one step   void stateBacktracked (Search search); //a previously generated state was restored  void stateRestored (Search search); // JPF encountered a property violation   void propertyViolated (Search search); //a search loop was started void searchStarted (Search search); // the search loop was finished void searchFinished (Search search); } và VM Listener được đặng ký tới các sự kiện của đối tượng VM trong quá trình thực thi một chương trình. VMListener được sử dụng để quản lý việc thực thi các chỉ thị bytecode: public interface VMListener { // VM has executed next instruction    void instructionExecuted (JVM vm); // new Thread entered run() method   void threadStarted (JVM vm); // Thread exited run() method  void threadTerminated (JVM vm); // new class was loaded    void classLoaded (JVM vm); // new object was created    void objectCreated (JVM vm); // object was garbage collected    void objectReleased (JVM vm); // garbage collection mark phase started    void gcBegin (JVM vm); // garbage collection sweep phase terminated    void gcEnd (JVM vm); // exception was thrown    void exceptionThrown (JVM vm); // choice generator returned new value    void nextChoice (JVM vm); ... } Model Java Interface (MJI): Nếu JNI là giao diện cho phép các ứng dụng Java chạy trong máy ảo Java của môi trường thực thi giao tiếp với các thư viện và ứng dụng viết trong các ngôn ngữ khác như C, C++, Assembly của hệ điều hành bên dưới thì MJI là giao diện cho phép các ứng dụng Java chạy trong máy ảo JPF giao tiếp với máy ảo của môi trường thực thi bên dưới. Nói cách khác, MJI cho phép chuyển hướng việc thực thi một chương trình Java bên trong máy ảo JPF sang máy ảo của môi trường thực thi bên dưới (host JVM) mà JPF đang được chạy trên đó. Bộ sinh lựa chọn (CG): JPF sử dụng CG để đạt tới các trạng thái chương trình mong muốn trong trường hợp có nhiều lựa chọn để từ một trạng thái có thể chuyển sang các trạng thái khác. Các trạng thái chương trình được bao gói trong đối tượng SystemState. Mỗi trạng thái bao gồm trạng thái thực thi hiện thời của VM (KernelState), các đối tượng ChoiceGenerator bao gói các sự lựa chọn cho việc chuyển đổi trạng thái (Transition). Bằng việc thực thi các chỉ thị bytecode chương trình có thể chuyển từ một trạng thái này sang một trạng thái khác. Mỗi trạng thái hiện hành của chương trình được đăng ký bởi một đối tượng ChoiceGenerator chứa các sự lựa chọn và trạng thái hiện hành này có thể chuyển tới trạng thái thực thi tiếp theo bằng việc truy vấn tới các giá trị của đối tượng ChoiceGenerator để lựa chọn dãy chỉ thị bytecode sẽ được thực thi tiếp theo. Hình 13: Bộ sinh lựa chọn trong JPF Bộ tạo chỉ thị (Bytecode Factory): Trong JPF có các lớp biểu thị cho tất cả các chỉ thị bytecode được cài đặt để thông dịch các chỉ thị bytecode đó sử dụng thư viện bcel[30]. InstructionFactory là giao diện cho phép tạo các đối tượng Instruction bao gói việc thực thi các chỉ thị bytecode. Khi một chỉ thị bytecode trong tập tin .class được tải vào trong máy ảo JPF để xử lý thì một đối tượng Instruction sẽ được tạo ra. Nói cách khác, khi một tập tin .class được đọc một mảng các đối tượng Instruction sẽ được tạo ra. Các đối tượng Instruction có phương thức execute() để thực hiện việc thực thi chỉ thị bytecode tương ứng. Chế độ thực thi mặc định trong JPF là chế độ thực thi cụ thể. Với giao diện InstructionFactory, ta có khả năng ghi đè các lớp chỉ thị mà cài đặt việc thông dịch các chỉ thị bytecode để thay đổi chế độ thực thi trong JPF. 3.2. Symbolic JPF Thực thi tương trưng một chương trình Java bằng cách cài đặt một trình thông dịch bytecode đặc biệt. Symbolic JPF là sự mở rộng của JPF bằng cách thông dịch bytecode theo ngữ nghĩa thực thi tượng trưng. Symbolic JPF không đòi hỏi phải sửa đổi chương trình mã nguồn như các cách tiếp cận thực thi tượng trưng một chương trình sử dụng JPF trước đây[16, 20, 26]. Với Symbolic JPF, việc thực thi tượng trưng với các phương thức mà gọi các phương thức khác sẽ được thực hiện dễ dàng. 3.2.1. Bộ tạo chỉ thị Bộ tạo chỉ thị (Instuction Factory) cho phép thay thế và mở rộng ngữ nghĩa thực thi cụ thể của bytecode bằng ngữ nghĩa thực thi tượng trưng. Các thông tin tượng trưng được lưu trữ trong các thuộc tính (attributes) kết hợp với dữ liệu chương trình (fields, stack operands, local variables) và được cập nhật trong quá trình thực thi. Thực thi các chương trình Java đã được biên dịch (.class files) bằng cách thông dịch các chỉ thị bytecode bằng một máy ảo Java (VM). Theo mặc định, VM thông dịch các bytecode theo ngữ nghĩa thực thi cụ thể. VM của JPF cũng dựa trên mô hình ngăn xếp (stack machine) và tuân theo các đặc tả về máy ảo Java. JPF cho phép thay đổi ngữ nghĩa thực thị cụ thể cho bytecode bằng cách sử dụng Instruction Factory. Hình 14. Bộ tạo chỉ thị trong JPF Với mỗi phương thức được thực thi, JPF quản lý một đối tượng đó là MethodInfo. Đối tượng MethodInfo lưu trữ các chỉ thị bytecode như là mảng các đối tượng Instruction. Các đối tượng Instruction được tạo ra từ việc đọc các các bytecode từ tập tin .class tương ứng. JPF xây dựng một số ràng buộc trên lớp Instruction hơn là yêu cầu một phương thức execute(). JPF sử dụng mẫu thiết kế abstract factory[3] để khởi tạo các đối tượng Instruction. Lớp SymbolicInstructionFactory chứa các chỉ thị bytecode theo ngữ nghĩa thực thi tượng trưng. Lớp SymbolicInstructionFactory ủy quyền (delegate) tới lớp cha DefaultInstructionFactory chứa các chỉ thị bytecode theo nghĩa thực thi cụ thể. 3.2.2. Các thuộc tính JPF quản lý các trạng thái chương trình tương tự như máy ảo Java chuẩn. Mỗi trạng thái bao gồm một ngăn xếp lời gọi cho mỗi tiến trình, giá trị của các trường (fields) và thông tin lập lịch. Ngăn xếp lời gọi bao gồm các stack frame tương ứng với các phương thức sẽ được thực thi. Mỗi stack frame lưu trữ thông tin tượng trưng trong các vùng biến cục bộ (local variables) và các toán hạng ngăn xếp (stack operands). Hình 15. Trạng thái chương trình thực thi trong Symbolic JPF Hình 15 minh họa trạng thái của chương trình được thực thi bên trong JPF. Phương thức caller là phương thức đang được thực thi hiện thời. Stack frame tương ứng với phương thức caller nằm trên cùng của ngăn xếp lời gọi. Phương thức caller được thực thi và gọi phương thức callee. Trạng thái chương trình bao gồm heap, stack frame tương ứng với phương thức caller, và stack frame tương ứng với phương thức callee. Giá trị của heap và các stack frame được tạo ra thông qua việc thực thi các chỉ thị bytecode khác nhau. Chỉ thị dup làm nhiệm vụ sao lưu các giá trị giữa các khay toán hạng (operand slots) của stack frame. Chỉ thị istore để sao lưu giá trị giữa vùng biến cục bộ(local variable slots) và vùng toán hạng (operand slots). Chỉ thị putfield và getfield để lấy và thiết lập giá trị cho các trường của đối tượng được lưu trong heap. Chỉ thị invokevirtual để gọi phương thức callee và giá trị trả về sẽ được lưu vào vùng toán hạng của stack frame tương ứng với phương thức caller. Các thuộc tính kết hợp với dữ liệu chương trình được gọi là các thuộc tính khe (slot attributes). Trong symbolic JPF, các thuộc tính được sử dụng để lưu trữ các giá trị tượng trưng và các biểu thức tượng trưng được tạo ra trong quá trình thực thi. Các thuộc tính được tạo ra hoặc truy cập bởi các chỉ thị bytecode thông qua các accessors (phương thức setAttr, getAttr). Các thuộc tính cũng có thể được tạo hoặc truy cập thông qua các listener hoặc native peers. Việc thao tác với các thuộc tính được thực hiện hoàn toàn bên trong JPF bởi các hành động khác nhau. Các hành động đó là thay đổi và lưu trữ các trạng thái chương trình (như dup, istore, putfield và getfield). Các lớp chỉ thị bytecode mà thực hiện việc tạo hoặc thay đổi các thông tin tượng trựng sẽ được ghi đè (override) để thay đổi ngữ nghĩa từ thực thi cụ thể thành thực thi tượng trưng. Các lớp chỉ thị bytecode đó là các chỉ thị rẽ nhánh, tính toán số học, chuyển đổi kiểu… Các chỉ thị bytecode mà chỉ lấy ra hoặc lưu trữ các thông tin tượng trưng sẽ được giữ không đổi theo ngữ nghĩa thực thi cụ thể. 3.2.3. Xử lý các điều kiện rẽ nhánh Thực thi tượng trưng các điều kiện rẽ nhánh liên quan tới việc tạo ra các lựa chọn khác nhau cho việc tìm kiếm của JPF. Việc điều hướng việc thực thi đi theo các nhánh thông qua một bộ sinh lựa chọn mới là PCChoiceGenerator. Một điều kiện đường đi được kết hợp với một lựa chọn được tạo ra bởi PCChoiceGenerator. Điều kiện rẽ nhánh hoặc phủ định điều kiện rẽ nhánh sẽ được thêm vào điều kiện đường đi tương ứng với mỗi lựa chọn. Điều kiện đường đi sẽ được kiểm tra sử dụng một bộ xử lý ràng buộc để xác định việc thực thi theo nhánh tương ứng với điều kiện đường đi đó có khả thi. Nếu điều kiện đường đi không thỏa mãn, JPF sẽ quay lui để đi theo các nhánh khả thi khác. Symbolic JPF sử dụng bộ xử lý ràng buộc choco[27] và Iasolver[30] cho các ràng buộc số học tuyến tính. IAsolver có thể xử lý được cả ràng buộc liên quan tới các hàm toán học phức tạp. Hai bộ xử lý ràng buộc này được tích hợp vào JPF thông qua môt giao tiếp (interface) và ta có thể sử dụng một trong 2 bộ xử lý này để thực thi tượng trưng một chương trình thông qua việc cấu hình. 3.2.4. Ví dụ Như đã trình bày ở trên, chỉ những chỉ thị bytecode liên quan tới việc tạo hoặc thay đổi thông tin tượng trưng sẽ được thay đổi ngữ nghĩa từ thực thi cụ thể thành thực thi tượng trưng. Một trong những chỉ thị như thế là chỉ chị IADD, chỉ thị này thực hiện việc tính tổng của 2 số nguyên. public class IADD extends Instruction {... public Instruction execute(...ThreadInfo th){ 1: int v1 = th.pop(); 2: int v2 = th.pop(); 3: th.push(v1 + v2, false); 4: return getNext(th); } } Đoạn mã ở trên thực hiện việc thông dịch chỉ thị IADD theo ngữ nghĩa thực thi cụ thể. Theo mặc định, JPF gồm các lớp chỉ thị tương ứng với các chỉ thị bytecode được cài đặt để thông dịch bytecode theo ngữ nghĩa thực thi cụ thể. Máy ảo JPF thực hiện việc thông dịch bytecode tương tự như các máy ảo Java chuẩn khác. Các máy ảo Java thông dịch bytecode bằng cách thao tác với phần tử ở đỉnh của ngăn xếp (operand stack) trong stack frame. Có 2 thao tác chính là push và pop: + push: chèn một giá trị lên đỉnh operand stack + pop: lấy giá trị lưu ở đỉnh operand stack đồng thời loại bỏ phần tử đó ra khỏi operand stack. Việc thông dịch chỉ thị IADD theo ngữ nghĩa thực thi cụ thể như sau: lấy lần lượt 2 giá trị lưu ở 2 stack operand trên cùng của operand stack (dòng 1 và 2), sau đó tính tổng của chúng và lưu lại kết quả vào operand stack (dòng 3). Cuối cùng là trả về chỉ thị tiếp theo để thực thi (dòng 4). Đoạn mã cài đặt việc thông dịch chỉ thị IADD theo ngữ nghĩa thực thi tượng trưng trong Symbolic JPF: … public class IADD extends gov.nasa.jpf.jvm.bytecode.IADD { @Override public Instruction execute (...ThreadInfo th) { 1: StackFrame sf = th.getTopFrame(); 2: IntegerExpression sym_v1 = ...sf.getOperandAttr(0); 3: IntegerExpression sym_v2 = ...sf.getOperandAttr(1); 4: if(sym_v1==null && sym_v2==null) 5: return super.execute(ss, ks, th); 6: else { 7: int v1 = th.pop(); 8: int v2 = th.pop(); 9: th.push(0, false); 10: IntegerExpression result = null; if(sym_v1!=null) { if (sym_v2!=null) 13: result = sym_v1._plus(sym_v2); else 15: result = sym_v1._plus(v2); } else if (sym_v2!=null) 18: result = sym_v2._plus(v1); 19: sf.setOperandAttr(result); 20: return getNext(th); } } } Ý tưởng của việc thay đổi ngữ nghĩa thực thi của bytecode cũng tương tự như việc sửa đổi (instrument) một chương trình để hỗ trợ việc thực thi tượng trưng. Với các kiểu dữ liệu chuẩn (int, float,…) cần cài đặt các lớp để biểu thị cho kiểu của các biến tượng trưng tương ứng với các kiểu dữ liệu chuẩn đó. Trong Symbolic JPF, IntegerExpression biểu thị cho biểu thức số nguyên tượng trưng. RealExpression biểu thị cho biểu thức số thực tượng trưng. Trong quá trình thực thi tượng trưng, các thông tin tượng trưng được lưu trữ bởi các thuộc tính trong các toán hạng ngăn xếp (stack operand) của ngăn xếp toán hạng (operand stack) tương ứng với stack frame của phương thức đang được thực thi tượng trưng. Việc thực thi chỉ thị IADD theo nghĩa thực thi tượng trưng như sau: Trước tiên, các giá trị tượng trưng lưu trong các thuộc tính của 2 toán hạng ngăn xếp trên cùng được lấy ra (dòng 2 và 3). Việc lấy ra các giá trị tượng trưng lưu trong các thuộc tính không loại bỏ các toán hạng ngăn xếp chứa các thuộc tính đó. Các giá trị tương trưng được biểu thị bằng biểu thức của các giá trị đầu vào tượng trưng. Nếu các giá trị tượng trưng này đều bằng null (dòng 4) thì Symbolic JPF sẽ thực thi chỉ thị IADD theo ngữ nghĩa thực thi cụ thể (dòng 5) . Ngược lại nếu ít nhất một trong 2 giá trị đó khác null, việc thực thi theo nghĩa cụ thể vẫn được thực hiện (dòng 7, 8, 9). Tuy nhiên trong việc thực thi cụ thể này ta không quan tâm tới kết quả của việc tính toán các giá trị cụ thể. Ta cần tính toán các giá trị tượng trưng để kết hợp với thuộc tính tương ứng với kết quả đó. Phương thức _plus thực hiện việc xây dựng một biểu thức tượng trưng mới biểu thị cho kết quả của việc tính tổng của 2 giá trị tượng trưng. Giá trị tượng trưng biểu thị cho tổng của 2 giá trị tượng trưng sẽ được lưu lại vào thuộc tính của kết quả trong toán hạng ngăn xếp (dòng 19). Cuối cùng, chỉ thị tiếp theo được trả về để thực thi (dòng 20). Ví dụ 3.1: Ví dụ này sẽ minh họa việc sử dụng bộ sinh lựa chọn trong việc thực thi tượng trưng với các điều kiện rẽ nhánh. Ta xét chỉ thị rẽ nhánh IF_ICMPEQ, chỉ thị rẽ nhánh này thực hiện việc so sánh giá trị của 2 biến kiểu int trong điều kiện rẽ nhánh có bằng nhau hay không để điều hướng việc thực thi đi theo nhánh mà giá trị trả về của điều kiện rẽ nhánh là true hoặc false. Trong JPF, lớp IfInstruction là lớp trừu tượng cài đặt việc thông dịch các chỉ thị rẽ nhánh if. Lớp này có một phương thức trừu tượng (dòng 2) để nhận giá trị trả về true hoặc false của điều kiện rẽ nhánh. Phương thức trừu tượng này cần được cài đặt tương ứng với mỗi chỉ thị rẽ nhánh if khác nhau. Việc thông dịch các chỉ thị rẽ nhánh if một cách tổng quát như sau: Thực hiện việc đánh giá biểu thức điều kiện rẽ nhánh (dòng 4). Nếu điều kiện rẽ nhánh nhận giá trị true (dòng 5) thì nhảy tới chỉ thị tiếp theo của nhánh tương ứng với điều kiện rẽ nhánh nhận giá trị true (dòng 6). Nếu không thì trả về chỉ thị tiếp theo để thực thi (dòng 8). public abstract class IfInstruction extends Instruction { 1: protected boolean conditionValue; 2: public abstract boolean popConditionValue(ThreadInfo ti); public Instruction execute (... ThreadInfo ti){ 4: conditionValue = popConditionValue(ti); 5: if (conditionValue) 6: return getTarget(); 7: else 8: return getNext(ti); } ... } Với chỉ thị IF_ICMPEQ thì việc đánh giá điều kiện rẽ nhánh được thực hiện như sau. Lấy giá trị của 2 phần tử trên cùng của stack (dòng 1, 2) và trả về kết quả so sánh giữa 2 giá trị đó (dòng 3). Các giá trị này là các giá trị thực do đó điều kiện rẽ nhánh sẽ chỉ nhận một trong hai giá trị là true hoặc false.  public class IF_ICMPEQ extends IfInstruction { public boolean popConditionValue (ThreadInfo ti){ 1: int v1 = ti.pop(); 2: int v2 = ti.pop(); 3: return (v1 == v2); } ... } Lớp IF_ICMPEQ bên dưới cài đặt việc thông dịch chỉ thị IF_ICMPEQ theo ngữ nghĩa thực thi tượng trưng. Khi thông dịch chỉ thị rẽ nhánh theo ngữ nghĩa thực thi cụ thể thì việc thực thi chỉ có thể đi theo một trong hai nhánh tương ứng với điều kiện rẽ nhánh nhận giá trị true hoặc false. Thông dịch một chỉ thị rẽ nhánh theo ngữ nghĩa thực thi tượng trưng thì cả 2 nhánh đều được xem xét để điều hướng việc thực thi đi theo. public class IF_ICMPEQ extends gov.nasa.jpf.jvm.bytecode.IF_ICMPEQ { @Override public Instruction execute(SystemState ss,KernelState ks,ThreadInfo ti) { 1: StackFrame sf = ti.getTopFrame(); 2: IntegerExpression sym_v1 = (IntegerExpression) sf.getOperandAttr(0); 3: IntegerExpression sym_v2 = (IntegerExpression) sf.getOperandAttr(1); // both conditions are concrete 4: if ((sym_v1 == null) && (sym_v2 == null)) { 5: return super.execute(ss, ks, ti); 6: }else{ // at least one condition is symbolic ... 7: ChoiceGenerator cg = new PCChoiceGenerator(2); ... 8: conditionValue = (Integer)cg.getNextChoice()==0 ? false: true; ... 9: int v2 = ti.pop(); 10: int v1 = ti.pop(); ... 11: if (conditionValue) { ... 12: pc._addDet(Comparator.EQ,sym_v1,sym_v2); ... 13: if(!pc.simplify()) {// not satisfiable ...//instruct JPF to backtrack 14: }else{ 15: ((PCChoiceGenerator) cg).setCurrentPC(pc); 16: } 17: return getTarget(); 18: }else { ... 19: pc._addDet(Comparator.NE,sym_v1,sym_v2); ... 20: if(!pc.simplify()) {// not satisfiable ...//instruct JPF to backtrack 21: }else { 22: ((PCChoiceGenerator) cg).setCurrentPC(pc); 23: } 24: return getNext(ti); } } } Việc thông dịch chỉ thị IF_ICMPEQ theo ngữ nghĩa thực thi tượng trưng bắt đầu bằng việc lấy ra các giá trị tượng trưng lưu trong các thuộc tính tương ứng với 2 phần tử trên cùng của stack (dòng 2, 3). Nếu cả 2 giá trị tượng trưng lấy ra là null thì JPF sẽ chuyển hướng sự thực thị chỉ thị IF_ICMPEQ theo ngữ nghĩa thực thi cụ thể (dòng 5). Nếu ít nhất một trong hai giá trị không bằng null, một bộ sinh lựa chọn (CG) sẽ được tạo ra (dòng 7). CG sinh ra lựa chọn cho phép cả 2 nhánh được xem xét để điều hướng sự thực thi đi theo (dòng 8). 3.2.5. Kết hợp thực thi cụ thể và thực thi tượng trưng Symbolic JPF hỗ trợ tốt cho việc kiểm thử phần mềm mức đơn vị. Symbolic JPF có thể kết hợp thực thi cụ thể với thực thi tượng trưng do đó cho phép thực thi một phương thức bằng cách kết hợp giữa các giá trị đầu vào cụ thể và các giá trị đầu vào tượng trưng. Để thực thi tượng trưng một phương thức, ta cần cấu hình để JPF sử dụng lớp thông dịch bytecode theo ngữ nghĩa thực thi tương trưng SymbolicInstructionFactory, chỉ định tên phương thức cần thực thi tượng trưng và các đầu vào nào của phương thức là cụ thể hoặc tượng trưng. Các đầu vào bao gồm các tham số đầu vào của phương thức và các trường toàn cục (global) mà phương thức đó truy cập. Một chương trình bắt đầu thực thi theo ngữ nghĩa thực thi cụ thể. Tất cả các lớp chỉ thị bytecode tượng trưng (các lớp Instruction) chuyển quyền (delegate) thực thi tới các lớp chỉ thị bytecode cha mà cài đặt việc thông dịch bytecode theo ngữ nghĩa thực thi cụ thể khi không có các thông tin tượng trưng lưu trữ trong thuộc tính kết hợp với dữ liệu. Một listener quản lý việc thực thi cụ thể bên trong máy ảo JPF và bùng nổ (trigger) việc thực thi tượng trưng lần đầu tiên một phương thức với tên chỉ định được gọi. Từ thời điểm đó, sự thực thi tượng trưng được tiếp tục. Các thông tin tượng trưng lưu trữ trong các thuộc tính được xử lý. Khi phương thức được thực thi xong, JPF in ra các thông tin thu được trong quá trình thực thi phương thức đó. Một listener đặc biệt được cài đặt để bùng nổ sự thực thi tượng trưng bất cứ lúc nào trong quá trình thực thi cụ thể (Hình 16). Hình 16: Bùng nổ việc thực thi tượng trưng trong Symbolic JPF Listener có thể chuyển về thực thi cụ thể như xử lý các ràng buộc trong PC hiện thời, tính toán các giá trị cụ thể tương ứng với các biến và tiếp tục thực thi trong chế độ thực thi cụ thể. Từ việc có thể thực thi một chương trình kết hợp giữa các đầu vào cụ thể và các đầu vào tượng trưng với Symbolic JPF. Ta có thể sử dụng việc thực thi cụ thể một chương trình để thiết lập các ngữ cảnh thực thi cụ thể khác nhau trong phân tích tượng trưng mức đơn vị. Với một phương thức có nhiều đầu vào ta có thể chỉ định một số đầu vào là cụ thể để giảm đi sự phức tạp của các điều kiện đường đi trong việc thực thi tượng trưng phương thức đó. Tất nhiên, nếu chỉ định một số đầu vào là cụ thể thì việc thực thi tương trưng sẽ không đi theo được tất cả các nhánh mà chỉ đi theo nhánh mà phụ thuộc vào các đầu vào cụ thể đó. 3.3. Sinh PUT với Symbolic JPF Symbolic JPF hỗ trợ việc thực thi tượng trưng các phương thức nhận tham số đầu vào có kiểu dữ liệu là dạng số học (int, long, float, double). Từ khả năng này của Symbolic JPF ta có thể xây dựng một nền kiểm thử cho phép viết các phương thức kiểm thử tham số hóa (PUT) để kiểm thử các lớp Java đơn giản gồm các phương thức nhận tham số đầu vào có kiểu mà Symbolic JPF hỗ trợ. Trong Java, có nền kiểm thử JUnit hỗ trợ viết và thực thi các ca kiểm thử đơn vị. Ta sẽ viết các PUT dựa trên nền kiểm thử này và xây dựng một hệ thống để thực thi các PUT đó để sinh tự động các ca kiểm thử JUnit. Với JUnit ta có thể viết các lớp kiểm thử mà chứa các ca kiểm thử đơn vị JUnit. Ta cũng có thể viết các lớp kiểm thử mà chứa các ca kiểm thử tham số hóa. Nền kiểm thử JUnit ta sử dụng là JUnit 3.8. Do đó ta cần viết các PUT để sinh ra các ca kiểm thử đơn vị JUnit tương ứng với phiên bản này. Cấu trúc của một lớp kiểm thử đối với phiên bản này như bên dưới: import junit.framework.TestCase; //other libraries public class ClassName extends TestCase { public ClassName(String name) { super(name); } protected void setUp() throws Exception { super.setUp(); } protected void tearDown() throws Exception { super.tearDown(); } //JUnit Test Methods ... } Tên của các phương thức kiểm thử JUnit bắt đầu bằng test. Nền kiểm thử JUnit quy ước điều này để xác định một phương thức là phương thức kiểm thử. Quy ước này cũng giống như ta sử dụng thuộc tính [TestMethod] để chỉ định một phương thức là một UT trong nền kiểm thử VSUnit[29] của .NET. Ta cũng sẽ viết lớp kiểm thử tham số hóa có cấu trúc như trên. Chỉ khác rằng các ca kiểm thử đơn vị JUnit được thay thế bằng các ca kiểm thử tham số hóa. Bằng cách viết các ca kiểm thử tham số hóa dựa trên nền kiểm thử JUnit ta sẽ giảm được công sức để xây dựng lại thư viện xác nhận (assertion) và giúp việc sinh lại các ca kiểm thử đơn vị JUnit dễ dàng hơn. Ta sử dụng công cụ Eclipe Classic 3.4.2 để làm môi trường phát triển ứng dụng và viết các ca kiểm thử tham số hóa. Hình 17: Kiến trúc hệ thống cài đặt Với Symbolic JPF, các phương thức muốn được thực thi tượng trưng thì cần được chỉ định để Symbolic JPF có thể thực thi chúng. Việc một phương thức có được thực thi tượng trưng hay không phụ thuộc vào việc ta cấu hình để thực thi nó với JPF. Đoạn mã bên dưới sử dụng cho việc cấu hình: // điều khiển JPF để sử dụng tập hợp các bytecode tượng trưng +vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory // cấu hình JFF để sử dụng Listener cho việc báo cáo kết quả +jpf.listener=gov.nasa.jpf.symbc.SymbolicListener // cấu hình để sử dụng các thư viện toán học +vm.peer_packages=gov.nasa.jpf.symbc:gov.nasa.jpf.jvm // cấu hình để sử dụng bộ xử lý ràng buộc mong muốn +symbolic.dp=iasolver // chỉ định phương thức cần thực thi tượng trưng +symbolic.method=UnitUnderTest(sym#sym#con) // chỉ định lớp chứa phương thức cần thực thi tượng trưng Main JPF là một máy ảo do đó để có thể thực thi tượng trưng một phương thức thì lớp được chỉ định để thực thi phải chứa phương thức main. Và trong phương thức main này phương thức cần thực thi tượng trưng được gọi như bình thường với các giá trị cụ thể. Với phương thức cần thực thi tượng trưng ta cần chỉ định tên và các tham số sẽ được thực thi tượng trưng hoặc thực thi cụ thể. Giả sử như phương thức UnitUnderTest ở đoạn mã cấu hình trên thì 2 tham số đầu vào đầu tiên chỉ định cho thực thi tượng trưng, còn tham số thứ 3 sẽ thực thi cụ thể. Nếu như ta không chỉ định bộ xử lý ràng buộc được sử dụng với cấu hình +symbolic.method thì bộ xử lý ràng buộc choco[27] sẽ được sử dụng mặc định. Ta đang muốn thực thi tượng trưng phương thức kiểm thử PUT. Lớp kiểm thử chứa các phương thức kiểm thử PUT không chứa phương thức main do đó JPF sẽ không thể thực thi nó như thông thường. Do đó thành phần PUTDriver được cài đặt để xử lý điều này. Hệ thống của ta được cài đặt để thực hiện việc cấu hình động JPF và quản lý việc thực thi của JPF qua lớp PUTListener cho việc báo cáo và sinh ra các ca kiểm thử JUnit. Hệ thống cài đặt của ta có ưu điểm hơn so với Pex đó là ta có thể thực thi tất cả các PUT trong một lần chạy. Để thực hiện được điều này ta cần đồng bộ hóa để thực thi lần lượt các ca kiểm thử đó. Tất cả các ca kiểm thử JUnit sinh ra từ việc thực thi lớp kiểm thử chứa các ca kiểm thử tham số hóa đều được đưa vào một lớp kiểm thử JUnit. Tuy nhiên như đã đề cập ở trên, hệ thống của ta áp dụng khả năng của Symbolic JPF để thực thi các PUT do đó chỉ các PUT nhận tham số đầu vào có kiểu số như int, float, long, double mới được thực thi. Hệ thống của ta sẽ mở rộng dễ dàng để thực thi các ca kiểm thử tham số hóa nhận các tham số đầu vào có kiểu tham chiếu khác nếu như Symbolic JPF được mở rộng để thực thi tượng trưng những phương thức như thế. Để thực thi các ca kiểm thử tham số hóa viết cho trong môi trường Eclipse. Ta chạy run configuration và tiến hành cấu hình như sau: Main Class : put.framework.PUTRunner Program arguments :[] Giả sử có một lớp UnderTest chứa phương thức Add đơn giản như sau: public int Add(int x, int y){ String s = “”; if(x == 2*y) { s = s + ”K50”; } if(x > y){ return x - y; } return x + y; } Ta có một PUT là testAdd để kiểm tra việc thực thi của phương thức Add. import junit.framework.TestCase; import put.framework.Assume; public class PUT extends TestCase { void testAdd(int x, int y){ Assume.isTrue(x>0 && x<10); UnderTest ut = new UnderTest(); ut.Add(x, y); } }  Thực thi lớp kiểm thử này ta sẽ được kết quả như hình bên dưới : Hình 18. Một ví dụ với hệ thống cài đặt Lớp GeneratedJUnits_by_PUT được tạo ra chứa các ca kiểm thử JUnit. import junit.framework.TestCase; public class GeneratedJUnits_by_PUT extends TestCase{ private PUT cls_PUT = new PUT(); public GeneratedJUnits_by_PUT(String name){ super(name); } protected void setUp()throws Exception { super.setUp(); } protected void tearDown()throws Exception { super.tearDown(); } public void testAdd_1_minus10000(){ cls_PUT.testAdd(1, -10000); } public void testAdd_10_x(){ cls_PUT.testAdd(10, 0); } public void testAdd_2_1(){ cls_PUT.testAdd(2, 1); } public void testAdd_1_1(){ cls_PUT.testAdd(1, 1); } }  3.4. Mở rộng Symbolic JPF JPF đang ngày càng phổ biến trong cộng đồng mã nguồn mở. Đã có rất nhiều dự án liên quan đến việc mở rộng JPF để ứng dụng nó cho những mục đích khác nhau như kiểm tra mô hình lược đồ trạng thái UML(statechart), kiểm tra mô hình đối với các ứng dụng giao diện (ui) sử dụng javax.swing, java.awt. Khả năng của JPF không chỉ dừng lại ở việc kiểm chứng các chương trình Java đơn luồng mà nó có thể kiểm chứng với mọi chương trình Java đa luồng khác. Ngày nay, các công cụ và các nền hỗ trợ việc phát triển ứng dụng đều được thương mại hóa do đó việc ta nghiên cứu để mở rộng JPF là một việc làm vô cùng có ý nghĩa. Tuy nhiên như ta đã đề cập trong các chương trước, mục đích của ta là sử dụng khả năng của JPF để thực thi các ca kiểm thử tham số hóa viết cho ngôn ngữ Java. Vì vậy, ta chỉ tập trung vào việc nghiên cứu mở rộng khả năng thực thi tượng trưng của JPF để JPF có thể thực thi tượng trưng các chương trình Java nhận những tham số đầu vào có kiểu dữ liệu phức tạp hơn. Trong tương lai gần có thể biến JPF thành một cộng cụ (nền) hoàn thiện hỗ trợ việc thực thi các ca kiểm thử tham số hóa cho bất kỳ chương trình Java nào. 3.4.1. Các phương pháp cũ Đã có những nghiên cứu khác nhau[16, 20, 26] áp dụng khả năng của JPF để thực thi tượng trưng các chương trình Java. Ý tưởng của các phương pháp này đó là sửa đổi các chương trình Java để hỗ trợ việc thực thi tượng trưng và JPF sẽ được sử dụng để thực thi các chương trình Java đã được sửa đổi đó. Quá trình sửa đổi mã nguồn Java ở các cách tiếp cận này không yêu cầu chuyển mã Java thành mã trung gian để thêm các phần mã hỗ trợ việc thực thi tượng trưng. Việc sửa đổi mã nguồn Java được thực hiện bằng cách thay các biến có kiểu cụ thể trong ngôn ngữ Java (int, float, string,…) thành các biến có kiểu tương trưng tương ứng và các hành động tính toán (các phép tính toán, so sánh,...) đối với các biến có kiểu cụ thể đó chuyển thành hành động tính toán với các biến có kiểu tượng trưng tương ứng. Ví dụ như trong Symbolic JPF, biến kiểu int có một kiểu tượng trưng tương ứng là SymbolicInteger, kiểu số thực thì có kiểu tượng trưng tương ứng là SymbolicReal. Nói cách khác, phương pháp sửa đổi ở đây chính là việc chuyển đổi mã nguồn (source-to-source) trực tiếp từ mã nguồn Java sang mã nguồn Java sử dụng các thư viện hỗ trợ thực thi tượng trưng sao cho mã nguồn Java sau khi được chuyển đổi có thể thực thi tượng trưng sử dụng JPF. Các thư viện hỗ trợ thực thi tượng trưng được xây dựng gồm các lớp để biểu thị cho các kiểu tượng trưng và các lớp với các phương thức được cài đặt để thực hiện hành động tính toán với các kiểu tượng trưng đó. Kỹ thuật phân tích phụ thuộc kiểu[22] được sử dụng để hỗ trợ quá trình chuyển đổi mã nguồn. Các cách tiếp cận này hướng tới việc thực thi tượng trưng các chương trình Java nhận đầu vào có cấu trúc dữ liệu phức tạp. Ý tưởng chính ở đây chính là việc kết hợp thực thi tượng trưng với khởi tạo lười[20]. Một phương thức bắt đầu được thực thi với các đối tượng làm đầu vào mà các trường của nó chưa được khởi tạo, khi các trường của đối tượng lần đầu tiên được truy cập trong quá trình thực thi thì khởi tạo lười sẽ được sử dụng để gán các giá trị cho các trường đó. Với các trường của đối tượng có kiểu dữ liệu nguyên thủy hoặc string thì chúng sẽ được khởi tạo với một giá trị tượng trưng tương ứng kết hợp với nó. Với các trường có kiểu tham chiếu thì chúng sẽ được khởi tạo với một giá trị null, hoặc một tham chiếu tới một đối tượng với các trường chưa được khởi tạo, hoặc một tham chiếu tới đối tượng đã được khởi tạo lúc trước có cùng kiểu. Trong thuật toán khởi tạo lười, các phương thức lấy (getter) và thiết lập (setter) được cài đặt cho mỗi trường của lớp. Các trường của lớp sẽ được truy cập và cập nhật bởi các getter và setter này. Một số ví dụ về việc chuyển đổi mã nguồn Java để hỗ trợ thực thi tượng trưng sử dụng JPF ta có thể tham khảo trong[16, 20, 26]. 3.4.2. Hướng mở rộng Như đã trình bày ở trên, JPF được sử dụng để thực thi các chương trình Java đã được sửa đổi để hỗ trợ việc thực thi tượng trưng. Tuy nhiên, ta sẽ không quay lại để nghiên cứu xem làm sao có thể sử dụng JPF để thực thi các chương trình đã được sửa đổi như thế mà cách tiếp cận của ta ở đây là sẽ sử dụng các thư viện hỗ trợ thực thi tượng trưng và ý tưởng khởi tạo lười để thay đổi nghữ nghĩa thực thi các chỉ thị bytecode theo ngữ nghĩa thực thi tượng trưng sao cho JPF có thể thực thi tượng trưng các chương trình nhận đầu vào có kiểu cấu trúc dữ liệu phức tạp. Tất nhiên đó chỉ là việc đầu tiên ta cần làm để có thể mở rộng JPF. Một điều vô cùng quan trọng nữa là nghiên cứu để xây dựng các bộ xử lý ràng buộc để có thể xử lý các ràng buộc sinh ra từ việc thực thi tượng trưng đó. Ta đã được nghe nhiều tới các bộ xử lý ràng buộc hiệu quả như Z3[31], nhưng vấn đề là các bộ xử lý ràng buộc đó thường được viết trong các dạng ngôn ngữ không phải là ngôn ngữ Java. Do đó việc xây dựng các bộ xử lý ràng buộc để có thể tích hợp vào JPF cũng là một thách thức không nhỏ. Như ta đã đề cập ở trên, ta cần xây dựng các thư viện tượng trưng để hỗ trợ việc thực thi tượng trưng chương trình và cũng là để hỗ trợ việc cài đặt các lớp chỉ thị bytecode theo ngữ nghĩa thực thi tượng trưng. Tất nhiên ta sẽ không thay đổi ngữ nghĩa thực thi cho tất cả các chỉ thị bytecode mà chỉ những chỉ thị bytecode nào liên quan đến việc tạo và cập nhật các thông tin tượng trưng và các chỉ thi bytecode rẽ nhánh mới cần thay đổi ngữ nghĩa từ thực thi cụ thể sang ngữ nghĩa thực thi tượng trưng. Trong JPF phiên bản 4.1 mà ta đang nghiên cứu ở đây, ngoài các thư viện hỗ trợ thực thi tượng trưng với kiểu số học JPF còn cung cấp thư viện hỗ trợ thực thi tượng trưng với kiểu String. Việc cài đặt các lớp để biểu thị cho kiểu String tượng trưng và các hành động tính toán đối với kiểu String tượng trưng này cũng như việc cài đặt các lớp hỗ trợ thực thi tượng trưng với kiểu số học. Tuy nhiên có một điều quan trọng mà ta cần lưu ý đó là kiểu String cũng là kiểu tham chiếu như các đối tượng khác. Do đó việc lưu trữ và tính toán các giá trị tượng trưng với kiểu String không giống như đối với kiểu số học. Nếu như với kiểu số học thì các giá trị tượng trưng của các biến được kết hợp với các thuộc tính (attributes) của toán hạng ngăn xếp (stack operands) của ngăn xếp (operand stack) trong stack frame và ở các vùng biến cục bộ thì đối với kiểu String hay các kiểu tham chiếu đối tượng khác các giá trị tượng trưng sẽ được lưu trữ trong vùng nhớ heap. Như ta đã biết đối với máy ảo Java thì vùng nhớ heap chính là vùng nhớ lưu trữ các đối tượng được tạo ra trong quá trình thực thi một chương trình. Nhưng có một điều mà ta cần nhớ đó là mọi thao tác tính toán, so sánh, v.v. đều được thực hiện trên ngăn xếp toán hạng của stack frame với 2 thao tác là push (đẩy) và pop (lấy). Do đó để có thể thay đổi ngữ nghĩa thực thi đối với các chỉ thị bytecode mà thực hiện việc so sánh, tính toán với kiểu tham chiếu thì ta cần có cơ chế để lấy cũng như cập nhật các giá trị tượng trưng được kết hợp với các tham chiếu đó trong vùng nhớ heap để xử lý cùng với thao tác tính toán diễn ra trên ngăn xếp toán hạng của stack frame. Để minh họa điều này ta xét một ví dụ đơn giản với kiểu String như sau: public String Compare(String s){ if(s=="K50") return s + "CNPM"; return s; } Bytecodes tương ứng với phương thức Compare ở trên: // access flags 1 public Compare(Ljava/lang/String;)Ljava/lang/String; L0 LINENUMBER 3 L0 ALOAD 1 LDC "K50" IF_ACMPEQ L1 L2 LINENUMBER 4 L2 NEW java/lang/StringBuilder DUP ALOAD 1 INVOKESTATIC java/lang/String.valueOf(Ljava/lang/Object;)... INVOKESPECIAL java/lang/StringBuilder.(Ljava/lang/String;)V LDC "CNPM" INVOKEVIRTUAL java/lang/StringBuilder.append(Ljava/lang/String;)... INVOKEVIRTUAL java/lang/StringBuilder.toString()Ljava/lang/String; ARETURN L1 LINENUMBER 5 L1 FRAME SAME ALOAD 1 ARETURN L3 LOCALVARIABLE this LBuffer; L0 L3 0 LOCALVARIABLE s Ljava/lang/String; L0 L3 1 MAXSTACK = 3 MAXLOCALS = 2 Chỉ thị bytecode IF_ACMPEQ chính là chỉ thị bytecode thực hiện việc so sánh bằng nhau giữa các tham chiếu đối tượng. Dưới đây là mã cài đặt của nó theo ngữ nghĩa thực thi cụ thể: import gov.nasa.jpf.jvm.ThreadInfo; public class IF_ACMPEQ extends IfInstruction { public boolean popConditionValue (ThreadInfo ti) { int v1 = ti.pop(); int v2 = ti.pop(); return (v1 == v2); } ... } Rõ ràng việc thông dịch chỉ thị này theo ngữ nghĩa thực thi cụ thể không khác gì so với chỉ thị IF_ICMPEQ đối với kiểu dữ liệu nguyên thủy mà ta đã trình bày trong ví dụ của phần trước. Mọi việc so sánh trên operand stack của stack frame đều là việc so sánh đối với các giá trị số học. Với chỉ thị IF_ACMPEQ này thì việc so sánh 2 tham chiếu đối tượng dẫn đến việc so sánh 2 giá trị số học biểu thị cho chúng. Nếu 2 giá trị đó bằng nhau có nghĩa là 2 tham chiếu tới cùng một đối tượng. Điều này cũng tương tự như bộ nhớ (Map) M ánh xạ một địa chỉ logic (logic address) là một số tự nhiên tới một đối tượng mà ta đã làm quen trong chương trước nếu như 2 địa chỉ logic này bằng nhau có nghĩa là chúng đang ánh xạ tới cùng một đối tượng. Nếu như với các biến có kiểu dữ liệu nguyên thủy (int, float, double, long) thì giá trị của nó được đưa trực tiếp lên stack để so sánh và các giá trị tượng trưng của nó được kết hợp luôn cùng các thuộc tính của operand stack thì với kiểu dữ liệu String ở trên cũng như các đối tượng khác thì việc so sánh thực hiện với các giá trị số học đại diện cho chúng còn bản thân các đối tượng đó vẫn lưu trong vùng heap. Như ở ví dụ trên thì giá trị String “K50” chính là một đối tượng lưu trong vùng nhớ heap. Và ràng buộc ta muốn xây dựng với phương thức đó chính là (s=”K50”) và (s!=”K50”). Rõ ràng để có thể xây dựng được các ràng buộc như thế thì cần lấy các giá trị tượng trưng biểu thị cho biến s và hằng “K50” lưu trong vùng nhớ heap và xử lý cùng với các thao tác trên stack operand của stack frame. Đó chính là việc ta phải làm nếu như muốn thay đổi ngữ nghĩa thực thi của chỉ thị bytecode IF_ACMPEQ ở trên theo ngữ nghĩa thực thi tương trưng. Với những chương trình nhận đầu vào có kiểu tham chiếu thì trạng thái của chương được thực thi tượng trưng bao gồm cả trạng thái của vùng nhớ heap. Theo [21] trạng thái đó bao gồm một cấu trúc heap (heap configuration) chứa giá trị tượng trưng của các biến và các trường tham chiếu, một điều kiện đường đi (PC), và biến đếm chương trình (program counter). Với đối tượng thì cần phải xây dựng các ràng buộc liên quan tới các trường của nó. Và kỹ thuật khởi tạo lười được sử dụng để khởi tạo giá trị tượng trưng cho các trường của đối tượng. Với kiểu dữ liệu mảng thì có một giá trị tượng trưng biểu thị cho chiều dài của mảng (length), và danh sách các ô mảng (array cell). Mỗi ô mảng (phần tử mảng) gồm giá trị tượng trưng biểu thị cho vị trí của ô mảng (cell index) và giá trị tượng trưng lưu trong ô mảng đó. Trong JPF thì các lớp thư viện tượng trưng đã được xây dựng cho các mảng có kiểu int. Do đó ta cần sử dụng các thử viện hỗ trợ thực thi tượng trưng này cùng với khởi tạo lười để thay đổi ngữ nghĩa thực thi của các chỉ thị bytecode truy cập (getfield) hay cập nhật (putfield) và các chỉ thị bytecode tính toán và rẽ nhánh khác đối với kiểu tham chiếu để có thể xây dựng ràng buộc được cho đối tượng. Khi mà ràng buộc liên quan tới các trường của đổi tượng được xây dựng và xử lý thì cũng có nghĩa là sẽ có các đối tượng làm đầu vào mới được sinh ra. Tuy nhiên, việc mở rộng JPF chưa được thực hiện ngay trong khóa luận này mà sẽ là trong tương lai gần. KẾT LUẬN Kiểm thử đơn vị tham số hóa đang dần trở lên phổ biến và đóng vai trò vô cùng quan trọng trong phát triển phần mềm. Kiểm thử đơn vị tham số hóa giúp giảm đáng kể chi phí giành cho việc kiểm thử phần mềm, cải thiện khả năng phát hiện lỗi các phần mềm so với phương pháp kiểm thử đơn vị truyền thống trước đây. Nghiên cứu về kiểm thử đơn vị tham số hóa liên quan tới một vấn đề rất rộng và phức tạp trong kiểm thử phần mềm đó là sinh dữ liệu kiểm thử tự động. Tuy nhiên khóa luận cũng đã đạt được một số kết quả hết sức có ý nghĩa đó là đã làm rõ bản chất của kiểm thử đơn vị tham số hóa, phương pháp và các kỹ thuật để sinh dữ liệu kiểm thử tự động sao cho có thể kiểm tra được tất cả các trường hợp thực thi của một chương trình, mô tả về một hệ thống kiểm thử tổng quát nhất giúp cho việc thực thi các ca kiểm thử tham số hóa. Bên cạnh đó khóa luận cũng đã nghiên cứu và ứng dụng một nền kiểm chứng Java bytecode mã nguồn mở đang rất phổ biến hiện nay đó là Java PathFinder cho việc thực thi các ca kiểm thử tham số hóa viết cho ngôn ngữ Java. Từ khả năng của Java PathFinder ta đã xây dựng được một hệ thống kiểm thử để có thể thực thi các ca kiểm thử tham số hóa viết cho các chương trình Java đơn giản nhận tham số đầu vào có kiểu số học để sinh tự động các ca kiểm thử đơn vị JUnit. Trong khóa luận ta cũng đã đề xuất hướng mở rộng Java PathFinder để có thể thực thi tượng trưng những chương trình Java nhận đầu vào có kiểu cấu trúc dữ liệu phức tạp nhằm mục đích hoàn thiện nền kiểm thử mà ta đã xây dựng. Tất nhiên, việc mở rộng Java PathFinder là một vấn đề hết sức phức tạp đi kèm với những kiến thức rất rộng khác nữa đó là việc xử lý các ràng buộc, cũng như cơ chế thực thi của các chỉ thị bytecode. Do thời gian có hạn nên nội dung trình bày trong khóa luận chắc chắn còn rất nhiều thiếu xót. Tuy nhiên, dựa trên khóa luận này ta có thể mở ra rất nhiều hướng nghiên cứu khác như việc mở rộng Java PathFinder để hỗ trợ việc thực thi tượng trưng các chương trình Java nhận đầu vào có kiểu cấu trúc dữ liệu phức tạp, nghiên cứu để cài đặt một hệ thống kiểm thử cho việc thực thi các ca kiểm thử tham số hóa viết trong ngôn ngữ Java sử dụng kỹ thuật thực thi tượng trưng động. TÀI LIỆU THAM KHẢO Tài Liệu Tiếng Anh [1] B. Beizer. Software Testing Techniques. Van Nostrand Reinhold Co., New York,NY, USA, 2nd edition, 1990. [2] Daniel Kroening · Ofer Strichman. Decision Procedures: An Algorithmic Point of View, © 2008 Springer-Verlag Berlin Heidelberg [3] E. Gamma, R. Helm, R. Johnson, and J. M. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994. [4] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, January 2000. [5] H. Zhu, P. Hall, J. May. Software Unit Test Coverage and Adequacy. ACM Computing Surveys, 29 (4). ISSN 0360-0300, December 1997, pp. 366–427. [6] J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–394, 1976 [7] J. de Halleux and N. Tillmann. Parameterized unit testing with Pex (tutorial). In Proc. of Tests and Proofs (TAP’08), volume 4966 of LNCS, pages 171–181, Prato,Italy, April 2008. Springer. [8] Jon Edvardsson. Techniques for Automatic Generation of Tests from Programs and Specifications. Department of Computer and Information Science Linkoping SE-581, Sweden 2006 [9]Koushik Sen. Scalable automated methods for dynamic program analysis. Electro-nic version of doctoral thesis, Department of Computer Science, University of Illinois at Urubana Champaign, 2006. [10] Michael, C.C.; McGraw, G.E.; Schatz, M.A.; Walton, C.C. Genetic algorithms for dynamic test data generation. Automated Software Engineering, 1997. Procee-dings., 12th IEEE International Conference Volume , Issue , 1-5 Nov 1997 Page(s):307 – 308 [11] N. Tillmann and W. Schulte. Unit tests reloaded: Parameterized unit testing with symbolic execution. IEEE Software, 23(4):38–47, 2006. [12] N. Tillmann and W. Schulte. Parameterized unit tests. In Proceedings of the 10thEuropean Software Engineering Conference held jointly with 13th ACM SIG-SOFT International Symposium on Foundations of Software Engineering, pages 253–262. ACM, 2005. [13] Patrice Godefroid. Compositional dynamic test generation. In Proceedings ofthe 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 47-54. ACM, 2007. [14] Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: directed automated random testing. In Proceedings of the ACM SIGPLAN 2005 Conference on program-ming Language Design and Implementation (PLDI), pages 213-223. ACM, 2005. [15] Peli de Halleux and Nikolai Tillmann, Parameterized Test Patterns For Effective Testing with Pex. Copyright Microsoft Corporation.October 21, 2008 [16] Petri Ihantola. Automatic test data generation for programming exercises withsymbolic execution and Java PathFinder. Master's thesis, Helsinki University of Technology, Departement of Theoretical Computer Science, 2006. [17] Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie J. Hendren, Patrick Lam, and Vijay Sundaresan. Soot - a Java bytecode optimization framework. In Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative Research (CASCON), page 13. IBM, 1999. [18]R. Ferguson and B. Korel. The chaining approach for software test data generation. IEEE Transactions on Software Engineering, 5(1):63–86, January 1996. [19]S. Anand, P. Godefroid, and N. Tillmann. Demand-driven compositional symbolic execution. In Proc. of TACAS’08, volume 4963 of LNCS, pages 367–381. Springer, 2008. [20] Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. Generalized symbolic execution for model checking and testing. In 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science, pages 553-568. Springer, 2003. [21] Saswat Anand, Corina S. Pasareanu, and Willem Visser. Symbolic execution with abstraction. International Journal on Software Tools for Technology Transfer (STTT)Volume 11 ,  Issue 1 Pages 53-67 , January 2009 [22] Saswat Anand, Alessandro Orso, and Mary Jean Harrold. Type-dependence analysis and program transformation for symbolic execution. In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4424 of Lecture Notes in Computer Science, pages 117-133. Springer, 2007. [23] S. Khurshid and Y. Suen. Generalizing symbolic execution to library classes. In Proc. PASTE, pages 103-110, 2005. [24] T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Proc. Static Analysis Symposium, Santa Barbara, CA, June 2000. [25]Tao Xie, Nikolai Tillmann, Peli de Halleux, and Wolfram Schulte. Fitness-Guided Path Exploration in Dynamic Symbolic Execution. To appear in Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, Lisbon, Portugal, June-July 2009. [26] Willem Visser, Corina S. Pasareanu, and Sarfraz Khurshid. Test input generation with Java PathFinder. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pages 97-107. ACM, 2004. Các Trang Web [27] [28] [29] [30] 2008 [31] [32] [33] [34]