[TG-9189] Value retriever: Allow @nondetLength field to be false. #5043

allredj · 2019-08-20T17:55:12Z

This can happen with Arrays$ArrayList.
get_untyped now no longer calls has_nondet_length, which would fail if @nondetLength was false.

There will be a regression test in TG.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 3786fa1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123942200
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

codecov-io · 2019-08-20T18:43:27Z

Codecov Report

Merging #5043 into develop will decrease coverage by 0.05%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #5043      +/-   ##
===========================================
- Coverage    69.53%   69.48%   -0.06%     
===========================================
  Files         1314     1310       -4     
  Lines       108988   108815     -173     
===========================================
- Hits         75786    75611     -175     
- Misses       33202    33204       +2

Impacted Files	Coverage Δ
jbmc/src/java_bytecode/assignments_from_json.cpp	`97.8% <100%> (+0.01%)`	⬆️
...lvers/strings/string_constraint_generator_main.cpp	`80.72% <0%> (-2.61%)`	⬇️
src/util/unicode.cpp	`78.07% <0%> (-0.75%)`	⬇️
jbmc/src/java_bytecode/expr2java.cpp	`84.57% <0%> (-0.4%)`	⬇️
.../goto-instrument/goto_instrument_parse_options.cpp	`56.26% <0%> (-0.4%)`	⬇️
src/solvers/strings/string_refinement.cpp	`88.28% <0%> (-0.25%)`	⬇️
src/solvers/strings/string_dependencies.cpp	`82.6% <0%> (-0.15%)`	⬇️
unit/catch/catch.hpp	`41.26% <0%> (-0.09%)`	⬇️
src/goto-symex/goto_symex.cpp	`99.34% <0%> (-0.01%)`	⬇️
...src/java_bytecode/java_bytecode_convert_method.cpp	`97.52% <0%> (ø)`	⬆️
... and 13 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 153a4b9...3786fa1. Read the comment docs.

smowton · 2019-08-20T19:06:29Z

jbmc/src/java_bytecode/assignments_from_json.cpp

-  if(get_type(json) || has_nondet_length(json))
-    return json[object_key];
-  return json;
+  if(!json.is_object())


Are you really expecting just any old thing here when it's not an object, or do you expect something specific, such as null for example? If so, check for your expectation.

@smowton It could be pretty much anything so I think this change makes sense.

antlechner

I think the ticket number should be at the beginning of the PR title.
Thanks for fixing this!

antlechner · 2019-08-21T11:22:26Z

jbmc/src/java_bytecode/assignments_from_json.cpp

-  if(get_type(json) || has_nondet_length(json))
-    return json[object_key];
-  return json;
+  if(!json.is_object())


@smowton It could be pretty much anything so I think this change makes sense.

antlechner · 2019-08-21T11:25:33Z

jbmc/src/java_bytecode/assignments_from_json.cpp

+
+  const auto &json_object = to_json_object(json);
+  PRECONDITION(
+    get_type(json) || json_object.find("@nondetLength") != json_object.end());


⛏️ We could be more precise and assert the current precondition only if json is contains a json_arrayt, and assert only get_type(json) otherwise, as we wouldn't expect a @nondetLength key on e.g. a number or boolean. But then again in the current version we would just ignore such @nondetLength keys, which wouldn't cause any harm.

precondition is split

This introduced problems, so I reverted to the initial solution.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 01d759f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/124064989
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 31f77ab).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/124068722

antlechner · 2019-08-21T15:12:57Z

jbmc/src/java_bytecode/assignments_from_json.cpp

+
+  const auto &json_object = to_json_object(json);
+  if(json.is_array())
+    PRECONDITION(json_object.find("@nondetLength") != json_object.end());


This would have to be

PRECONDITION(get_type(json) || json_object.find("@nondetLength") != json_object.end());

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 926d4b8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/124113599
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj · 2019-08-22T15:21:07Z

Blocked by #5047

This can happen with Arrays$ArrayList. get_untyped now no longer calls has_nondet_length, which would fail if @nondetLength was false.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 901403d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/124729691

allredj requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners August 20, 2019 17:55

allredj self-assigned this Aug 20, 2019

allredj changed the title ~~Value retriever: Allow @nondetLength field to be false.~~ Value retriever: Allow @nondetLength field to be false. [TG-9189] Aug 20, 2019

allredj commented Aug 20, 2019

View reviewed changes

smowton reviewed Aug 20, 2019

View reviewed changes

antlechner approved these changes Aug 21, 2019

View reviewed changes

antlechner added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Aug 21, 2019

allredj force-pushed the bugfix/retriever-arrays-arraylist branch 2 times, most recently from 01d759f to 31f77ab Compare August 21, 2019 13:21

allredj commented Aug 21, 2019

View reviewed changes

antlechner reviewed Aug 21, 2019

View reviewed changes

allredj force-pushed the bugfix/retriever-arrays-arraylist branch from 31f77ab to 926d4b8 Compare August 21, 2019 17:22

allredj commented Aug 21, 2019

View reviewed changes

allredj force-pushed the bugfix/retriever-arrays-arraylist branch 2 times, most recently from 43b05de to 681f353 Compare August 22, 2019 14:24

Allow @nondetLength field to be false.

901403d

This can happen with Arrays$ArrayList. get_untyped now no longer calls has_nondet_length, which would fail if @nondetLength was false.

allredj force-pushed the bugfix/retriever-arrays-arraylist branch from 681f353 to 901403d Compare August 27, 2019 09:33

allredj changed the title ~~Value retriever: Allow @nondetLength field to be false. [TG-9189]~~ [TG-9189] Value retriever: Allow @nondetLength field to be false. Aug 27, 2019

allredj commented Aug 27, 2019

View reviewed changes

smowton approved these changes Aug 27, 2019

View reviewed changes

allredj removed the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Aug 27, 2019

allredj merged commit 8f06fdf into develop Aug 27, 2019

allredj deleted the bugfix/retriever-arrays-arraylist branch August 27, 2019 17:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[TG-9189] Value retriever: Allow @nondetLength field to be false. #5043

[TG-9189] Value retriever: Allow @nondetLength field to be false. #5043

Uh oh!

allredj commented Aug 20, 2019

Uh oh!

allredj left a comment

Uh oh!

codecov-io commented Aug 20, 2019

Uh oh!

smowton Aug 20, 2019

Uh oh!

antlechner Aug 21, 2019

Uh oh!

antlechner left a comment

Uh oh!

antlechner Aug 21, 2019

Uh oh!

antlechner Aug 21, 2019 •

edited

Loading

Uh oh!

allredj Aug 21, 2019

Uh oh!

allredj Aug 27, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

antlechner Aug 21, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj commented Aug 22, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

[TG-9189] Value retriever: Allow @nondetLength field to be false. #5043

[TG-9189] Value retriever: Allow @nondetLength field to be false. #5043

Uh oh!

Conversation

allredj commented Aug 20, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Aug 20, 2019

Codecov Report

Uh oh!

smowton Aug 20, 2019

Choose a reason for hiding this comment

Uh oh!

antlechner Aug 21, 2019

Choose a reason for hiding this comment

Uh oh!

antlechner left a comment

Choose a reason for hiding this comment

Uh oh!

antlechner Aug 21, 2019

Choose a reason for hiding this comment

Uh oh!

antlechner Aug 21, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj Aug 21, 2019

Choose a reason for hiding this comment

Uh oh!

allredj Aug 27, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

antlechner Aug 21, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj commented Aug 22, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

antlechner Aug 21, 2019 •

edited

Loading