- Thực thi tượng trưng. - Thực thi tượng trưng tĩnh. - Thực thi tượng trưng động. - Kết hợp thực thi cụ thể và thực thi tượng trưng. - 16Hình 2 : Cây thực thi tượng trưng. - 22Hình 3: Cây thực thi tượng trưng được quản lý riêng. - 27Hình 6: Thực thi tượng trưng với câu lệnh gán. - 28Hình 7: Thực thi tượng trưng với câu lệnh rẽ nhánh. - Trạng thái chương trình thực thi trong Symbolic JPF. - 48Hình 16: Bùng nổ việc thực thi tượng trưng trong Symbolic JPF. - Phát hiện và thực thi tự động các UT. - Khi thực thi phương thức kiểm thử Test1 thì ngoại lệ ArgumentNullException được ném ra. - Khi thực thi phương thức kiểm thử Test2 thì ArgumentException được ném ra. - Việc viết các ca kiểm thử đơn vị để thực thi tất cả các đường đi của một chương trình là một công việc nặng nhọc. - Nói cách khác, mỗi UT biểu thị cho một hành vi thực thi cụ thể của chương trình. - PUT cũng xác nhận về hành vị thực thi của chương trình nhưng được mở rộng cho tất cả các giá trị đầu vào có thể. - Với sự hỗ trợ của Pex ta có thể thực thi các ca kiểm thử tham số hóa đó. - Khi Pex thực thi ca kiểm thử tham số hóa ở trên sẽ sinh ra Test Suite gồm 2 VSUnit UT. - PUT sẽ không thể thực thi nếu không có các giá trị cụ thể được truyền vào cho các tham số đầu vào của PUT.. - Ý tưởng chính của thực thi tượng trưng đó là thực thi một chương trình với những giá trị tượng trưng. - Thực thi tượng trưng 2.1.1. - Sự thực thi của chương trình P với đầu vào i ( S được biểu thị bởi P(i).. - Ý tưởng chính của thực thi tượng trưng (SE)[6] là thực thi chương trình với các giá trị tượng trưng (symbolic values) thay vì các giá trị cụ thể (concrete values) của các tham số đầu vào. - Kết quả trả về của một chương trình được thực thi tương trưng nếu có cũng được biểu thị bởi biểu thức của các giá trị tượng trưng. - Một ký hiệu đầu vào biểu thị cho giá trị tượng trưng của một tham số đầu vào lúc bắt đầu thực thi chương trình. - Giá trị tượng trưng cuả các biến và các tham số đầu vào được cập nhật như các giá trị cụ thể của nó trong quá trình thực thi. - Trạng thái của một chương trình được thực thi tương trưng bao gồm các giá trị của các biến trong chương trình, điều kiện đường đi (PC) và biến đếm chương trình (program counter). - Biến đếm chương trình xác định chỉ thị (câu lệnh) tiếp theo sẽ được thực thi. - Trong quá trình thực thi tượng trưng, việc chương trình được thực thi theo một đường đi cụ thể nào đó không phụ thuộc vào các giá trị cụ thể của các biến và các tham số đầu vào. - Để mô tả sự thực thi tượng trưng một chương trình. - Hình 2 : Cây thực thi tượng trưng. - Cây thực thi tượng trưng (Hình 2) biểu thị cho việc thực thi tượng trưng hàm Swap. - Tới câu lệnh rẽ nhánh 1, cả hai nhánh đi của chương trình đều chọn để thực thi với các giá trị tượng trưng. - Khi tới câu lệnh rẽ nhánh 5, thêm 2 nhánh đi mới được xem xét để thực thi với các giá trị tượng trưng. - Và câu lệnh 6 sẽ không bao giờ được thực thi. - Thực thi tượng trưng động chính là sự kết hợp giữa thực thi cụ thể và thực thi tượng trưng. - Trong thực thi tượng trưng động, chương trình được thực thi nhiều lần với những giá trị khác nhau của tham số đầu vào.. - Bắt đầu bằng việc chọn những giá trị tùy ý cho các tham số đầu vào và thực thi chương trình với những giá trị cụ thể đó. - Với những giá trị cụ thể này thì chương trình sẽ được thực thi theo một đường đi xác định. - Hàm DSE bắt đầu được thực thi với giá trị tùy ý của tham số đầu vào. - Tiếp tục thực thi chương trình với giá trị a. - Tiếp tục thực thi hàm DSE với giá trị a={0}. - Bảng 1: Ví dụ về thực thi tượng trưng động. - Chương trình được thực thi với những giá trị ngẫu nhiên với một chiều sâu (depth) định trước của SET. - Với những giá trị cụ thể việc thực thi sẽ đi theo một nhánh cụ thể. - Ví dụ 2.3: Thực thi tượng trưng với phương thức nhận đầu vào là đối tượng. - Với những phương thức nhận tham số đầu vào có kiểu đối tượng thì kỹ thuật khởi tạo lười[29] được sử dụng trong việc thực thi tượng trưng phương thức đó. - Thực thi chương trình với giá trị của các tham số đầu vào được chọn ngẫu nhiên này. - Sau khi thực thi câu lệnh 2, giá trị tượng trưng của x là S(x)=sym+5, giá trị cụ thể của nó cũng được tính toán (x = -5). - Cây thực thi tượng trưng được xây dựng tương ứng với lần chạy này (Hình 3(a. - Ràng buộc obj1≠obj2 tương ứng với nhánh mà sự thực thi cụ thể hiện thời đang đi theo. - Cây thực thi tượng trưng tương ứng với lần thực thi này được biểu thị trong Hình 3(b). - Cây thực thi tương trưng tương ứng với lần thực thi chương trình với các giá trị đầu vào mới sinh ra này được biểu thị trong Hình 3(c).. - Hình 3: Cây thực thi tượng trưng được quản lý riêng. - Các công cụ như Pex[30], CUTE[9] được cài đặt dựa trên kỹ thuật thực thi tượng trưng động. - Tuy nhiên, cần có cơ chế để cho phép một chương trình có thể thực thi tượng trưng. - Việc thực thi tượng trưng một chương trình được biểu thị bằng cây thực thi tượng trưng. - Cộng cụ Pex cũng xây dựng và quản lý cây thực thi tượng trưng để sinh các đầu vào cho PUT. - 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. - 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 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ỏ. - 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. - Hình 7: Thực thi tượng trưng với câu lệnh rẽ nhánh 2.2.3. - Đầ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. - 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. - 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ể. - khởi tạo cây thực thi tượng trưng. - 11: execute(inputs);//inputs đưa tới Test Executor để thực thi. - 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ớ. - 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). - 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).. - 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 ƒ. - VM là một bộ sinh trạng thái bằng việc thực thi các chỉ thị bytecode. - Search Object điều khiển việc thực thi trong JVM. - 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. - 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. - 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.. - Lớp SymbolicInstructionFactory chứa các chỉ thị bytecode theo ngữ nghĩa thực thi tượng trưng. - Phương thức caller là phương thức đang được thực thi hiện thời. - Phương thức caller được thực thi và gọi phương thức callee. - 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.. - 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:. - Việc thực thi chỉ thị IADD theo nghĩa thực thi tượng trưng như sau:. - 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. - Cuối cùng, chỉ thị tiếp theo được trả về để thực thi (dòng 20).. - 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. - Nếu không thì trả về chỉ thị tiếp theo để thực thi (dòng 8). - 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. - Một chương trình bắt đầu thực thi theo ngữ nghĩa thực thi cụ thể. - Từ thời điểm đó, sự thực thi tượng trưng được tiếp tục. - 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. - 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). - 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. - 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ể. - Ta đang muốn thực thi tượng trưng phương thức kiểm thử PUT. - Để thực thi các ca kiểm thử tham số hóa viết cho trong môi trường Eclipse