Some algorithm benchmarks written in Java. #823

zafer-esen · 2019-10-10T13:24:19Z

programs added to new and appropriately named directory
license present and acceptable (either in separate file or as comment at beginning of program)
contributed-by present (either in README file or as comment at beginning of program)
programs added to a .set file of an existing category, or new sub-category established (if justified)
intended property matches the corresponding .prp file
programs and expected answer added to a .yml file according to task definitions

architecture (32 bit vs. 64 bit) matches the corresponding .cfg file
original sources present
preprocessed files present
preprocessed files generated with correct architecture
Makefile added with correct content and without overly broad suppression of warnings

…sive

…updated the BellmanFord-MemUnsat* algorithms.

mmuesly

Thank you Zafer for adding these interesting benchmarks.
I tried to review them, but found a couple of issues that need to be addressed before merging.

In addition, I think these benchmarks raise a couple of interesting question regarding which new properties should be introduced for the Java SV-Comp track. Not all files are checking assert properties. Could you clarify for these examples what the target property is ? Eventually, we could introduce a proposal how to specify these target properties for future versions of the SV-Comp Java track as a second step.

In general, I would suggest to split the PR into smaller pieces of files that should be ready to merge soon and a second PR with files that involve more discussion. This might shorten the time required to get some of the test cases into the code base.

java/algorithms/BellmanFord-FunSat01/Main.java

mmuesly · 2019-10-23T09:12:35Z

java/algorithms/BellmanFord-FunSat01/Main.java

+    final int V = Verifier.nondetInt();
+    if (V <= 0) return; // change with Verifier.assume?
+
+    final int D[] = new int[V*V];


Site notice:

Until now, I think just assert statements are allowed to specify reachability properties in the Java track but it would be interesting to check here for the possible overflow in the execution.

Specifying the reachability of certain Standard Java-Exceptions might be one option report this overflow or we might add an assert statement that ensures no overflow before the int.

nit-pick:
INFINITY < V might occur using Verifier.nondetInt()

I guess the change INFINITY = Integer.MAX_VALUE should resolve this:

nit-pick:
INFINITY < V might occur using Verifier.nondetInt()

Adding the assumptions I've mentioned in another comment should resolve the overflow issue I think:

assume that V is at most 1e6, which should still be almost impossible to verify using bounded methods and cause no overflows in the calculations

assume the same with the initialization of D at line 98

Specifying the reachability of certain Standard Java-Exceptions might be one option report this overflow or we might add an assert statement that ensures no overflow before the int.

We have assumed that the verifier should check the reachability of these standard exceptions. If this is not suitable, maybe we can wrap the potentially unsafe code with try-catch blocks, with assert false; in the catch statement?

It is my understanding that currently only explicit assert violations are checked in this category according to the property file. Using a try-catch blog sounds legit to me. But I might be wrong.
Otherwise it might be possible to define a new property for checking the standard errors on a program and use such a property along with this file. I am not sure, what would be the better approach.

Eventually @peterschrammel or @dbeyer might give some guidance for the better solution here.

mmuesly · 2019-10-23T09:20:53Z

java/algorithms/BellmanFord-FunSat01/Main.java

+    for (int i = 0; i < V; i++) {
+      for (int j = 0; j < V; j++) {
+        if (i == j) continue;
+        D[i*V+j] =  Verifier.nondetInt();


Using the complete Integer space in the weight function in combination with the standard Java integer arithmetic will lead to potentially tons of overflows in line 67 and 68 that impact the algorithm's functional correctness.
Nevertheless, if a run terminates the assert in line 106 might hold while the complete result is wrong regarding the requirements of the BellmanFord algorithm.

In my personal Opinion, this example needs a stronger guard for checking the functional correctness, or more asserts/assumes guarding the arithmetic to be valuable to the SV-Comp Java benchmark set. But this comment is only intended to start a discussion.

I am not sure how we can strengthen the assertions without making them almost impossible to verify. Maybe we can add two assumptions?

assume that V is at most 1e6, which should still be almost impossible to verify using bounded methods and cause no overflows in the calculations

assume the same with the initialization of D at line 98

I think the assumptions might be fine for now. Nevertheless, being able to verify such functional correctness properties and find a way to express them might be an interesting challenge in the long term.

I've added the assumptions to BellmanFord benchmarks for now.

java/algorithms/BellmanFord-FunUnsat01/.#Main.java

mmuesly · 2019-10-23T10:24:40Z

java/algorithms/BellmanFord-MemSat01/Main.java

@@ -0,0 +1,104 @@
+import org.sosy_lab.sv_benchmarks.Verifier;


From my point of view, this example is missing an assert statement. What is the property that should be checked here?

The benchmarks with the extension MemSat and MemUnsat are all without explicit assertions, and the property being checked is that there are no thrown standard Java exceptions. As you've mentioned in another comment we have assumed that the verifier should check the reachability of these standard exceptions.

If this is not suitable, maybe we can wrap the potentially unsafe code with try-catch blocks, with assert false; in the catch statement?

LGTM! Thank you for changing the benchmarks.

mmuesly · 2019-10-23T11:11:43Z

java/algorithms/Tsp-MemSat01/Main.java

@@ -0,0 +1,123 @@
+import org.sosy_lab.sv_benchmarks.Verifier;


From my point of view, this file is missing an assert statement. What is the property, that should be proved here?

mmuesly · 2019-10-23T11:12:05Z

java/algorithms/Tsp-MemUnsat01/Main.java

@@ -0,0 +1,123 @@
+import org.sosy_lab.sv_benchmarks.Verifier;


From my point of view, this file is missing an assert statement. What is the property, that should be proved here?

mmuesly · 2019-10-23T11:14:47Z

java/algorithms/MergeSortIterative-FunUnsat01/Main.java

+ */
+
+// IterativeMergeSort.java
+// By David Kosbie


I think this is not a proper license. Might you clarify it?

I've tracked the original source of the benchmark to here, but I cannot really see any mention of a license either. I can separate the MergeSort algorithms from the pull request until I can resolve this issue.

mmuesly · 2019-10-23T11:15:14Z

java/algorithms/MergeSortIterative-FunSat01/Main.java

+
+// IterativeMergeSort.java
+// By David Kosbie
+


I think this is not a proper license. Might you clarify it?

Same as above.

mmuesly · 2019-10-23T11:18:43Z

java/algorithms/BellmanFord-FunSat01/Main.java

@@ -0,0 +1,109 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+


General comment: I think all files need a clear comment under which license the modifications are published.
Further, there should be a clear indication whether the files is modified or not and how is the author of the modifications.

dbeyer · 2019-10-27T13:07:18Z

@zafer-esen Could you please complete this pull request such that it can be merged?
People would like to train on the programs.

zafer-esen · 2019-10-27T14:34:07Z

@zafer-esen Could you please complete this pull request such that it can be merged?
People would like to train on the programs.

Hi @dbeyer, I have just pushed a new commit covering most of the requested changes.

I have not done anything regarding the issue in this comment. Depending on your feedback, I can add the try-catch blocks in the memory safety benchmarks in this pull request or separately.

Addiiton of more benchmarks with different assertion strength levels proposed in this comment is also not in the latest commit. I can maybe create another pull request for those?

dbeyer · 2019-10-29T18:47:10Z

@zafer-esen I would say yes to both comments (yes, in the competition we check (currently) only for asserts that are reached and violated, yes, please add the variants, but in a new pull request).

…est memory safety

zafer-esen · 2019-10-29T19:34:56Z

@dbeyer and @mmuesly, thank you both for your comments. I have added the assertions via try-catch blocks to all the benchmarks which lacked these, in the latest commit.

Regarding this comment, I have not deleted the MergeSortIterative* benchmarks as I have contacted the original author David Kosbie (koz@cmu.edu), and he kindly granted permission to freely use this code. I have added this info to the headers of the relevant benchmarks, if this will suffice.

I will create another pull request for the sorting algorithm benchmaks, with assertions which test stronger properties.

dbeyer · 2019-11-09T10:00:39Z

@mmuesly Could you please have another look? Is this pull request ready to be merged from your point of view?

mmuesly

I finished a second round of review.
The modifications made by @zafer-esen look good to me. I think the benchmarks are following the SV-Comp format now and might be merged. Thank you for the additional work invested.

@dbeyer I would love to add the following point to the wish list for future SV-Comp Java infrastructure arising from the discussion about this PR:

Integrate property definitions for standard exceptions. There are various examples in the code base of SV-Comp triggering standard exceptions. As these are standard exceptions, Java verification tools should be able to detect them from my point of view. It would be interesting to make this also part of the competition.

Does CI make sure these test cases are compilable? I haven't checked this myself, but we might fix this along the way, if problems arise. This PR contributes some examples using more than one Java file. I think this is the first time I have seen this in the Java track. Therefore, we should check that all tools are able to deal with these cases from my point of view, even if the rule allow this explicitly.

mmuesly · 2019-11-11T08:47:09Z

java/algorithms/BellmanFord-MemSat01/Main.java

@@ -0,0 +1,104 @@
+import org.sosy_lab.sv_benchmarks.Verifier;


LGTM! Thank you for changing the benchmarks.

PhilippWendler · 2019-11-11T10:13:14Z

Does CI make sure these test cases are compilable? I haven't checked this myself, but we might fix this along the way, if problems arise.

CI checks test cases if they are added to compile.xml, which this PR does. This CI check just runs javac with all .java files below any of the directories in input_files.

dbeyer

@mmuesly Thanks for the reviewing and suggestions for improvement.

I added the suggestion (properties for standard exceptions) as issue #884 separately.
This should be done. Next time.

zafer-esen added 17 commits October 8, 2019 13:15

added some more bms, which still need some cleaning.

eebbf1a

Merge remote-tracking branch 'upstream/master'

30df68b

deleted Mccarthy91-01, it's already among the bms under jayhorn-recur…

b1482ef

…sive

changed folder name and added revised BellmanFord benchmarks

1726984

deleted the jayhorn folder

2e58841

renamed directory

2779b1f

updated binary tree search benchmarks

a3c41c4

updated insertion sort

69696b5

updated iterative merge sort

34fdc2f

updated red black tree

94a3c2c

updated sorted list insert

8d592e1

added trie, and deleted simple loop bms

942b25d

revised tsp

b1273c7

updated .xml and .set files

1688098

removed .yml file which did not have a corresponding benchmark. also …

a9f91e7

…updated the BellmanFord-MemUnsat* algorithms.

Merge branch 'master' of https://github.com/sosy-lab/sv-benchmarks

c02af02

deleted redundant tsp benchmarks

5adccf7

dbeyer added for verification Java Task in language Java new benchmarks labels Oct 15, 2019

Merge branch 'master' of https://github.com/sosy-lab/sv-benchmarks

6986d68

mmuesly suggested changes Oct 23, 2019

View reviewed changes

implemented most of the changes asked in pull request sosy-lab#823

b76736c

added reachable assertions via try-catch blocks to benchmarks which t…

f848b1a

…est memory safety

mmuesly approved these changes Nov 11, 2019

View reviewed changes

mmuesly mentioned this pull request Nov 11, 2019

Adding a second property in WBS to prove #860

Merged

dbeyer mentioned this pull request Nov 11, 2019

Property definitions for standard Java exceptions #884

Open

dbeyer approved these changes Nov 11, 2019

View reviewed changes

dbeyer merged commit c7faa6e into sosy-lab:master Nov 11, 2019

zafer-esen mentioned this pull request Nov 13, 2019

Extra java algorithm benchmarks which check stronger sortedness properties #906

Merged

4 tasks

vaibhavbsharma pushed a commit to vaibhavbsharma/sv-benchmarks that referenced this pull request Nov 20, 2019

implemented most of the changes asked in pull request sosy-lab#823

c12ee97

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Some algorithm benchmarks written in Java. #823

Some algorithm benchmarks written in Java. #823

zafer-esen commented Oct 10, 2019 •

edited

Loading

mmuesly left a comment

mmuesly Oct 23, 2019

zafer-esen Oct 23, 2019

mmuesly Oct 23, 2019

mmuesly Oct 23, 2019

zafer-esen Oct 23, 2019

mmuesly Oct 23, 2019

zafer-esen Oct 23, 2019

mmuesly Oct 23, 2019

zafer-esen Oct 23, 2019

mmuesly Nov 11, 2019

mmuesly Oct 23, 2019

mmuesly Oct 23, 2019

mmuesly Oct 23, 2019

zafer-esen Oct 23, 2019

mmuesly Oct 23, 2019

zafer-esen Oct 23, 2019

mmuesly Oct 23, 2019

dbeyer commented Oct 27, 2019

zafer-esen commented Oct 27, 2019

dbeyer commented Oct 29, 2019

zafer-esen commented Oct 29, 2019

dbeyer commented Nov 9, 2019

mmuesly left a comment

mmuesly Nov 11, 2019

PhilippWendler commented Nov 11, 2019

dbeyer left a comment

		@@ -0,0 +1,104 @@
		import org.sosy_lab.sv_benchmarks.Verifier;

		@@ -0,0 +1,123 @@
		import org.sosy_lab.sv_benchmarks.Verifier;

		@@ -0,0 +1,109 @@
		import org.sosy_lab.sv_benchmarks.Verifier;

Some algorithm benchmarks written in Java. #823

Some algorithm benchmarks written in Java. #823

Conversation

zafer-esen commented Oct 10, 2019 • edited Loading

mmuesly left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dbeyer commented Oct 27, 2019

zafer-esen commented Oct 27, 2019

dbeyer commented Oct 29, 2019

zafer-esen commented Oct 29, 2019

dbeyer commented Nov 9, 2019

mmuesly left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

PhilippWendler commented Nov 11, 2019

dbeyer left a comment

Choose a reason for hiding this comment

zafer-esen commented Oct 10, 2019 •

edited

Loading