fix exprt::opX() accesses in cpp/ #4984

kroening · 2019-08-04T16:19:46Z

This improves type safety.

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.
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.

tautschnig

Various requests for somewhat minor changes.

tautschnig · 2019-08-04T16:30:31Z

src/cpp/cpp_constructor.cpp

-    side_effect_expr_function_callt &func_ini=
-      to_side_effect_expr_function_call(initializer.op0());
+    side_effect_expr_function_callt &func_ini =
+      to_side_effect_expr_function_call(to_unary_expr(initializer).op());


This seems wrong: we above assert that it's a statement expression.

The side_effect_expr_function_call is the operand of the statement expression.

Ah, sorry, my comment was unclear: I think using to_unary_expr on something that actually is a codet seems wrong (even when the type system currently permits it).

Now using side_effect_expr_statement_expressiont

src/cpp/cpp_typecheck_code.cpp

tautschnig · 2019-08-04T16:34:59Z

src/cpp/cpp_typecheck_code.cpp

-    assert(decl.op0().op0().id()==ID_symbol);
-    value = decl.op0().op0();
+    DATA_INVARIANT(
+      to_unary_expr(decl).op().op0().id() == ID_symbol,


How do we know that the .op0() is safe here?

added a check

src/cpp/cpp_typecheck_compound_type.cpp

tautschnig · 2019-08-04T16:38:31Z

src/cpp/cpp_typecheck_constructor.cpp

-  assign.copy_to_operands(op0.as_expr());
-  assign.op0().add_source_location() = source_location;
-  assign.copy_to_operands(op1);
+  assign.copy_to_operands(op0.as_expr(), op1);


Could use the side_effect_exprt constructor that also takes operands?

indeed, done

tautschnig · 2019-08-04T16:39:16Z

src/cpp/cpp_typecheck_constructor.cpp

-  assign.op0().add_source_location() = source_location;
-  assign.copy_to_operands(op1);
+  assign.copy_to_operands(op0.as_expr(), op1);
+  to_binary_expr(assign).op0().add_source_location() = source_location;


Doing to_binary_expr on a side_effect_exprt feels very wrong.

now uses side_effect_expr_assignt

tautschnig · 2019-08-04T16:40:22Z

src/cpp/cpp_typecheck_constructor.cpp

-  assign.op1().add_source_location() = source_location;
+
+  to_binary_expr(assign).op0().add_source_location() = source_location;
+  to_binary_expr(assign).op1().add_source_location() = source_location;


As above: use the side_effect_exprt constructor that takes operands, and use some other approach instead of applying to_binary_expr on a side_effect_exprt.

fixed as above

tautschnig · 2019-08-04T16:41:19Z

src/cpp/cpp_typecheck_constructor.cpp

@@ -295,7 +294,7 @@ void cpp_typecheckt::default_assignop(
  cpctor.operands().push_back(exprt(ID_cpp_declarator));
  cpctor.add_source_location()=source_location;

-  cpp_declaratort &declarator=(cpp_declaratort&) cpctor.op0();
+  cpp_declaratort &declarator = (cpp_declaratort &)cpctor.op0();


Looks like a whitespace-only change, but maybe we can actually get rid of the C-style cast?

tautschnig · 2019-08-04T16:42:15Z

src/cpp/cpp_typecheck_conversions.cpp

-          assert(returned_value.id()==ID_dereference &&
-                 is_reference(returned_value.op0().type()));
+          assert(
+            returned_value.id() == ID_dereference &&


Seems unnecessary as the second conjunct now uses to_dereference_expr.

tautschnig · 2019-08-04T16:44:38Z

src/cpp/expr2cpp.cpp

-  assert(src.operands().size()==2);
-  return convert(src.op0())+"["+convert(src.op1())+"]";
+  return convert(to_binary_expr(src).op0()) + "[" +
+         convert(to_binary_expr(src).op1()) + "]";


Could we use to_extractbit_expr instead?

allredj

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

codecov-io · 2019-08-05T08:29:45Z

Codecov Report

Merging #4984 into develop will decrease coverage by <.01%.
The diff coverage is 71.07%.

@@             Coverage Diff             @@
##           develop    #4984      +/-   ##
===========================================
- Coverage    69.56%   69.56%   -0.01%     
===========================================
  Files         1314     1314              
  Lines       108922   108945      +23     
===========================================
+ Hits         75776    75786      +10     
- Misses       33146    33159      +13

Impacted Files	Coverage Δ
src/cpp/cpp_typecheck.cpp	`79.13% <ø> (ø)`	⬆️
src/cpp/cpp_typecheck_conversions.cpp	`70.95% <0%> (-0.72%)`	⬇️
src/cpp/expr2cpp.cpp	`42.37% <0%> (-0.49%)`	⬇️
src/cpp/cpp_static_assert.h	`100% <100%> (ø)`	⬆️
src/cpp/cpp_typecheck_constructor.cpp	`83.33% <100%> (+0.11%)`	⬆️
src/cpp/cpp_typecheck_function.cpp	`94.44% <100%> (+0.21%)`	⬆️
src/cpp/cpp_constructor.cpp	`69.07% <100%> (+0.32%)`	⬆️
src/cpp/cpp_typecheck_resolve.cpp	`65.61% <100%> (+0.04%)`	⬆️
src/cpp/cpp_typecheck_fargs.cpp	`86.66% <100%> (ø)`	⬆️
src/cpp/cpp_typecheck_compound_type.cpp	`85.64% <100%> (ø)`	⬆️
... and 5 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b8302cf...e8c4be1. Read the comment docs.

allredj

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

allredj

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

allredj

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

allredj

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

tautschnig

Looks good except for one new issue that needs to be fixed.

tautschnig · 2019-10-18T21:13:42Z

src/cpp/cpp_typecheck_code.cpp

+    DATA_INVARIANT(
+      to_code_decl(to_code(to_unary_expr(decl).op())).symbol().id() ==
+        ID_symbol,
+      "declaration must have symbol as operand");


This DATA_INVARIANT cannot fail, because to_code_decl will already fail its code_declt::check(code);

This improves type safety.

allredj

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

kroening added the cleanup label Aug 4, 2019

kroening requested review from peterschrammel and tautschnig as code owners August 4, 2019 16:19

kroening assigned tautschnig Aug 4, 2019

tautschnig requested changes Aug 4, 2019

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Aug 4, 2019

kroening force-pushed the cpp-opX branch from 0921e5c to 7f48ddc Compare August 5, 2019 07:35

allredj reviewed Aug 5, 2019

View reviewed changes

kroening force-pushed the cpp-opX branch 2 times, most recently from 8f1a0be to 37fe7c7 Compare August 13, 2019 13:55

kroening assigned tautschnig and unassigned kroening Aug 13, 2019

allredj reviewed Aug 13, 2019

View reviewed changes

kroening force-pushed the cpp-opX branch 3 times, most recently from 887e2b1 to e8c4be1 Compare August 23, 2019 14:26

allredj reviewed Aug 23, 2019

View reviewed changes

kroening force-pushed the cpp-opX branch from e8c4be1 to f69bbac Compare October 10, 2019 13:20

allredj reviewed Oct 10, 2019

View reviewed changes

kroening force-pushed the cpp-opX branch from f69bbac to 9ff2a56 Compare October 12, 2019 08:44

allredj reviewed Oct 12, 2019

View reviewed changes

tautschnig approved these changes Oct 18, 2019

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Oct 18, 2019

fix exprt::opX() accesses in cpp/

6457a5e

This improves type safety.

kroening force-pushed the cpp-opX branch from 9ff2a56 to 6457a5e Compare October 20, 2019 23:52

allredj reviewed Oct 21, 2019

View reviewed changes

kroening merged commit 7a70b13 into develop Oct 22, 2019

kroening deleted the cpp-opX branch October 22, 2019 01:15

fix exprt::opX() accesses in cpp/ #4984

fix exprt::opX() accesses in cpp/ #4984

Uh oh!

Conversation

kroening commented Aug 4, 2019

Uh oh!

tautschnig 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!

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!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Aug 5, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

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!

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!

tautschnig 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Aug 5, 2019 •

edited

Loading