introduce protected_exprt #3855

kroening · 2019-01-19T17:36:52Z

This will serve as the interface that we aspire exprt to offer; in
particular, access to opX is protected.

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.
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

thk123

This presumably requires a TG bump before merging - will create to see how much additional work is required.

thk123 · 2019-01-21T11:57:30Z

src/pointer-analysis/value_set_fi.cpp

@@ -870,8 +870,8 @@ void value_set_fit::get_reference_set_sharing_rec(
        insert(dest, exprt(ID_unknown, expr.type()));
      else
      {
-        index_exprt index_expr(
-          object, from_integer(0, index_type()), expr.type());
+        exprt index_expr =


❓ Why remove the type from lhs? Because we call make_typecast which makes this not an index_exprt 😱 -> ⛏️ don't change the type, instead create a typecast from the index_exprt

#3856 will fix this!

thk123 · 2019-01-21T11:59:11Z

src/util/expr.h

+/// This API will eventually replace exprt.
+class protected_exprt : public exprt
+{
+protected:


❓ Would it make more sense to use protected inheritance? I assume the answer is no as there remains calls to other methods, that have not been removed, but perhaps given this direction of travel it would making more sense to using them into the public section? (I think you can do this, but I have not actually tried).

This would circumvent the need for this class entirely and just update the classes that inherit from exprt to protected extend it and in fact allow for explicitly identifying the classes that use the wrong interface.

There are a lot of classes inheriting from exprt; furthermore, the interface of exprt should change as well, once we are there.

thk123 · 2019-01-21T12:02:20Z

src/util/expr.h

@@ -318,6 +318,40 @@ class exprt:public irept
  const_unique_depth_iteratort unique_depth_cend() const;
 };

+/// Protected class for all expressions.
+/// This API will eventually replace exprt.
+class protected_exprt : public exprt


⛏️ I slightly worry about the name, in general, X_exprt means an expression representing an AST node of type X. I guess protected is never a node of a C/C++/Java AST, but perhaps this should be called expr_protected or expr_api_protected to indicate that this is an internal fudge rather than an actual GOTO thing.

thk123 · 2019-01-21T12:08:35Z

Ah this doesn't yet compile on CBMC - will hold off on the bump front for now.

allredj

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

thk123 · 2019-01-24T09:16:28Z

@kroening This still isn't compiling on cbmc yet:

value_set_fi.cpp:858:48: error: within this context
           index_expr.make_typecast(array.type());

So will hold off on the bump for now.

tautschnig · 2019-01-24T13:33:29Z

src/util/expr.h

@@ -319,6 +319,40 @@ class exprt:public irept
  const_unique_depth_iteratort unique_depth_cend() const;
 };

+/// Protected class for all expressions.


What is a "protected" class? Who is being protected? From what risks are they being shielded? When should anyone use it? I think this comment needs to be reworded.

I'm a bit confused, an intermittent version had more elaborate documentation. Do a git reflog to look at those?

tautschnig · 2019-01-24T13:34:27Z

src/util/expr.h

+  DEPRECATED("use protected_exprt(id, type) instead")
+  explicit protected_exprt(const irep_idt &_id) : exprt(_id)
+  {
+  }


It seems rather weird that newly introduced code would be deprecated? Can we just not have these?

sure, removed

Back again?

tautschnig · 2019-01-24T13:35:26Z

src/util/expr.h

+  using exprt::op3;
+  // using exprt::find;
+  // using exprt::get;
+  // using exprt::set;


Adding commented-out code without comments is just raising questions, but not providing answers.

sure, removed

tautschnig · 2019-01-24T13:36:32Z

src/util/pointer_offset_size.cpp

-  const typet &type=
-    static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
+  // need to cast down to access 'find'
+  const auto &expr_as_irep = static_cast<const irept &>(expr);


I don't think that's an improvement?

allredj

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

tautschnig · 2019-01-24T23:21:14Z

src/util/pointer_offset_size.cpp

+  const auto &expr_as_irep = static_cast<const irept &>(expr);
+
+  const typet &type =
+    static_cast<const typet &>(expr_as_irep.find(ID_C_c_sizeof_type));


Is this still necessary, given .find is no longer protected?

tautschnig · 2019-01-24T23:23:52Z

src/util/std_expr.h

+  using exprt::op0;
+  using exprt::op1;
+  using exprt::op2;
+  using exprt::op3;


Should this really be done? A multi_ary_exprt can, but need not have this many operands? For an unidentified multi_ary_exprt the caller should always use .operands() and just operate on that data structure.

replaced by ranged-checked opX().

hannes-steffenhagen-diffblue

🤔

hannes-steffenhagen-diffblue · 2019-01-25T10:57:46Z

src/util/expr.h

@@ -319,6 +319,29 @@ class exprt:public irept
  const_unique_depth_iteratort unique_depth_cend() const;
 };

+/// Class for expressions that offers a restriction of the API
+/// offered by exprt. Notably, access to non-type-safe methods such
+/// as opX() is protected.


Does that mean that exprt subclasses that so far only have these as their API will get updated (e.g. classes like typecast_exprt that only have op0 rather than a named accessor?).

Also, if we're already going to do an API do-over, why make the "new" expr inherit from irept at all, rather than have an irep as a protected field or something?

tautschnig

It looks like some earlier version has been restored? Might be worth looking at the commits the GitHub lists or going for git reflog.

tautschnig · 2019-01-25T23:01:00Z

src/util/expr.h

@@ -319,6 +319,40 @@ class exprt:public irept
  const_unique_depth_iteratort unique_depth_cend() const;
 };

+/// Protected class for all expressions.


I'm a bit confused, an intermittent version had more elaborate documentation. Do a git reflog to look at those?

tautschnig · 2019-01-25T23:01:29Z

src/util/expr.h

+  DEPRECATED("use protected_exprt(id, type) instead")
+  explicit protected_exprt(const irep_idt &_id) : exprt(_id)
+  {
+  }


Back again?

This will enable protecting exprt::opX()

make_typecast isn't type safe; typecast_exprt::conditional_cast is.

exprt::make_typecast() isn't type safe

This prevents out-of-bound accesses to operands().

This will serve as the interface that we aspire exprt to offer; in particular, access to opX is protected.

kroening · 2019-01-26T12:13:11Z

Back again!

tautschnig · 2019-01-26T12:24:50Z

src/util/std_expr.h

+  // make op0 and op1 public
+  using exprt::op0;
+  using exprt::op1;
+
  const exprt &op2() const = delete;
  exprt &op2() = delete;
  const exprt &op3() const = delete;


Is this still needed?

Yes, there are still too many users -- but I'd say that it makes sense to work towards removing these two lines.

(But at least it's not dangerous to use them).

I don't understand - these are being deleted, even though protected_exprt makes them unavailable anyway.

Ah, ok, the "this" was unclear.

The deletion of op2() and op3() is indeed no longer needed.

allredj

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

martin-cs

The changes to bits of code I am responsible for are fine. I will leave it to others to have opinions on the exact API. Being cleaner about the use of exprts / irepts is a good thing in general.

peterschrammel · 2019-01-28T22:51:53Z

src/util/expr.h

@@ -319,6 +319,28 @@ class exprt:public irept
  const_unique_depth_iteratort unique_depth_cend() const;
 };

+/// Base class for all expressions. This protects low-level methods in
+/// exprt that are not type safe. Depcrecated constructors are removed.


Typo in deprecated

kroening added cleanup work in progress do not review labels Jan 19, 2019

kroening requested review from allredj, cesaro, chrisr-diffblue, cristina-david, martin-cs, NathanJPhillips, peterschrammel, pkesseli, romainbrenguier, smowton, tautschnig and thk123 as code owners January 19, 2019 17:36

kroening force-pushed the protected_exprt branch 2 times, most recently from cd7d05d to 6947aaa Compare January 19, 2019 21:26

allredj reviewed Jan 19, 2019

View reviewed changes

thk123 reviewed Jan 21, 2019

View reviewed changes

kroening force-pushed the protected_exprt branch 3 times, most recently from 5d451cc to a9a44af Compare January 24, 2019 08:18

kroening removed do not review work in progress labels Jan 24, 2019

kroening assigned thk123 Jan 24, 2019

allredj reviewed Jan 24, 2019

View reviewed changes

thk123 assigned kroening and unassigned thk123 Jan 24, 2019

tautschnig reviewed Jan 24, 2019

View reviewed changes

kroening force-pushed the protected_exprt branch 2 times, most recently from 768c17e to f9368aa Compare January 24, 2019 15:00

allredj reviewed Jan 24, 2019

View reviewed changes

kroening force-pushed the protected_exprt branch from f9368aa to d9ae0f7 Compare January 24, 2019 18:46

allredj reviewed Jan 24, 2019

View reviewed changes

tautschnig reviewed Jan 24, 2019

View reviewed changes

hannes-steffenhagen-diffblue reviewed Jan 25, 2019

View reviewed changes

kroening force-pushed the protected_exprt branch from d9ae0f7 to e8a1037 Compare January 25, 2019 21:57

tautschnig requested changes Jan 25, 2019

View reviewed changes

Daniel Kroening added 2 commits January 26, 2019 11:53

avoid direct access to exprt::op0()

1280010

This will enable protecting exprt::opX()

use conditional_cast instead of make_typecast

6c14669

make_typecast isn't type safe; typecast_exprt::conditional_cast is.

kroening force-pushed the protected_exprt branch from e8a1037 to 431eb3e Compare January 26, 2019 12:02

Daniel Kroening added 3 commits January 26, 2019 12:09

replace exprt::make_typecast() by typecast_exprt()

39d38f1

exprt::make_typecast() isn't type safe

multi_ary_exprt::opX with precondtion

adb0533

This prevents out-of-bound accesses to operands().

introduce expr_protectedt

a48f855

This will serve as the interface that we aspire exprt to offer; in particular, access to opX is protected.

kroening force-pushed the protected_exprt branch from 431eb3e to a48f855 Compare January 26, 2019 12:13

tautschnig approved these changes Jan 26, 2019

View reviewed changes

allredj reviewed Jan 26, 2019

View reviewed changes

kroening assigned peterschrammel and unassigned kroening Jan 27, 2019

martin-cs approved these changes Jan 28, 2019

View reviewed changes

peterschrammel approved these changes Jan 28, 2019

View reviewed changes

peterschrammel assigned kroening and unassigned peterschrammel Jan 28, 2019

kroening merged commit e4af3bf into develop Jan 29, 2019

kroening deleted the protected_exprt branch January 29, 2019 09:21

introduce protected_exprt #3855

introduce protected_exprt #3855

Conversation

kroening commented Jan 19, 2019

allredj left a comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Jan 21, 2019

allredj left a comment

Choose a reason for hiding this comment

thk123 commented Jan 24, 2019

tautschnig Jan 24, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kroening commented Jan 26, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig Jan 24, 2019 •

edited

Loading