Make replace_java_nondet() work even if remove_returns() hasn't been run #1962

owen-mc-diffblue · 2018-03-22T16:08:24Z

Currently, it finds a function call to a function that should be replaced with a nondet, finds the assignment of the return value on the next line, but then goes and finds a second assignment whose rhs is the lhs of the first assignment, and deletes everything between the function call and the second assignment, replacing it with an assignment of the relevant nondet to the lhs of the second assignment.

I don't understand why it does this, so I've changed it to just use the first assignment. If there is a good reason it does what it currently does then please let me know.

tautschnig · 2018-03-22T17:29:16Z

I have no idea what this code is doing, mainly because I don't know what the code generated by the Java front-end looks like. The code in question was originally merged in #691. As the resulting code should look different, there ought to be a regression test accompanying this change to show what has change (and how this is better than before).

smowton · 2018-03-23T13:41:32Z

@owen-jones-diffblue looks like there's a very particular family of broken tests, and the failures are real (verification success expected, actually got failure)

owen-mc-diffblue · 2018-03-25T15:33:24Z

I understand what is going on now. I hope to have an update to this PR soon.

owen-mc-diffblue · 2018-04-05T16:58:22Z

The purpose of this PR has changed, so I have changed the title. The behaviour when remove_returns has been run, as is the case in cbmc, should not change.

tautschnig · 2018-04-05T17:46:44Z

Thank you very much for all the additional explanations! There are three lines the linter complains about:

src/goto-programs/replace_java_nondet.cpp:192:  assert is deprecated, use INVARIANT, PRECONDITION, CHECK_RETURN, etc. instead  [build/deprecated] [4]
src/goto-programs/replace_java_nondet.cpp:215:  Put braces on a separate next line  [whitespace/braces] [5]
src/goto-programs/replace_java_nondet.cpp:219:  assert is deprecated, use INVARIANT, PRECONDITION, CHECK_RETURN, etc. instead  [build/deprecated] [4]

owen-mc-diffblue · 2018-04-06T09:02:15Z

Thanks for pointing those out @tautschnig, I would have missed them. I recall that the linter and clang-format disagreed about formatting braces for lambdas, but not what the resolution was (if there was one). I've tried making the linter happy.

I should have said, the new version of the PR was done by @JohnDumbell, so all credit for improvements should go to him. I'm only pushing it because it's easier for me to push to my fork and keep the same PR.

tautschnig

Yes, the linter and clang-format disagree on lambdas; I think for this one the resolution is fine as it simply leaves some lines untouched. Otherwise use clang-format's suggestion and add // NOLINT(whitespace/braces).

tautschnig · 2018-04-06T09:15:49Z

src/goto-programs/replace_java_nondet.cpp

+  else
+  {
+    // If not, we need to look at the next line instead.
+    assert(next_instr->is_assign());


This will need to become a DATA_INVARIANT

owen-mc-diffblue · 2018-04-06T09:34:52Z

I've replaced the assertions and slightly clarified the function comment.

tautschnig · 2018-04-06T09:48:26Z

Based on github rules this could get merged as soon as CI passes, but I am wondering whether you want to make sure no none-public tools have regressions? Consequently I'd prefer to leave merging to Diffblue team members.

thk123

You know what this comment is going to say - can we have a test of some description? An end-to-end might be quite difficult if remove-returns is always ran, but perhaps a trivial goto program being fed into this analysis to just exercise the new branch.

In future could reformating/swapping asserts to invariant changes be in a separate commit so easier to see how small the change is.

👍 TG pointer bump passed (diffblue/test-gen#1661)

owen-mc-diffblue · 2018-04-06T15:11:07Z

@thk123 It is very hard to write a test in this repository, because the remove_returns pass is run before the replace_java_nondet in jbmc. The only way I can think to do it is to add a flag to run them in the other order, which would obviously be awful. However, the new configuration will be tested in our private repo, so it will be exercised.

tautschnig · 2018-04-06T15:18:03Z

It is very hard to write a test in this repository, because the remove_returns pass is run before the replace_java_nondet in jbmc.

How about doing a unit test instead? (See also #1915 (comment) in case it helps.)

thk123

This test would be better if if it also checked that the function call hasn't just been removed but actually replaced with the non det expression. You might find the utilities in require_goto_statements and require_expr useful for this. Appologies if I've jumped the gun with this review

thk123 · 2018-04-11T13:25:35Z

unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+TEST_CASE(
+  "Load class with a generated java nondet method call, run remove returns "
+  "both before and after the nondet statements have been removed, check results "
+  "are as expected.", "[!mayfail][core][java_bytecode][replace_nondet]")


Why !mayfail?

The mayfail was an oversight on my part - I was writing it on a branch that still had the old code (and so broke).

owen-mc-diffblue · 2018-04-13T13:53:12Z

@JohnDumbell has added a unit test, using the Catch framework. CI has passed. @thk123 Please review and merge if you approve.

thk123 · 2018-04-16T08:58:32Z

unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+    }
+  }
+
+  REQUIRE((method_removed && replacement_nondet_exists));


Not blocking but in future I'd split this into two require statements - then the output will be more useful (it will say which one is not true).

Thanks 👍

Previously, remove_java_nondet assumed that remove_returns had been run. Now it will work even if remove_returns hasn't been run.

ad62682 Merge pull request diffblue#2071 from thk123/refactor/split-string-unit-tests fc8ba88 Revert to aborting precondition for function inputs 3e2ab6f Merge pull request diffblue#2080 from diffblue/java-bytecode-dependency 6ff1eec cbmc: remove dependency on java_bytecode 0bff19b Merge pull request diffblue#2049 from karkhaz/kk-factor-goto-model-processing 79e3b25 Merge pull request diffblue#2084 from tautschnig/has_subtype-test cd45b0b Test has_subtype on recursive data types 85ac315 Merge pull request diffblue#2082 from thomasspriggs/default_dstring_hash 28c2e8b Merge pull request diffblue#2065 from tautschnig/be-constructor afa6023 Merge pull request diffblue#2061 from tautschnig/simplify-extractbits 014d151 Factor out getting & processing goto-model 06b3adc Merge pull request diffblue#2077 from peterschrammel/stable-tmp-var-names 0b3170d Stabilize clinit wrapper function type parameters 3cd8bf4 Temporary vars tests for goto-diff 9f0626c Prefix temporary var names with function id ca678aa More permissive regression tests regarding tmp var suffixes 47951ca Merge pull request diffblue#2079 from romainbrenguier/bugfix/has-subtype-recursion dd73b1a Specify default hash function of `dstringt` to STL. fe8e589 Avoid infinite recursion in has_subtype 00b9bf6 Merge pull request diffblue#2051 from svorenova/generics_tg2717 cd4bfc3 Merge pull request diffblue#2078 from romainbrenguier/bool-literal-in-while-loop 67ea889 Use bool literal in while loop d229ad9 Merge pull request diffblue#2056 from diffblue/fix-regression-cbmc-memcpy1 506faf0 Refactor a function for base existence 617d388 Utility functions for generic types c07e6ca Update generic specialization map when replacing pointers ed26d0a Merge pull request diffblue#2058 from peterschrammel/stable-disjuncts b663734 Simplify extractbits(concatenation(...)) b091560 Typing and refactoring of simplify_extractbits 49ad1bd Merge pull request diffblue#974 from tautschnig/fix-assert-encoding 16e9599 Merge pull request diffblue#2063 from tautschnig/has-subtype 950f58b Merge pull request diffblue#2060 from tautschnig/opt-local-map 4222a94 Regression tests for unstable instanceof and virtual method disjuncts b44589e Make disjuncts in instanceof removal independent of class loading 3afff86 Make disjuncts in virtual method removal independent of class loading a385d9b Allowed split_string to be used on whitespace if not also trying to strip fe4a642 Merge pull request diffblue#2062 from tautschnig/no-has-deref 145f474 Adding tests for empty string edge cases 07009d4 Refactored test to run all combinations 252c24c Migrate old string utils unit tests e87edbf Removing wrong elements from the make file b165c52 make test work on 32-bit Linux b804570 Merge pull request diffblue#2048 from JohnDumbell/improvement/adding_null_object_id 61f14d8 Merge pull request diffblue#1962 from owen-jones-diffblue/owen-jones-diffblue/simplify-replace-java-nondet fdee7e8 Merge pull request diffblue#2059 from tautschnig/generalise-test 4625cc5 Extend global has_subexpr to take a predicate as has_subtype does e9ebd59 has_subtype(type, pred, ns) to search for contained type matching pred 1f1f67f Merge pull request diffblue#1889 from hannes-steffenhagen-diffblue/develop-feature_generate_function_bodies 048c188 Add unit test for java_replace_nondet 0fe48c9 Make remove_java_nondet work before remove_returns bcc4dc4 Use byte_extract_exprt constructor a1814a3 Get rid of thin (and duplicate) has_dereference wrapper 4122a28 Test to demonstrate assert bug on alpine d44bfd3 Also simplify assert structure found on alpine linux c5cde18 Do not generate redundant if statements in assert expansions 4fb0603 Make is_skip publicly available and use constant argument 5832ffd Negative numbers should also pass the test 3c23b28 Consistently disable simplify_exprt::local_replace_map da63652 Merge pull request diffblue#2054 from romainbrenguier/bugfix/clear-equations d77f6a2 Merge pull request diffblue#1831 from NathanJPhillips/feature/class-annotations 60c8296 Clear string_refinement equations (not dependencies) 314ed53 Correcting the value of ID_null_object 751a882 Factor out default CBMC options to static method 6f24009 Can now test for an option being set in optionst 9a8d937 Add to_annotated_type and enable type_checked_cast for annotated_typet ca77b4e Add test for added annotations b06a27d Introduce abstract qualifierst base class e6fb3bf Pretty printing of java_class_typet e22b95b Fix spurious virtual function related keywords 3ac6d17 Add type_dynamic_cast and friends for java_class_typet ce1f4d2 Add annotations to java_class_typet, its methods and fields f84753d Merge pull request diffblue#2042 from hannes-steffenhagen-diffblue/add_deprecate_macro 7a38669 Merge pull request diffblue#2017 from NathanJPhillips/feature/overlay-classes 75a4aec Revert "the deprecation will need to wait until codebase is clean" 67735b5 Disable deprecation warnings by default 0764f77 Merge pull request diffblue#2036 from romainbrenguier/id_array_list 690b606 Merge pull request diffblue#2039 from peterschrammel/fix-duplicate-msg-json-ui bba17d9 the deprecation will need to wait until codebase is clean 822c757 Regression test for redundant JSON message output de0644d Only force end of previous message if there actually is one. 5a637bf Merge pull request diffblue#2037 from hannes-steffenhagen-diffblue/add_deprecate_macro bff456a Merge pull request diffblue#2040 from tautschnig/remove-swp 87ebe90 Remove vim temp file 228c019 Fix duplicate message output in json-ui 0a2c43e Add DEPRECATED to functions documented as \deprecated 47f4b35 interval_sparse_arrayt constructor from array-list 026c4ca Declare an array_list_exprt class 50a2696 Define ID_array_list 513b67a Merge pull request diffblue#2038 from romainbrenguier/bugfix/assign-at-malloc-site c207106 Test with array of strings 60183a3 Assign string at malloc site 116fffd Add DEPRECATED macro to mark deprecated functions and variables 7952f2c Add option to generate function body to goto-instrument 3d4183a Add ability to overlay classes with new definitions of existing methods dbc2f71 Improve code and error message in infer_opaque_type_fields 7c0ea4d Tidied up java_class_loader_limitt git-subtree-dir: cbmc git-subtree-split: ad62682

owen-mc-diffblue requested review from kroening, peterschrammel, smowton and tautschnig as code owners March 22, 2018 16:08

owen-mc-diffblue changed the title ~~Change odd behaviour of remove_java_nondet()~~ Change odd behaviour of replace_java_nondet() Mar 22, 2018

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch 2 times, most recently from 5e2024c to 067883f Compare March 23, 2018 09:35

tautschnig assigned owen-mc-diffblue Apr 5, 2018

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch from 067883f to 3411e90 Compare April 5, 2018 16:55

owen-mc-diffblue changed the title ~~Change odd behaviour of replace_java_nondet()~~ Make replace_java_nondet() work even if remove_returns() hasn't been run Apr 5, 2018

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch from 3411e90 to 67fa7ba Compare April 6, 2018 08:58

tautschnig reviewed Apr 6, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch 3 times, most recently from a6c086a to ea871b6 Compare April 6, 2018 09:29

tautschnig approved these changes Apr 6, 2018

View reviewed changes

thk123 reviewed Apr 6, 2018

View reviewed changes

karkhaz mentioned this pull request Apr 10, 2018

Path exploration goodies #1915

Merged

thk123 reviewed Apr 11, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch from bb96458 to efda81c Compare April 13, 2018 08:29

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch from efda81c to 60c8468 Compare April 13, 2018 08:33

thk123 approved these changes Apr 16, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch from 60c8468 to f61760e Compare April 16, 2018 09:07

Owen Jones added 2 commits April 16, 2018 10:19

Make remove_java_nondet work before remove_returns

0fe48c9

Previously, remove_java_nondet assumed that remove_returns had been run. Now it will work even if remove_returns hasn't been run.

Add unit test for java_replace_nondet

048c188

owen-mc-diffblue force-pushed the owen-jones-diffblue/simplify-replace-java-nondet branch from f61760e to 048c188 Compare April 16, 2018 09:20

thk123 merged commit 61f14d8 into diffblue:develop Apr 16, 2018

owen-mc-diffblue deleted the owen-jones-diffblue/simplify-replace-java-nondet branch April 16, 2018 10:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make replace_java_nondet() work even if remove_returns() hasn't been run #1962

Make replace_java_nondet() work even if remove_returns() hasn't been run #1962

owen-mc-diffblue commented Mar 22, 2018

tautschnig commented Mar 22, 2018

smowton commented Mar 23, 2018

owen-mc-diffblue commented Mar 25, 2018

owen-mc-diffblue commented Apr 5, 2018

tautschnig commented Apr 5, 2018

owen-mc-diffblue commented Apr 6, 2018 •

edited

Loading

tautschnig left a comment

tautschnig Apr 6, 2018

owen-mc-diffblue commented Apr 6, 2018

tautschnig commented Apr 6, 2018

thk123 left a comment •

edited

Loading

owen-mc-diffblue commented Apr 6, 2018

tautschnig commented Apr 6, 2018

thk123 left a comment

thk123 Apr 11, 2018

JohnDumbell Apr 11, 2018

owen-mc-diffblue commented Apr 13, 2018

thk123 Apr 16, 2018

thk123 Apr 16, 2018

Make replace_java_nondet() work even if remove_returns() hasn't been run #1962

Make replace_java_nondet() work even if remove_returns() hasn't been run #1962

Conversation

owen-mc-diffblue commented Mar 22, 2018

tautschnig commented Mar 22, 2018

smowton commented Mar 23, 2018

owen-mc-diffblue commented Mar 25, 2018

owen-mc-diffblue commented Apr 5, 2018

tautschnig commented Apr 5, 2018

owen-mc-diffblue commented Apr 6, 2018 • edited Loading

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Apr 6, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 6, 2018

tautschnig commented Apr 6, 2018

thk123 left a comment • edited Loading

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 6, 2018

tautschnig commented Apr 6, 2018

thk123 left a comment

Choose a reason for hiding this comment

thk123 Apr 11, 2018

Choose a reason for hiding this comment

JohnDumbell Apr 11, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 13, 2018

thk123 Apr 16, 2018

Choose a reason for hiding this comment

thk123 Apr 16, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 6, 2018 •

edited

Loading

thk123 left a comment •

edited

Loading