Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Do not generate redundant if statements in assert expansions #974

Merged
merged 4 commits into from
Apr 16, 2018
Merged

Do not generate redundant if statements in assert expansions #974

merged 4 commits into from
Apr 16, 2018

Conversation

tautschnig
Copy link
Collaborator

No description provided.

@tautschnig
Copy link
Collaborator Author

I am now including the test proposed in #726.

@tautschnig tautschnig force-pushed the fix-assert-encoding branch 2 times, most recently from b3ef844 to 2f9b822 Compare May 26, 2017 18:06
@kroening
Copy link
Member

I am wondering whether this might wreck structural coverage metrics?

@tautschnig
Copy link
Collaborator Author

@kroening: I would hope it doesn't, but maybe I'm missing something. (I don't think we expected to have "IF ..." generated from assert statements, but I may well be wrong.)

@tautschnig tautschnig force-pushed the fix-assert-encoding branch from 2f9b822 to f1e9c8e Compare May 29, 2017 16:21
@tautschnig tautschnig force-pushed the fix-assert-encoding branch from f1e9c8e to 549d8d5 Compare June 8, 2017 08:56
@thk123 thk123 mentioned this pull request Jun 26, 2017
Closed
@tautschnig tautschnig force-pushed the fix-assert-encoding branch from 549d8d5 to fef73cb Compare August 7, 2017 12:33
@tautschnig tautschnig self-assigned this Aug 20, 2017
@tautschnig tautschnig changed the base branch from master to develop August 22, 2017 12:23
@tautschnig tautschnig mentioned this pull request Jan 8, 2018
Closed
@tautschnig tautschnig force-pushed the fix-assert-encoding branch from fef73cb to 4bb1b1e Compare January 8, 2018 15:53
@tautschnig tautschnig force-pushed the fix-assert-encoding branch 2 times, most recently from cda52a8 to 3ea0760 Compare January 8, 2018 18:52
smowton
smowton reviewed Jan 9, 2018
View reviewed changes
src/goto-programs/goto_clean_expr.cpp Outdated
@@ -260,13 +260,15 @@ void goto_convertt::clean_expr(
// preserve the expressions for possible later checks
if(if_expr.true_case().is_not_nil())
{
code_expressiont code_expression(if_expr.true_case());
code_expressiont code_expression(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess this is C-style (void)x to mark something "used"? If so perhaps say that in the comment.

src/goto-programs/goto_convert.cpp
// a special case for C libraries that use
// (void)((cond) || (assert(0),0))
if(
is_empty(false_case) && true_case.instructions.size() == 2 &&
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there any reason to restrict ourselves to two instructions here? Could we simply say "if(x) { assert(false); ... } --> assert(!x)", since the rest of the true-case is dead code? Also, why only consider the true case?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's only dead code if none of the instruction has a label that could be jumped to.

@tautschnig tautschnig force-pushed the fix-assert-encoding branch 2 times, most recently from ea0a679 to 9fbf6ff Compare January 9, 2018 22:36
@tautschnig tautschnig force-pushed the fix-assert-encoding branch from 9fbf6ff to 4122a28 Compare April 15, 2018 23:15
@tautschnig
Copy link
Collaborator Author

@kroening What would a test look like that tells whether coverage metrics have been impacted? @peterschrammel @smowton Would it be possible to have a TG bump for this one?

@smowton
Copy link
Contributor

smowton commented Apr 16, 2018

TG bump: https://github.com/diffblue/test-gen/pull/1709

@smowton
Copy link
Contributor

smowton commented Apr 16, 2018

TG bump passing CI.

@tautschnig tautschnig merged commit 49ad1bd into diffblue:develop Apr 16, 2018
@tautschnig tautschnig deleted the fix-assert-encoding branch April 16, 2018 16:27
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
@smowton
Squashed 'cbmc/' changes from 768e8a6..ad62682
7420f4a 
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@smowton smowton smowton approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

Assignees

@smowton smowton

@kroening kroening

@peterschrammel peterschrammel

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@tautschnig @kroening @smowton @peterschrammel