fix accesses to exprt::opX() in ansi-c/ #4983

kroening · 2019-08-04T15:21:42Z

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

This seems to be removing a bunch of user-facing error messages. Either these were dead code or we are now going to produce invariant violations that can be triggered by input files, which would be entirely wrong.

src/ansi-c/ansi_c_convert_type.cpp

src/ansi-c/c_typecheck_base.cpp

src/ansi-c/c_typecheck_expr.cpp

kroening · 2019-08-04T17:42:56Z

@tautschnig I did think about those error messages: the conditions checked by them should be post-conditions of the parser, i.e., it should be impossible for a user to trigger these.

allredj

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

tautschnig · 2019-08-05T06:40:38Z

@tautschnig I did think about those error messages: the conditions checked by them should be post-conditions of the parser, i.e., it should be impossible for a user to trigger these.

Seems fair. In that case, can all the to_unary_expr, to_binary_expr please be done as early in the control flow as possible? It will not always be possible, but in many cases the typecheck_... method should take a unary_exprt etc rather than doing this conversion within the method, often doing so multiple times.

kroening · 2019-08-05T07:24:39Z

@tautschnig Yes, agreed -- these should be early. That will touch both the ansi-c and C++ front-ends, and we would need to think about a mechanism similar to what we've done in the simplifier. The problem is that some of the typechecking methods change the type of what's being checked.

tautschnig · 2019-08-05T07:52:52Z

The problem is that some of the typechecking methods change the type of what's being checked.

While that's certainly true we don't change the number of operands, do we? So using unary_exprt, binary_exprt should be fine?

allredj

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

tautschnig

I've only reviewed about the first half, but my comments seemed to repeat a lot so I think those should be addressed across the PR (or discussed and resolved) first.

src/ansi-c/c_typecheck_base.cpp

src/ansi-c/c_typecheck_expr.cpp

kroening · 2019-08-05T11:10:09Z

While that's certainly true we don't change the number of operands, do we? So using unary_exprt, binary_exprt should be fine?

Yes, we may change the number of operands, at least in some places.

allredj

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

codecov-io · 2019-08-05T12:18:41Z

Codecov Report

Merging #4983 into develop will increase coverage by 0.01%.
The diff coverage is 72.63%.

@@             Coverage Diff             @@
##           develop    #4983      +/-   ##
===========================================
+ Coverage    69.24%   69.26%   +0.01%     
===========================================
  Files         1309     1309              
  Lines       108476   108430      -46     
===========================================
- Hits         75117    75102      -15     
+ Misses       33359    33328      -31

Impacted Files	Coverage Δ
src/util/std_code.h	`92.19% <ø> (+1%)`	⬆️
src/ansi-c/ansi_c_convert_type.cpp	`82.63% <ø> (+0.19%)`	⬆️
src/ansi-c/c_typecheck_base.h	`100% <ø> (ø)`	⬆️
src/ansi-c/c_typecheck_code.cpp	`82.1% <100%> (-0.06%)`	⬇️
src/ansi-c/ansi_c_language.cpp	`97.26% <100%> (+0.03%)`	⬆️
src/ansi-c/parser.y	`78.08% <100%> (ø)`	⬆️
src/ansi-c/c_typecheck_base.cpp	`80.89% <100%> (ø)`	⬆️
src/ansi-c/c_typecheck_type.cpp	`76.08% <100%> (+0.08%)`	⬆️
src/ansi-c/expr2c.cpp	`67.04% <30%> (-0.1%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`73.61% <73.17%> (+1.08%)`	⬆️
... and 3 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 602e2e8...7e20208. Read the comment docs.

tautschnig

I've resolved all the comments that won't be fixed in this PR, but some others remain open and I added a few more now that I made it through the entire PR.

src/ansi-c/c_typecheck_expr.cpp

tautschnig · 2019-08-05T12:15:17Z

src/ansi-c/c_typecheck_expr.cpp

-  exprt &op0=expr.op0();
-  exprt &op1=expr.op1();
+  exprt &op0 = to_binary_expr(expr).op0();
+  exprt &op1 = to_binary_expr(expr).op1();


I think we should do to_binary_expr just once.

src/ansi-c/c_typecheck_expr.cpp

tautschnig · 2019-08-05T12:15:33Z

src/ansi-c/c_typecheck_expr.cpp

-  exprt &op0=expr.op0();
-  exprt &op1=expr.op1();
+  exprt &op0 = to_binary_expr(expr).op0();
+  exprt &op1 = to_binary_expr(expr).op1();


I think we should do to_binary_expr just once.

src/ansi-c/c_typecheck_initializer.cpp

src/ansi-c/c_typecheck_type.cpp

tautschnig · 2019-08-05T12:18:41Z

src/ansi-c/c_typecheck_type.cpp

+    DATA_INVARIANT(
+      as_expr.operands().size() == 1,
+      "typeof of an expression must have one operand");
+    exprt expr = to_unary_expr(as_expr).op();


Why this DATA_INVARIANT here when elsewhere we just use to_unary_expr?

src/ansi-c/expr2c.cpp

This improves type safety.

allredj

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

kroening added the cleanup label Aug 4, 2019

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners August 4, 2019 15:21

kroening assigned tautschnig Aug 4, 2019

tautschnig requested changes Aug 4, 2019

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Aug 4, 2019

allredj reviewed Aug 4, 2019

View reviewed changes

kroening force-pushed the ansi-c-opX branch from 117a17c to 79b35a6 Compare August 5, 2019 07:25

allredj reviewed Aug 5, 2019

View reviewed changes

tautschnig reviewed Aug 5, 2019

View reviewed changes

kroening force-pushed the ansi-c-opX branch from 79b35a6 to 7e20208 Compare August 5, 2019 11:20

allredj reviewed Aug 5, 2019

View reviewed changes

tautschnig reviewed Aug 5, 2019

View reviewed changes

Daniel Kroening added 2 commits August 5, 2019 19:44

added side_effect_expr_statement_expressiont

75e1999

fix accesses to exprt::opX() in ansi-c/

9ae4c37

This improves type safety.

kroening force-pushed the ansi-c-opX branch from 7e20208 to 9ae4c37 Compare August 5, 2019 18:44

kroening assigned tautschnig and unassigned kroening Aug 5, 2019

allredj reviewed Aug 5, 2019

View reviewed changes

tautschnig approved these changes Aug 6, 2019

View reviewed changes

tautschnig merged commit 33c00c1 into develop Aug 6, 2019

tautschnig deleted the ansi-c-opX branch August 6, 2019 00:08

fix accesses to exprt::opX() in ansi-c/ #4983

fix accesses to exprt::opX() in ansi-c/ #4983

Uh oh!

Conversation

kroening commented Aug 4, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kroening commented Aug 4, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Aug 5, 2019

Uh oh!

kroening commented Aug 5, 2019

Uh oh!

tautschnig commented Aug 5, 2019

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kroening commented Aug 5, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Aug 5, 2019

Codecov Report

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment