Consider the method “test1” of class Problem1.java:

import jbse.meta.Analysis;

public class Problem1 {

	public void foo(){
	}
	public Problem1 calc(int i) {
		if(i > 0) return null;
		else return new Problem1();
	}
	
	public int test1(int x, int y) {
		try{
		if (x > 0) {
			calc(x);
			if (x < y) {
				calc(y).foo();
			}
			else {
				calc(x).foo();
			}
		}
		else if (x < 0){
			if (x < y) {
				calc(x).foo();
			}
			else {
				calc(y).foo();
			}
		}
		y = y + 1;
		if (y > 0) {
			calc(y).calc(1);
		}
		} catch(Exception e) {
			Analysis.ass3rt(false);
		}
		return 0;
		
	}
	
}

Inspect the code and try to count the number of paths in the static control flow graph of the program. Answer the following questions, justifying them: 

a) How many paths can you count in the static control flow graph?

b) How many paths will result in raising an exception?  

Now, use JBSE to symbolically execute method “test1” and count the number of explored paths without pruning unfeasible paths. Use the following settings:

import static jbse.apps.run.RunParameters.DecisionProcedureType.ALL_SAT;
...
p.setMethodSignature("exercises/Problem1","(II)I", "test1");
p.setDecisionProcedure(ALL_SAT);

Inspect the output of the symbolic executor to answer the questions: 

c) How many paths does the symbolic executor explore?

d) How many paths result in raising an exception?

Compare the answers to question a) and b) with the answers to questions c) and d) and possibly rework your answers to questions a) and b) until they match the results of the symbolic execution.

e) Inject an assertion in the program to automatically count the paths that result in raising an exception. Use the JBSE API call: 

import jbse.meta.Analysis;
Analysis.ass3rt(<boolean expression>);

where <boolean expression> is the assertion you need to inject.

Now set JBSE to use the SMT solver Z3. You will need the following settings:

import static jbse.apps.run.RunParameters.DecisionProcedureType.Z3;
...
p.setDecisionProcedure(DecisionProcedureType.Z3);
p.setExternalDecisionProcedurePath(<z3 path>); 

where <z3Path> indicates a string with the full pathname of the Z3 executable program, e.g. "/opt/local/bin/z3".

Now, use JBSE to symbolically execute method “test1” and count the number of traces once again.

f) How many paths does the symbolic executor explore?

g) How many paths result in raising an exception?

h) Report the path condition of an infeasible path that was computed during the first execution (the one that did not prune the infeasible paths). At the purpose use the following settings:

import static jbse.apps.run.RunParameters.StateFormatMode.TEXT;
import static jbse.apps.run.RunParameters.StepShowMode.LEAVES;
...
p.setDecisionProcedure(DecisionProcedureType.ALL_SAT);
p.setStateFormatMode(TEXT);
p.setStepShowMode(LEAVES);

These settings will print the last (leaves) states of the execution traces, with their final path conditions.


Ultime modifiche: mercoledì, 5 maggio 2021, 15:30