Adding a second property in WBS to prove

[vaibhavbsharma]

This version of Wheel Brake System has been part of the SPF repository
for the past few years. It can be found at https://github.com/SymbolicPathFinder/jpf-symbc/blob/master/src/examples/WBS.java. An existing pull request checks one property on this benchmark (#825). In this commit, I am adding it again to the SV-COMP repository of benchmarks so that we can check a different property in it.

• WBS_prop2 is the name of the newly added benchmark
• license file is the same as the one used for existing benchmarks in the java-ranger-regression/ folder
• contributed by developers of Java Ranger (https://github.com/vaibhavbsharma/java-ranger). This benchmark originates from the WBS version maintained in the src/examples directory of the source code of SPF as mentioned earlier.
• The ReachSafety.set category has been updated to now include benchmarks in the java-ranger-regression directory
• assert.prp should be used to verify the intended property
• expected answer has been added WBS_prop2.yml

[dbeyer]

Question: Is here really the property the only difference?
Is there a way to achieve a second property without duplicating the program?

@peterschrammel Can you imagine we use a call to a method as specification, as in the C track?
E.g., A call to verifier_error_1() should not be reachable, second property ...verifier_error_2() ...

[vaibhavbsharma]

Not duplicating the program would be an elegant way to organize benchmarks based on the Wheel Brake System. I would be happy to make this change and an example showing a similar setup in the existing SV-COMP benchmarks would be even more useful!

[mmuesly]

IMHO, we could use the Java exception mechanism for your request @dbeyer.
We could agree on a certain set of exception classes for SV-Comp and instead of violating assertions, a property check might be encoded as an if-condition followed by a throw statement. This way, different properties could be encoded as reachability of different errors. In addition, we might use the same approach for the specification of the reachability of standard Java exceptions as I requested in #823.

In the mean time, we might move the implementation in a single class with one method per check of one assert conditions into the java/common directory and only have small driver files for each property in the benchmark repository. This might reduce code duplication without any further harm to the competition in its current format from my point of view.

[dbeyer]

@vaibhavbsharma and @mmuesly Could you please have a look at the following in the C track?
https://github.com/sosy-lab/sv-benchmarks/tree/master/c/eca-rers2018

There are 100 function calls like __VERIFIER_error_94(), each encoding a different property.

Then there are 100 properties as in properties/unreach-call-94.prp
to verify.

Further, for the task definitions, have a look at
https://github.com/sosy-lab/sv-benchmarks/blob/master/c/eca-rers2018/Problem10.yml

Does this look like the way to go?

[peterschrammel]

(A) Different proposal that doesn't require any change to the infrastructure:

1. Structure your code in a way that separates the implementation from the property.
2. Then put the implementation into java/WBS/impl/WBS.java.
3. Each property propN can then be in java/WBS/propN/Main.java accompanied by a java/WBS/propN.yml that includes the implementation as input_files.

[peterschrammel]

(B) Alternatively, I have a preference for introducing property files that contain exception-specific specs as @mmuesly suggests, e.g.

CHECK( init(Main.main()), LTL(G !java.lang.NullPointerException) )

We can then also use CHECK( init(Main.main()), LTL(G !java.lang.AssertionError) ) instead of CHECK( init(Main.main()), LTL(G assert) ).

[dbeyer]

I like the proposal that @peterschrammel made.

But perhaps it is too late to introduce an extension of the spec language for AssertionError at this point in time?

So perhaps stick with LTL(G assert) for this SV-COMP edition and got to exceptions next time?

What is best for the Java community? I think I have to merge as soon as possible, as there are only 4 days left ...

[dbeyer]

Or would you like me to merge all the PRs and then you refactor via a new pull request?

[peterschrammel]

I'd say, let's go with my proposal (A) above, which doesn't require a rule change or changes to the verifiers; and let's add (B) to the discussion list for the community meeting.

[dbeyer]

So I will simply merge and you would be so kind to implement proposal (A)?
Thanks!

[dbeyer]

Thanks for the new verification tasks.
These tasks are planned to be refactored according to the discussion in pull request #860.