added test cases to check the string-solver

[lucasccordeiro]

Added test cases to check the Java API methods related to StringBuilder, String, Character, and StringTokenizer (https://github.com/diffblue/cbmc-testgen/issues/113). This PR is related to https://github.com/diffblue/cbmc-testgen/pull/135.

[tautschnig]

Is this possibly in the wrong repository? All the links in the comment hint towards cbmc-testgen. Also, what is being tested here - is it compilation/bytecode conversion?

[tautschnig]

Context needs clarification.

[lucasccordeiro]

@tautschnig: @jgwilson42, @forejtv, and @peterschrammel asked me to write test cases for checking the string-solver.

I have explained how I have created the test cases in this issue https://github.com/diffblue/cbmc-testgen/issues/113. Then I did a PR for cbmc-testgen, in order to merge these particular test cases into cbmc-testgen via https://github.com/diffblue/cbmc-testgen/pull/135. However, @peterschrammel asked me to make the PR to cbmc/master instead of cbmc-testgen.

If you need more clarification than that, then I would recommend that @peterschrammel clarifies it further.

[tautschnig]

Ok, thanks - cbmc-testgen isn't public so I was lacking all the context. I believe the commit message could do with some extensions to clarify what exactly is being tested here. The string solver appears to be work in progress.

[lucasccordeiro]

@romainbrenguier: I have just removed some trailing white-spaces and ^M characters.

@tautschnig: I have added a message to clarify exactly what is being tested here.

[peterschrammel]

Generally, I think that these tests contain too much stuff at once --- they should be split to test each feature separately. Also, we can't have regression tests that take minutes or hours to execute. A test should not run longer than 30 seconds (most tests run in less than a second). It should be as simple as possible and as complex as necessary to exhibit a (potential) bug.

[peterschrammel]

How is this supposed to work?

[peterschrammel]

It would be good to check which of the assertions pass and fail.

[tautschnig]

@lucasccordeiro @peterschrammel A few suggestions:

• Group tests as one commit per feature to address the first concern.
• Use THOROUGH instead of CORE for long-running tests. If the tests can be simplified then even better, but that would be an easy way out.

[lucasccordeiro]

@tautschnig: I'm getting confused about the test desc file. Initially, I wrote it as CORE. Then, @romainbrenguier asked me for changing it to FUTURE. Now, you ask me for changing it to THOROUGH. Should we keep FUTURE or change all test desc to THOROUGH?

[peterschrammel]

Core tests are those that are always run when we run the regression test suite.

Future tests are tests for features that are not implemented yet (or not expected to work soon). They should be set to core as soon as they are expected to work.

Thorough are tests that are expected to work but can't be run as core because they take a long time to execute, for example.

[lucasccordeiro]

I have implemented all comments as suggested:

(1) updated the test description to CORE and FUTURE accordingly.
(2) simplified all test cases so that CBMC can check each feature quickly
(3) distinguished all failing assertions.

In the current version of the string-solver, CBMC takes about 27 seconds to run 117 test cases. However, most test cases exposes segmentation fault in CBMC string-solver.

There is still one comment from Michael that I didn't implement:

• "Group tests as one commit per feature to address the first concern".

I'm unsure which git command we could use to introduce one commit per feature. Should I modify each file and then type the following commands?

$git add file1 file2 ... filen
$git commit -sm "message"
$git push

[tautschnig]

For the grouping part: if an individual test can be mapped onto a particular feature of string refinement, then then it would be great to have that test in a commit that speaks about that particular feature. As such I'd be thinking about:

git reset --soft HEAD^
git reset HEAD .
git add dir1/{test.desc,*.java,*.class} dir2/{test.desc,*.java,.*.class} ...
git commit -s  <enter descriptive message>
<more git add, commit>
git push --force <name of your remote> string-regression

[lucasccordeiro]

I have implemented all comments as suggested in this PR by @romainbrenguier, @tautschnig, and @peterschrammel.

Note that before grouping the test cases by feature, I synchronized that with @romainbrenguier who is leading the implementation of CBMC string-solver.

[tautschnig]

@lucasccordeiro Thanks a lot for all the re-shuffling!

[peterschrammel]

@kroening, this is mergeable now.