Clean-up use of guards #4188

romainbrenguier · 2019-02-14T14:29:19Z

In some places, guards are passed around but never really used, in other places they can be replaced by expressions.

Each commit message has a non-empty body, explaining why the change was made.
[na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] 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.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-02-14T14:35:07Z

src/pointer-analysis/goto_program_dereference.h

@@ -19,6 +19,8 @@ Author: Daniel Kroening, [email protected]
 #include "value_sets.h"
 #include "value_set_dereference.h"

+class guardt;


I'm not exactly sure about the order of the commits here, but at the very end this shouldn't be needed anymore at all I think?

It is still used in some unused deprecated function and I'm not sure of what to do with all these functions (most of the code in this class is unused).

Remove the cruft. git revert is not all that hard.

dereference is not overridden, we add final to value_set_dereferencet to be sure of that. Calls to virtual functions are slow, and in general it is better to avoid virtual recursive functions (like derefence was).

This argument was never actually used.

This is never actually used. This allows to remove a lot of useless operations.

The include statement is not usefull anymore, as the usage of guard disappeared from this file.

danpoe

LGTM

danpoe · 2019-02-14T16:21:28Z

src/goto-instrument/rw_set.cpp

  const std::string &suffix,
-  const guardt &guard)
+  const exprt::operandst &guard)


Can we rename the guard parameters maybe to guard_conjuncts? Otherwise it might be surprising to find a parameter named guard of type exprt::operandst.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 18f4ba5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100961989
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: af6bd9c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100962569
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

This was not making really use of guardt, since no guardt specific operations where performed, but instead just represents a conjunction. We replace that by a list of expressions and do the conjunction when needed. This avoids dependencies on guardt.

A lot of code in goto_program_dereference was deprecated, commented or documented as unused. This commit remove these parts of the code.

allredj

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

romainbrenguier requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners February 14, 2019 14:29

romainbrenguier mentioned this pull request Feb 14, 2019

Use BDDs for encoding symex guards #3730

Merged

5 tasks

tautschnig approved these changes Feb 14, 2019

View reviewed changes

tautschnig assigned smowton, peterschrammel, danpoe, chrisr-diffblue and hannes-steffenhagen-diffblue Feb 14, 2019

romainbrenguier force-pushed the clean-up/unused-guards branch from 78af785 to 18f4ba5 Compare February 14, 2019 15:01

romainbrenguier added 4 commits February 14, 2019 15:06

Make dereference non-virtual

e97fa0c

dereference is not overridden, we add final to value_set_dereferencet to be sure of that. Calls to virtual functions are slow, and in general it is better to avoid virtual recursive functions (like derefence was).

Remove unused guard argument from dereference

e1e2c11

This argument was never actually used.

Remove unused guard argument of dereference_rec

919ae48

This is never actually used. This allows to remove a lot of useless operations.

Remove unused include of guard.h

560f0df

The include statement is not usefull anymore, as the usage of guard disappeared from this file.

romainbrenguier force-pushed the clean-up/unused-guards branch 2 times, most recently from af6bd9c to c459861 Compare February 14, 2019 15:15

danpoe approved these changes Feb 14, 2019

View reviewed changes

allredj reviewed Feb 14, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/unused-guards branch from c459861 to ea7e631 Compare February 15, 2019 06:50

chrisr-diffblue approved these changes Feb 15, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/unused-guards branch from ea7e631 to 8dcbfc3 Compare February 15, 2019 09:13

romainbrenguier added 2 commits February 15, 2019 09:52

Remove unused code from goto_program_dereference

cee38c5

A lot of code in goto_program_dereference was deprecated, commented or documented as unused. This commit remove these parts of the code.

romainbrenguier force-pushed the clean-up/unused-guards branch from 8dcbfc3 to cee38c5 Compare February 15, 2019 09:52

allredj reviewed Feb 15, 2019

View reviewed changes

romainbrenguier merged commit 6406ee1 into diffblue:develop Feb 15, 2019

romainbrenguier deleted the clean-up/unused-guards branch February 15, 2019 11:07

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Clean-up use of guards #4188

Clean-up use of guards #4188

romainbrenguier commented Feb 14, 2019

tautschnig Feb 14, 2019

romainbrenguier Feb 14, 2019

tautschnig Feb 14, 2019

danpoe left a comment

danpoe Feb 14, 2019

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

Clean-up use of guards #4188

Clean-up use of guards #4188

Conversation

romainbrenguier commented Feb 14, 2019

tautschnig Feb 14, 2019

Choose a reason for hiding this comment

romainbrenguier Feb 14, 2019

Choose a reason for hiding this comment

tautschnig Feb 14, 2019

Choose a reason for hiding this comment

danpoe left a comment

Choose a reason for hiding this comment

danpoe Feb 14, 2019

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment