SymbolicListener doesn't seem to display path conditions

[nickywilliams]

Hello I have just started evaluating SymbolicPathFinder for use in industry. When I use SymbolicListener on jpf-symbc/doc/Example.java it reports "No path conditions" but when I use SymbolicSequenceListener the path conditions are displayed. This was already reported here: https://verificationglasses.wordpress.com/2017/02/13/installing-java-pathfinder-jpf-for-symbolic-execution/#comment-27 Could you please tell me if I am doing something wrong? Thanks Nicky Williams

[yannicnoller]

Hey Nicky,

sorry for the late answer!

The SymbolicListener would print path conditions that observe a property violation / error during symbolic execution, e.g., an exception. The Example program does not include any error, so your output is expected. You can check the code of the class SymbolicListener: the method instructionExecuted has some out-commented code, which would actually also add the path conditions for program termination without errors, but I think I commented it for some reason. You can play with it.

The SymbolicSequenceListener has a different behavior, which in this case, also prints the path conditions for all paths.

Best Yannic

[nickywilliams]

Hi Yannick

Thanks for this answer. I have tried SymbolicListener out on an example with a couple of exceptions and it does show the details (including path condition) for the tests which raise an exception. But unfortunately I am interested in branch coverage and would like to see all the tests generated, even if no exceptions are raised. I am not sure that I will have much time to try reprogramming the listener, I am trying to just evaluate how well SPF generates tests.

So I have another couple of questions:

1) Is it possible to make an array input symbolic (and how, and with which listener)?

2) If so, can the length of the symbolic array also be symbolic?

3) Is it the case that @Precondition can't treat arithmetic expressions, such as "t==n-1"? (I get a message:

java.lang.RuntimeException: ## Error: parse error in pre-condition n-1not a number)

I hope you can give me at least a quick answer to these questions too.

Nicky

[yannicnoller]

Sorry again for the late answer :/

Regarding q1 and q2: Please check out this paper: Symbolic Arrays in Symbolic PathFinder. The configuration is also mentioned in the documentation. If you have a fixed length, you can alternatively use a normal array and fill it with symbolic values.

Regarding q3: The parsing of the precondition is implemented in the class gov.nasa.jpf.symbc.numeric.PreCondition. It appears that both parts (the right hand side and the left hand side of the expression) must be either variables which are known to have symbolic values (cf. the expression map), or they should a constant number. You could try "t==n" and this should work, if n is also handled symbolically. The current implementation is very rudimentary as you can see. If you want to have an extension, please file another issue or make a pull request.

Best Yannic