avoid direct access to exprt::opX #3264

kroening · 2018-11-03T17:06:09Z

Rationale: accesses to exprt::opX can be memory safety violations; it's
better to cast to higher type, and then use the named access methods.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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.
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: f8dfd36).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90167415
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.

src/goto-symex/goto_symex_state.cpp

tautschnig · 2018-11-04T18:46:31Z

src/goto-symex/goto_symex_state.cpp

+    return check_renaming_l1(
+             to_index_expr(to_address_of_expr(expr).object()).array()) ||
+           check_renaming(
+             to_index_expr(to_address_of_expr(expr).object()).index());


Actually this code should be restructured to do the to_address_of_expr just once as it isn't zero cost.

src/goto-symex/symex_goto.cpp

tautschnig · 2018-11-04T18:50:11Z

src/util/json_expr.cpp

        // try to simplify the constant pointer
-        return simplify_json_expr(src.op0(), ns);
+        return simplify_json_expr(to_unary_expr(src).op0(), ns);


Please add braces to improve readability. And use .op() instead of .op0()

tautschnig · 2018-11-04T18:53:17Z

src/util/json_expr.cpp

+        (value != std::string(value.size(), '0') ||
+         !config.ansi_c.NULL_is_zero) &&
+        src.operands().size() == 1 &&
+        to_unary_expr(src).op0().id() != ID_constant)


Should be .op()

tautschnig · 2018-11-04T18:55:17Z

src/util/ssa_expr.cpp

-          expr.id()==ID_index)
-    return can_build_identifier(expr.op0());
+  else if(expr.id() == ID_member)
+    return can_build_identifier(to_member_expr(expr).struct_op());


Should be .compound() instead of .struct_op()

src/util/std_code.cpp

tautschnig · 2018-11-05T09:36:06Z

src/util/json_expr.cpp

+        // remove typecast on NULL
+        (simpl_expr.id() == ID_constant &&
+         simpl_expr.type().id() == ID_pointer &&
+         to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))


Please add braces below.

tautschnig · 2018-11-05T09:39:36Z

src/goto-symex/goto_symex_state.cpp

+    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
+    return check_renaming_l1(index_expr.array()) ||
+           check_renaming(index_expr.index());
+  }


I believe this part still needs further work to introduce something along the lines of:

if(expr.id() == ID_address_of) { const exprt &object = to_address_of(expr).object(); if(object.id() == ID_symbol) { ... } else if(object.id() == ID_index) { ... } } if(expr.id() == ID_symbol) // replacing the else if { ...

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: b5488f0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90241829
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 · 2018-11-05T16:24:23Z

I am quite confused by the complaints by clang-format, those seem rather unrelated to the changes. @kroening, could you please rebase?

Rationale: accesses to exprt::opX can be memory safety violations; it's better to cast to higher type, and then use the named access methods.

allredj

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

kroening added the cleanup label Nov 3, 2018

kroening assigned tautschnig Nov 3, 2018

kroening requested a review from tautschnig November 3, 2018 17:06

kroening requested review from peterschrammel, pkesseli and smowton as code owners November 3, 2018 17:06

allredj reviewed Nov 3, 2018

View reviewed changes

tautschnig reviewed Nov 4, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Nov 4, 2018

kroening force-pushed the exprt_opX_accesses branch from f8dfd36 to b5488f0 Compare November 5, 2018 09:04

kroening assigned tautschnig and unassigned kroening Nov 5, 2018

tautschnig reviewed Nov 5, 2018

View reviewed changes

allredj reviewed Nov 5, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Nov 5, 2018

tautschnig approved these changes Nov 5, 2018

View reviewed changes

kroening force-pushed the exprt_opX_accesses branch from b5488f0 to 6515c3a Compare November 5, 2018 14:30

avoid direct access to exprt::opX

d6603d3

Rationale: accesses to exprt::opX can be memory safety violations; it's better to cast to higher type, and then use the named access methods.

kroening force-pushed the exprt_opX_accesses branch from 6515c3a to d6603d3 Compare November 5, 2018 17:13

allredj reviewed Nov 5, 2018

View reviewed changes

tautschnig merged commit 27742dd into develop Nov 5, 2018

tautschnig deleted the exprt_opX_accesses branch November 5, 2018 19:09

avoid direct access to exprt::opX #3264

avoid direct access to exprt::opX #3264

Uh oh!

Conversation

kroening commented Nov 3, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Nov 5, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!