Refactor process_goto_program so that all tools use common processing code #5807
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
martin-cs
requested review from
chrisr-diffblue,
hannes-steffenhagen-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
|
Commit by commit reviewing strongly encouraged. |
tautschnig
approved these changes
Feb 8, 2021
martin-cs
force-pushed
the
refactor/process_goto_program
branch
from
8b9bfc3 to
b467993
Compare
martin-cs
force-pushed
the
refactor/process_goto_program
branch
3 times, most recently
from
f55e9a4 to
a8ca58a
Compare
added 15 commits
February 22, 2021 17:52
This should not alter observable behaviour.
…stent This will change the behaviour of goto-analyzer. I don't think it is currently tested so I suspect it was unable to handle inline assembler.
This does change the functionality quite substantially but strangely it only seems to affect one test, and that is syntactic rather than semantic. As with many of the other changes in this PR, I suspect this is swapping one lot of broken, untested functionality for another, slightly less broken but still not working lot of functionality.
The tests aren't really sufficient to tell whether this has an effect.
At the moment this code is dead and is only added to make the process_goto_program steps more similar. I will leave it to others to decide if this is a useful thing to have and add the required command line options and tests. Should not affect the behaviour of either tool.
This uncovered a bug in goto-analyzer where the options for goto-check are recognised but not actually parsed.
This adds some functionality for options that were previously allowed but silently ignored as they didn't make it from cmdline to goto_check.
This does add functionality but it is of the "used to be silently ignored but now sort of works or maybe breaks" kind.
In CBMC and goto-diff this is dead, in goto-analyze it preserves the existing behaviour. It is not 100% clear to me that the existing behaviour is useful or desirable but it is preserved as the point of this PR is not changing behaviour unless necessary.
Rewrite union converts union member access to byte extracts. This is (apparently) good for CBMC and goto-diff but it makes analysis harder for goto-analyzer. So to make them consistent we add an option which controls whether it is run or not. This is fixed in each tool but it takes us closer to common processing of goto programs.
goto-check makes use of the options assertions, assumptions, assert-to-assume and retain-trivial. These were handled to different degrees and in different way in each of the tools. This commit adds these options to the set of options in the *_GOTO_CHECK macros. This reduces the amount of duplication and parallel maintenance.
This was included in the options that goto-analyzer recognises and in its --help output but they were all silently ignored. This commit fixes that so that they are supported, making it more consistent with CBMC (and less inexplicable).
Strangely (or perhaps concerningly) this doesn't seem to break any of the regression tests.
In the case of goto-analyzer and goto-diff this should be dead code. In CBMC it reverses the order of string abstraction and non-det statics. It is conceivable that these two interact but this way around is probably better.
remove_skip and various other passes compute the updates so moving this should not effect the behaviour of the program.
added 4 commits
February 22, 2021 17:52
This requires cosmetic changes to a lot of unit tests.
This requires resolving a difference in the wording of a status message that breaks a lot of tests for function pointer removal.
martin-cs
force-pushed
the
refactor/process_goto_program
branch
from
a8ca58a to
e09efcb
Compare
|
@hannes-steffenhagen-diffblue and / or @peterschrammel any chance of a review? It looks big but commit by commit it is actually simple and should be easy to review quickly. |
Codecov Report
@@ Coverage Diff @@
## develop #5807 +/- ##
========================================
Coverage 72.88% 72.89%
========================================
Files 1422 1423 +1
Lines 154283 154229 -54
========================================
- Hits 112455 112426 -29
+ Misses 41828 41803 -25
Continue to review full report at Codecov.
|
peterschrammel
approved these changes
Feb 22, 2021
Co-authored-by: Peter Schrammel <[email protected]>
7 tasks
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.
*_parse_optionst::process_goto_programappears incbmc,goto-analyzeandgoto-diff(and maybe the Java tools, @peterschrammel @hannes-steffenhagen-diffblue who is handling these at the moment?) with slight variations, bugs, inconsistencies and omissions. This PR carefully makes them the same (so that we cangit-bisectto find any issues this might introduce) and then pulls the common code out into a helper function. This is another step towards a common format for goto-programs and stronger invariants.This does not break tested functionality but it will have an impact on untested functionality. Mostly, as far as I can see, it goes from 'silently doing the wrong thing' to 'maybe works, maybe breaks in an obvious way'. i consider this a net win.