Clean up in the value set API #4690

romainbrenguier · 2019-05-22T13:47:12Z

Several methods/members of value set are actually not used and should be deprecated to simplify the API.
The get_value_set interface in which the result has to be given as argument is also not clear and it is better to return the result.

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).
[na] 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-05-22T14:16:46Z

@romainbrenguier Various CI steps in Travis are failing.

tautschnig · 2019-05-22T14:27:21Z

src/pointer-analysis/value_set.h

  class object_map_dt
+    : public std::map<object_numberingt::number_type, offsett>


This basically is a revert of 3b5263f. We should have really good reasons if that's what should happen.

Ok I see. I will drop that commit for now and try to find a better solution

tautschnig · 2019-05-22T14:28:58Z

src/pointer-analysis/value_set.h

@@ -276,6 +277,7 @@ class value_sett
    const namespacet &ns) const;

  /// Appears to be unimplemented.
+  DEPRECATED(SINCE(2019, 05, 22, "Unimplemented"))
  expr_sett &get(const irep_idt &identifier, const std::string &suffix);


I think we can just remove what isn't even implemented.

I don't know. In test-gen there were cases of cpp files used instead of the cbmc ones which could add new implementation not existing in cbmc

smowton · 2019-05-22T14:31:01Z

@owen-jones-diffblue could you check if local_value_sett uses location_number?

smowton

Suggest dropping the std::map-inheriting commit, which is a straight revert of #919, for the reasons given in that PR

smowton · 2019-05-22T14:30:35Z

src/pointer-analysis/goto_program_dereference.h

  void
  get_value_set(const exprt &expr, value_setst::valuest &dest) const override;

+  std::list<exprt> get_value_set(const exprt &expr) const override;


If we're adding a new entry-point we probably shouldn't use std::list, there's no call for a doubly-linked list here AFAICT

but it is a list, and the fact that value_setst::valuest is a list is public, by writing value_setst::valuest we are just making it more complicated for the reader

I'm not suggesting valuest, I'm suggesting std::vector because that's the most performant C++ sequence container when you don't have a good reason for something else (e.g. deque or list)

romainbrenguier · 2019-05-22T15:47:44Z

@tautschnig @smowton here is a PR to go instead of the std::map inheritance #4694

owen-mc-diffblue · 2019-05-22T16:44:57Z

@smowton It does, but we can just add that field ourselves

romainbrenguier · 2019-05-24T09:28:14Z

actually it seems location_number is used by value_set_domain_templatet so I will have to drop that commit too...

romainbrenguier · 2019-05-24T14:23:32Z

@smowton I have now replace the use of list by vector

smowton · 2019-05-24T15:50:39Z

src/goto-symex/symex_dereference_state.h

@@ -34,9 +34,12 @@ class symex_dereference_statet:
  goto_symext::statet &state;
  const namespacet &ns;

+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))


vector returning

smowton · 2019-05-24T15:50:46Z

src/pointer-analysis/dereference_callback.h

@@ -29,9 +29,12 @@ class dereference_callbackt
 public:
  virtual ~dereference_callbackt() = default;

+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))


vector returning

smowton · 2019-05-24T15:51:19Z

src/pointer-analysis/value_sets.h

@@ -28,12 +28,19 @@ class value_setst
  typedef std::list<exprt> valuest;

  // this is not const to allow a lazy evaluation
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))


vector returning

romainbrenguier · 2019-05-29T06:39:33Z

@owen-jones-diffblue @smowton I've added a commit which gets rid of doxygen warning that were generated for this pull request, in case you want to have a look

tautschnig · 2019-05-30T08:10:36Z

@romainbrenguier Please rebase now that #4729 is in to make CI happy.

allredj

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

This avoids having to create a tmp expression and allows moving into the function.

This is unused

This is not implemented.

This is unused.

These return the computed value, which makes the information flow clearer in the program. We deprecate at the same time the functions from the previous version.

vectors are generally more efficient than list, unless we use concatenation or insertion which doesn't appear to be case here.

This prevents the macro from making doxyfile miss method definitions that are deprecated and automatically add the deprecated methods to the Deprecated List generated by doxygen

allredj

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

romainbrenguier requested review from chrisr-diffblue, kroening, martin-cs, owen-mc-diffblue, peterschrammel, smowton and tautschnig as code owners May 22, 2019 13:47

romainbrenguier force-pushed the clean-up/value-set branch from 501cf06 to 46ffcec Compare May 22, 2019 13:50

owen-mc-diffblue approved these changes May 22, 2019

View reviewed changes

tautschnig reviewed May 22, 2019

View reviewed changes

smowton suggested changes May 22, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/value-set branch from 46ffcec to 8265d1f Compare May 22, 2019 15:01

romainbrenguier force-pushed the clean-up/value-set branch 3 times, most recently from f015a95 to 1d13bfa Compare May 24, 2019 14:23

smowton approved these changes May 24, 2019

View reviewed changes

smowton reviewed May 24, 2019

View reviewed changes

tautschnig assigned romainbrenguier May 27, 2019

romainbrenguier force-pushed the clean-up/value-set branch 4 times, most recently from c138014 to 9b387f1 Compare May 28, 2019 14:52

romainbrenguier force-pushed the clean-up/value-set branch from 9b387f1 to a4b2eed Compare May 29, 2019 06:37

tautschnig added the Needs rebase label May 30, 2019

romainbrenguier force-pushed the clean-up/value-set branch from a4b2eed to 88cc5c5 Compare May 30, 2019 09:51

romainbrenguier removed the Needs rebase label May 30, 2019

romainbrenguier force-pushed the clean-up/value-set branch 2 times, most recently from 40b65af to 27f87e8 Compare May 31, 2019 06:18

allredj reviewed May 31, 2019

View reviewed changes

romainbrenguier added 7 commits June 3, 2019 09:19

get_value_set takes expr by copy

318d49a

This avoids having to create a tmp expression and allows moving into the function.

Deprecate offset_is_zero

b633d6d

This is unused

Deprecate value_sett::get

01dff41

This is not implemented.

Deprecate dynamic_object_id_sett

e1eb12e

This is unused.

Add versions of get_value_set returning a value

1e06eda

These return the computed value, which makes the information flow clearer in the program. We deprecate at the same time the functions from the previous version.

Use vector instead of list for get_value_set result

8d497eb

vectors are generally more efficient than list, unless we use concatenation or insertion which doesn't appear to be case here.

Predefine DEPRECATED macro in doxyfile

fa1412c

This prevents the macro from making doxyfile miss method definitions that are deprecated and automatically add the deprecated methods to the Deprecated List generated by doxygen

romainbrenguier force-pushed the clean-up/value-set branch from 27f87e8 to fa1412c Compare June 3, 2019 08:19

allredj reviewed Jun 3, 2019

View reviewed changes

tautschnig merged commit f175f75 into diffblue:develop Jun 3, 2019

romainbrenguier deleted the clean-up/value-set branch June 3, 2019 10:13

		class object_map_dt
		: public std::map<object_numberingt::number_type, offsett>

Clean up in the value set API #4690

Clean up in the value set API #4690

Uh oh!

Conversation

romainbrenguier commented May 22, 2019

Uh oh!

tautschnig commented May 22, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented May 22, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented May 22, 2019

Uh oh!

owen-mc-diffblue commented May 22, 2019

Uh oh!

romainbrenguier commented May 24, 2019

Uh oh!

romainbrenguier commented May 24, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented May 29, 2019

Uh oh!

tautschnig commented May 30, 2019

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!

Uh oh!