Replace make_typecast by typecast_exprt or typecast_exprt::conditional_cast [blocks: #3800] #3991

tautschnig · 2019-01-30T13:50:02Z

make_typecast is deprecated.

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.

smowton

Few places where there's now a multi-line statement after an if or for which I'd prefer to be braced, otherwise lgtm

src/goto-programs/builtin_functions.cpp

smowton · 2019-01-30T15:04:36Z

src/goto-programs/goto_convert.cpp

-      DATA_INVARIANT(
-        lhs.operands().size() == 1, "Typecast must have one operand");
+      UNREACHABLE; // the original code here was broken, presumably it's never used
+      typecast_exprt tc = to_typecast_expr(lhs);


I think some compilers will give you a hard time for this unreachable code

I have no idea how we would generate an expression that has a typecast on the left-hand side, but even if and when we do: at least goto-symex does handle that case, so we could safely leave it in the goto program. I am going to add a commit that simply removes this code.

We definitely do sometimes produce void** data = new void*[10]; ((Object**)data)[0] = new Object in the Java frontend. Whether we should is another question!

Sure, and you can make something similar happen in C (*(char*)&x = 42;) - but there's an index_exprt on the left-hand side in your example and a dereference_exprt in my case. Neither has a typecast at the top level on the left-hand side.

True. In the past we would sometimes do (Object*)var = new Object, but AFAIK that's no longer generated by the frontend

I think even if that were still the case, goto-symex would happily take care of that.

Just for the record, those changes have now been moved to #3770, this PR now exclusively deals with replacing make_typecast.

src/goto-programs/pointer_arithmetic.cpp

src/pointer-analysis/value_set.cpp

src/pointer-analysis/value_set_fi.cpp

src/pointer-analysis/value_set_fivr.cpp

src/pointer-analysis/value_set_fivrns.cpp

allredj

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

allredj

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

kroening · 2019-02-06T16:35:26Z

src/ansi-c/c_typecheck_expr.cpp

@@ -2955,7 +2956,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
    is_number(o_type1))
  {
    // convert op1 to the vector type
-    op1.make_typecast(o_type0);
+    op1 = typecast_exprt::conditional_cast(op1, o_type0);
    expr.type() = o_type0;


A conditional_cast appears to be wrong here. When we are in this branch, the cast is always needed. Simply use the constructor.

kroening · 2019-02-06T16:35:42Z

src/ansi-c/c_typecheck_expr.cpp

@@ -2964,7 +2965,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
    is_number(o_type0))
  {
    // convert op0 to the vector type
-    op0.make_typecast(o_type1);
+    op0 = typecast_exprt::conditional_cast(op0, o_type1);
    expr.type() = o_type1;


kroening · 2019-02-06T16:37:56Z

src/cpp/cpp_typecheck_conversions.cpp

    if(width==config.ansi_c.int_width)
      int_type.id(ID_unsignedbv);
-    new_expr.make_typecast(int_type);
+    new_expr = typecast_exprt::conditional_cast(expr, int_type);
    return true;


Same here -- the cast will always happen.

I don't think so - the line above the change would make the typecast a no-op.

Unrelated to PR: the two lines above the change are dead code (note the branch directly before). There's probably a bug there.

Oh, indeed. Aren't those two lines really just unnecessary, and we should do an unconditional cast as you suggested? To me it seems there no bug other than it being dead code.

The bug is that an "unsigned int" will be promoted to "signed int", which is wrong.

I don't think so, the width >= config.ansi_c.int_width would catch that?

kroening · 2019-02-06T16:38:38Z

src/cpp/cpp_typecheck_conversions.cpp

@@ -271,8 +267,7 @@ bool cpp_typecheckt::standard_conversion_floating_point_promotion(
  c_qualifierst qual_from;
  qual_from.read(expr.type());

-  new_expr=expr;
-  new_expr.make_typecast(double_type());
+  new_expr = typecast_exprt::conditional_cast(expr, double_type());
  qual_from.write(new_expr.type());


kroening · 2019-02-06T16:41:39Z

src/goto-cc/linker_script_merge.cpp

-    exprt rhs_tc(rhs);
-    rhs_tc.make_typecast(pointer_type(char_type()));
+    exprt rhs_tc =
+      typecast_exprt::conditional_cast(rhs, pointer_type(char_type()));



kroening · 2019-02-06T16:42:55Z

src/goto-programs/builtin_functions.cpp

-    if(count.type()!=object_size.type())
-      count.make_typecast(object_size.type());
+    count = typecast_exprt(
+      static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());



But here it's the conditional_cast

kroening · 2019-02-06T17:01:37Z

src/pointer-analysis/value_set_dereference.cpp

@@ -382,7 +382,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
      equal_exprt equality(pointer_expr, object_pointer);

      if(ns.follow(equality.lhs().type())!=ns.follow(equality.rhs().type()))
-        equality.lhs().make_typecast(equality.rhs().type());
+        equality.lhs() = typecast_exprt(equality.lhs(), equality.rhs().type());



Conditional cast!

Done (killing the ns.follow)

kroening · 2019-02-06T17:01:43Z

src/pointer-analysis/value_set_dereference.cpp

@@ -452,7 +452,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
      result.value=index_expr;

      if(ns.follow(result.value.type())!=ns.follow(dereference_type))
-        result.value.make_typecast(dereference_type);
+        result.value = typecast_exprt(result.value, dereference_type);
    }


Done (killing ns.follow)

kroening · 2019-02-06T17:01:48Z

src/pointer-analysis/value_set_dereference.cpp

@@ -594,7 +594,7 @@ bool value_set_dereferencet::memory_model_bytes(

    // possibly need to convert
    if(!base_type_eq(result.type(), to_type, ns))
-      result.make_typecast(to_type);
+      result = typecast_exprt(result, to_type);
  }


Done (killing this instance of base_type_eq)

allredj

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

allredj

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

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

…l_cast make_typecast is deprecated.

allredj

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

tautschnig added cleanup blocker labels Jan 30, 2019

tautschnig requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners January 30, 2019 13:50

tautschnig self-assigned this Jan 30, 2019

tautschnig added the work in progress label Jan 30, 2019

tautschnig force-pushed the deprecation-make_typecast branch from 5eeea41 to 8ce771e Compare January 30, 2019 14:36

tautschnig removed the work in progress label Jan 30, 2019

tautschnig removed their assignment Jan 30, 2019

smowton approved these changes Jan 30, 2019

View reviewed changes

tautschnig force-pushed the deprecation-make_typecast branch from 8ce771e to bc7f7d6 Compare January 30, 2019 18:16

tautschnig assigned kroening, peterschrammel, martin-cs and chrisr-diffblue Jan 30, 2019

tautschnig force-pushed the deprecation-make_typecast branch from bc7f7d6 to 9ee63c4 Compare January 30, 2019 20:10

allredj reviewed Jan 30, 2019

View reviewed changes

tautschnig force-pushed the deprecation-make_typecast branch from 9ee63c4 to 8685209 Compare February 2, 2019 23:17

tautschnig unassigned martin-cs Feb 2, 2019

allredj reviewed Feb 3, 2019

View reviewed changes

peterschrammel approved these changes Feb 3, 2019

View reviewed changes

peterschrammel removed their assignment Feb 3, 2019

tautschnig unassigned chrisr-diffblue Feb 4, 2019

tautschnig mentioned this pull request Feb 6, 2019

replace exprt::opX by named methods #4105

Merged

4 tasks

kroening reviewed Feb 6, 2019

View reviewed changes

kroening approved these changes Feb 6, 2019

View reviewed changes

kroening assigned tautschnig and unassigned kroening Feb 6, 2019

tautschnig force-pushed the deprecation-make_typecast branch from 8685209 to 76b2c26 Compare February 7, 2019 07:49

allredj reviewed Feb 7, 2019

View reviewed changes

tautschnig force-pushed the deprecation-make_typecast branch 2 times, most recently from 9ece3a7 to f6948db Compare February 7, 2019 12:00

allredj reviewed Feb 7, 2019

View reviewed changes

Replace make_typecast by typecast_exprt or typecast_exprt::conditiona…

ebaacea

…l_cast make_typecast is deprecated.

tautschnig force-pushed the deprecation-make_typecast branch from f6948db to ebaacea Compare February 7, 2019 13:13

allredj reviewed Feb 7, 2019

View reviewed changes

tautschnig merged commit dcb6b94 into diffblue:develop Feb 7, 2019

tautschnig deleted the deprecation-make_typecast branch February 7, 2019 15:29

Replace make_typecast by typecast_exprt or typecast_exprt::conditional_cast [blocks: #3800] #3991

Replace make_typecast by typecast_exprt or typecast_exprt::conditional_cast [blocks: #3800] #3991

Conversation

tautschnig commented Jan 30, 2019

smowton 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

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

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

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

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

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment