Fix for nondet replacement on a direct return pre-remove returns #2263
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JohnDumbell
requested review from
cesaro,
mgudemann,
peterschrammel,
smowton and
thk123
as code owners
JohnDumbell
force-pushed
the
bugfix/nondet_direct_return
branch
from
af50e42 to
d819de9
Compare
smowton
reviewed
Jun 1, 2018
|
|
||
| goto_model_functiont model_function( | ||
| symbol_table, functions, function_name, goto_function); | ||
| // Currently causes an abort, needs to be re-enabled when logic is fixed. |
There was a problem hiding this comment.
Elaborate briefly here, or reference a Github issue number.
smowton
reviewed
Jun 1, 2018
JohnDumbell
force-pushed
the
bugfix/nondet_direct_return
branch
from
d819de9 to
0d9d23f
Compare
|
Created #2281 just to chronicle the issue I saw and added a link to the failing tests. |
JohnDumbell
force-pushed
the
bugfix/nondet_direct_return
branch
2 times, most recently
from
01be3da to
8093c2d
Compare
smowton
approved these changes
Jun 18, 2018
owen-mc-diffblue
approved these changes
Jun 18, 2018
| inserted_expr.set_nullable( | ||
| instr_info.get_nullable_type() == | ||
| nondet_instruction_infot::is_nullablet::TRUE); | ||
| target_instruction->code = code_assignt(nondet_var, inserted_expr); |
There was a problem hiding this comment.
Should you call target_instruction->code.add_source_location()?
JohnDumbell
force-pushed
the
bugfix/nondet_direct_return
branch
from
8093c2d to
03afe96
Compare
JohnDumbell
force-pushed
the
bugfix/nondet_direct_return
branch
from
03afe96 to
6082ab8
Compare
allredj
reviewed
Jun 19, 2018
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 6082ab8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76670784
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- 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).
allredj
reviewed
Jun 20, 2018
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 6082ab8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76670784
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- 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).
JohnDumbell
force-pushed
the
bugfix/nondet_direct_return
branch
from
6082ab8 to
8c62e85
Compare
allredj
reviewed
Jun 25, 2018
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 8c62e85).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77232454
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- 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).
If remove returns hasn't been run and the nondet method call was a direct return - return nondetWithoutNull() - an assertion was hit because it couldn't find the destination assignment to add the nondet value too. This change just adds that particular situation in, saying if we can't find an assignment it's likely to be a return and then attempts to look for that. The logic is also very slightly modified to replace the code of the target instruction instead of destroying it, creating a new one and inserting that directly afterwards.
JohnDumbell
force-pushed
the
bugfix/nondet_direct_return
branch
from
8c62e85 to
91e8b89
Compare
allredj
reviewed
Jun 26, 2018
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 91e8b89).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77364460
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Aug 22, 2018
6fd77f4 Merge pull request diffblue#2472 from smowton/smowton/fix/nondet-stringbuilders 5423ea4 Merge pull request diffblue#2488 from polgreen/common_call_graph_funcs a2a5662 Merge pull request diffblue#2263 from JohnDumbell/bugfix/nondet_direct_return bbf0d02 Merge pull request diffblue#2482 from antlechner/antonia/direct-children-of-class c982c21 Merge pull request diffblue#2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix 8e7b6e7 Java object factory: initialize AbstractStringBuilder-derived types correctly 9af7ef1 Add tests for new class_hierarchy_grapht functions 79cad15 Fix existing class hierarchy test syntax dbac316 Add documentation to class_hierarchyt 3ecac30 Move non-graph function below graph functions 4badd8f Add useful functions to class_hierarchy_grapht 610467e Merge pull request diffblue#2480 from smowton/smowton/admin/graph-unit-tests 2431ac0 Doxygen formatting for dependence_graph test includes 19a1ceb factor out common call graph unit test functions into header deff59d Add tests for grapht::make_chordal and grapht::connected_subgraphs e94208f Merge pull request diffblue#2428 from tautschnig/vs-ref d00d833 Fix: several grapht functions were uncompilable if ever called b9014de Merge pull request diffblue#2381 from polgreen/depth_limited_search 7c767ab Merge pull request diffblue#2485 from tautschnig/vs-unreachable da76500 JBMC: Fixed asymmetry between synchronized blocks and methods. 5918640 Merge pull request diffblue#2487 from JohnDumbell/bugfix/add_java_load_class d65c655 Merge pull request diffblue#2484 from tautschnig/vs-printf 91e8b89 Fix for nondet replacement on a direct return (pre-remove returns) 904132d unit tests for depth limited search on call graph 2c76d0d call graph helper interface to depth limited search 64fdb9b depht limited search for grapht e708bfb Adds --java-load-class to tests that require it 6665c69 Remove unreachable instructions 6e4d5a7 printf does not and should not have a left-hand side 2111f7c Merge pull request diffblue#2475 from tautschnig/vs-wmm 6566d10 Merge pull request diffblue#2469 from tautschnig/vs-string2 3703974 Merge pull request diffblue#2477 from tautschnig/vs-string-abstraction cf797da Merge pull request diffblue#2473 from tautschnig/vs-update c07a09b Merge pull request diffblue#2476 from tautschnig/vs-cex e504e80 Remove unused parameter in string abstraction 4d88b98 Remove unused parameter in counterexample beautification 888f168 Remove unused parameter from update_scores 461754d Remove unused parameters in goto-instrument/wmm 93300aa Use string2unsigned when reading/expecting an unsigned 1a7033a String refinement: Take a reference to avoid copy git-subtree-dir: cbmc git-subtree-split: 6fd77f4
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
As a quick summary: if remove returns hasn't been run, there was a specific situation to do with direct returns in which a nondet wasn't being detected when it should've, which this fixes up.
More interestingly, while testing this I found out there are a variety of other situations where we can't work out precisely where the nondet statement should be inserted, specifically around any situation where the value moves between variables, like this:
temp0 = CProver.nonDetInt()
temp1 = Integer.unbox(temp0)
return_variable = temp1
The above will hit an assertion because the variable we're interested in is actually temp1, while we're searching for temp0 and not finding any assignments/returns attributed to that. I haven't fixed this (and other more complicated situations) because I felt repeated band-aids for each condition as they came up wasn't the best approach. I'm not sure what would be the best approach mind, but felt it was worth mentioning.