ĐẠ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

3.2.3. Xử lý các điều kiện rẽ nhánh

Đ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ụ

public class IADD extends Instruction {...

1: int v1 = th.pop();

2: int v2 = th.pop();

3: th.push(v1 + v2, false);

4: return getNext(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

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);

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);

}

}

}

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.

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.

@Override

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();

...

...

...

...//instruct JPF to backtrack

14: }else{

15: ((PCChoiceGenerator) cg).setCurrentPC(pc);

16: }

17: return getTarget();

...

...

...//instruct JPF to backtrack

21: }else {

22: ((PCChoiceGenerator) cg).setCurrentPC(pc);

23: }

24: return getNext(ti);

}

}

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ể đó.

Каталог: jspui -> bitstream -> 123456789
123456789 -> Nguyễn Ngọc Lý Giám đốc Trung tâm Nghiên cứu về Môi trường và Cộng đồng
123456789 -> Vò Quúnh Thu Cao häc K18
123456789 -> Khoa Báo chí Đhkhxh&NV
123456789 -> Acknowledgements
123456789 -> Danh mục chữ viết tắT
123456789 -> Chương TỔng quan vật liệu mao quản trung bình (mqtb) trật tự 1 Giới thiệu chung
123456789 -> Khoa hóa họC (141 142 báo cáo)

tải về 446.91 Kb.

Chia sẻ với bạn bè của bạn: