use typecast_exprt::conditional_cast

.make_typecast() isn't type save; when used in the pattern
if(a.type()!=b.type()) ... then use typecast_exprt::conditional_cast
instead.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1362,9 +1362,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       DATA_INVARIANT(
         arg0.id()==ID_constant,
         "ipush argument expected to be constant");
-      results[0]=arg0;
-      if(arg0.type()!=java_int_type())
-        results[0].make_typecast(java_int_type());
+      results[0] = typecast_exprt::conditional_cast(arg0, java_int_type());
     }
     else if(statement==patternt("if_?cmp??"))
     {
@@ -1574,9 +1572,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     {
       PRECONDITION(op.size() == 1 && results.size() == 1);
       typet type=java_type_from_char(statement[2]);
-      results[0]=op[0];
-      if(results[0].type()!=type)
-        results[0].make_typecast(type);
+      results[0] = typecast_exprt::conditional_cast(op[0], type);
     }
     else if(statement=="new")
     {
@@ -2225,9 +2221,9 @@ codet &java_bytecode_convert_methodt::replace_call_to_cprover_assume(
   codet &c)
 {
   exprt operand = pop(1)[0];
+
   // we may need to adjust the type of the argument
-  if(operand.type() != bool_typet())
-    operand.make_typecast(bool_typet());
+  operand = typecast_exprt::conditional_cast(operand, bool_typet());
 
   c = code_assumet(operand);
   location.set_function(method_id);
@@ -2649,16 +2645,12 @@ exprt::operandst &java_bytecode_convert_methodt::convert_ushr(
   const std::size_t width = get_bytecode_type_width(type);
   typet target = unsignedbv_typet(width);
 
-  exprt lhs = op[0];
-  if(lhs.type() != target)
-    lhs.make_typecast(target);
-  exprt rhs = op[1];
-  if(rhs.type() != target)
-    rhs.make_typecast(target);
+  exprt lhs = typecast_exprt::conditional_cast(op[0], target);
+  exprt rhs = typecast_exprt::conditional_cast(op[1], target);
+
+  results[0] =
+    typecast_exprt::conditional_cast(lshr_exprt(lhs, rhs), op[0].type());
 
-  results[0] = lshr_exprt(lhs, rhs);
-  if(results[0].type() != op[0].type())
-    results[0].make_typecast(op[0].type());
   return results;
 }
 

jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp

@@ -21,8 +21,8 @@ void java_bytecode_typecheckt::typecheck_code(codet &code)
     typecheck_expr(code_assign.lhs());
     typecheck_expr(code_assign.rhs());
 
-    if(code_assign.lhs().type()!=code_assign.rhs().type())
-      code_assign.rhs().make_typecast(code_assign.lhs().type());
+    code_assign.rhs() = typecast_exprt::conditional_cast(
+      code_assign.rhs(), code_assign.lhs().type());
   }
   else if(statement==ID_block)
   {

src/analyses/escape_analysis.cpp

@@ -421,8 +421,9 @@ void escape_analysist::insert_cleanup(
       exprt arg=lhs;
       if(is_object)
         arg=address_of_exprt(arg);
-      if(arg.type()!=param_type)
-        arg.make_typecast(param_type);
+
+      arg = typecast_exprt::conditional_cast(arg, param_type);
+
       code.arguments().push_back(arg);
     }
 

src/analyses/goto_check.cpp

@@ -1293,18 +1293,19 @@ void goto_checkt::bounds_check(
     const exprt &pointer=
       to_dereference_expr(ode.root_object()).pointer();
 
-    if_exprt size(
+    const if_exprt size(
       dynamic_object(pointer),
       typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
       object_size(pointer));
 
-    plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
+    const plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
 
     assert(effective_offset.op0().type()==effective_offset.op1().type());
-    if(effective_offset.type()!=size.type())
-      size.make_typecast(effective_offset.type());
 
-    binary_relation_exprt inequality(effective_offset, ID_lt, size);
+    const auto size_casted =
+      typecast_exprt::conditional_cast(size, effective_offset.type());
+
+    binary_relation_exprt inequality(effective_offset, ID_lt, size_casted);
 
     or_exprt precond(
       and_exprt(
@@ -1371,12 +1372,8 @@ void goto_checkt::bounds_check(
     binary_relation_exprt inequality(index, ID_lt, size);
 
     // typecast size
-    if(inequality.op1().type()!=inequality.op0().type())
-      inequality.op1().make_typecast(inequality.op0().type());
-
-    // typecast size
-    if(inequality.op1().type()!=inequality.op0().type())
-      inequality.op1().make_typecast(inequality.op0().type());
+    inequality.op1() = typecast_exprt::conditional_cast(
+      inequality.op1(), inequality.op0().type());
 
     add_guarded_claim(
       implies_exprt(type_matches_size, inequality),
@@ -1844,8 +1841,8 @@ void goto_checkt::goto_check(
           goto_programt::targett t=new_code.add_instruction(ASSIGN);
           exprt address_of_expr=address_of_exprt(variable);
           exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
-          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
-            address_of_expr.make_typecast(lhs.type());
+          address_of_expr =
+            typecast_exprt::conditional_cast(address_of_expr, lhs.type());
           const if_exprt rhs(
             side_effect_expr_nondett(bool_typet(), i.source_location),
             address_of_expr,

src/ansi-c/c_typecheck_expr.cpp

@@ -618,8 +618,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
               throw 0;
             }
 
-            if(o.type()!=size_type())
-              o.make_typecast(size_type());
+            o = typecast_exprt::conditional_cast(o, size_type());
 
             result=plus_exprt(result, o);
           }
@@ -652,8 +651,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
                     throw 0;
                   }
 
-                  if(o.type()!=size_type())
-                    o.make_typecast(size_type());
+                  o = typecast_exprt::conditional_cast(o, size_type());
 
                   result=plus_exprt(result, o);
                 }
@@ -695,8 +693,9 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
       typecheck_expr(index);
 
       exprt sub_size=size_of_expr(type.subtype(), *this);
-      if(index.type()!=size_type())
-        index.make_typecast(size_type());
+
+      index = typecast_exprt::conditional_cast(index, size_type());
+
       result=plus_exprt(result, mult_exprt(sub_size, index));
 
       typet tmp=type.subtype();
@@ -2972,8 +2971,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
       is_number(o_type0.subtype()))
     {
       // Vector arithmetic has fairly strict typing rules, no promotion
-      if(o_type0!=o_type1)
-        op1.make_typecast(op0.type());
+      op1 = typecast_exprt::conditional_cast(op1, op0.type());
       expr.type()=op0.type();
       return;
     }
@@ -3405,8 +3403,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
       if(gcc_vector_types_compatible(
            to_vector_type(o_type0), to_vector_type(o_type1)))
       {
-        if(o_type0!=o_type1)
-          op1.make_typecast(o_type0);
+        op1 = typecast_exprt::conditional_cast(op1, o_type0);
         return;
       }
     }
@@ -3426,8 +3423,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
       if(gcc_vector_types_compatible(
            to_vector_type(o_type0), to_vector_type(o_type1)))
       {
-        if(o_type0!=o_type1)
-          op1.make_typecast(o_type0);
+        op1 = typecast_exprt::conditional_cast(op1, o_type0);
         return;
       }
     }

src/cpp/cpp_typecheck_resolve.cpp

@@ -1724,9 +1724,7 @@ void cpp_typecheck_resolvet::guess_template_args(
           if(e.id()==ID_unassigned)
           {
             typet old_type=e.type();
-            e=desired_expr;
-            if(e.type()!=old_type)
-              e.make_typecast(old_type);
+            e = typecast_exprt::conditional_cast(desired_expr, old_type);
           }
         }
       }

src/pointer-analysis/goto_program_dereference.cpp

@@ -187,9 +187,7 @@ void goto_program_dereferencet::dereference_rec(
 
       exprt tmp;
       tmp.swap(expr.op0().op0());
-
-      if(tmp.type()!=expr.type())
-        tmp.make_typecast(expr.type());
+      tmp = typecast_exprt::conditional_cast(tmp, expr.type());
 
       expr.swap(tmp);
     }

src/solvers/flattening/arrays.cpp

@@ -325,12 +325,8 @@ void arrayst::add_array_Ackermann_constraints()
           // index equality
           equal_exprt indices_equal(*i1, *i2);
 
-          if(indices_equal.op0().type()!=
-             indices_equal.op1().type())
-          {
-            indices_equal.op1().
-              make_typecast(indices_equal.op0().type());
-          }
+          indices_equal.op1() = typecast_exprt::conditional_cast(
+            indices_equal.op1(), indices_equal.op0().type());
 
           literalt indices_equal_lit=convert(indices_equal);
 
@@ -537,8 +533,7 @@ void arrayst::add_array_constraints_with(
     {
       // we first build the guard
 
-      if(other_index.type()!=index.type())
-        other_index.make_typecast(index.type());
+      other_index = typecast_exprt::conditional_cast(other_index, index.type());
 
       literalt guard_lit=convert(equal_exprt(index, other_index));
 

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -91,8 +91,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
     object_descriptor_exprt o;
     o.build(expr.op(), ns);
     CHECK_RETURN(o.offset().id() != ID_unknown);
-    if(o.offset().type() != expr.offset().type())
-      o.offset().make_typecast(expr.offset().type());
+
+    o.offset() =
+      typecast_exprt::conditional_cast(o.offset(), expr.offset().type());
+
     byte_extract_exprt be(
       expr.id(),
       o.root_object(),

src/solvers/lowering/byte_operators.cpp

@@ -396,9 +396,7 @@ static exprt lower_byte_update(
 
           if(i==0 && element_size==1) // bytes?
           {
-            new_value = src.value();
-            if(new_value.type()!=subtype)
-              new_value.make_typecast(subtype);
+            new_value = typecast_exprt::conditional_cast(src.value(), subtype);
           }
           else
           {

src/util/pointer_offset_size.cpp

@@ -311,15 +311,14 @@ exprt size_of_expr(
       return nil_exprt();
 
     // get size
-    exprt size = array_type.size();
+    const auto size = array_type.size();
 
     if(size.is_nil())
       return nil_exprt();
 
-    if(size.type()!=sub.type())
-      size.make_typecast(sub.type());
+    const auto size_casted = typecast_exprt::conditional_cast(size, sub.type());
 
-    mult_exprt result(size, sub);
+    mult_exprt result(size_casted, sub);
     simplify(result, ns);
 
     return std::move(result);
@@ -342,15 +341,14 @@ exprt size_of_expr(
       return nil_exprt();
 
     // get size
-    exprt size=to_vector_type(type).size();
+    const auto size = to_vector_type(type).size();
 
     if(size.is_nil())
       return nil_exprt();
 
-    if(size.type()!=sub.type())
-      size.make_typecast(sub.type());
+    const auto size_casted = typecast_exprt::conditional_cast(size, sub.type());
 
-    mult_exprt result(size, sub);
+    mult_exprt result(size_casted, sub);
     simplify(result, ns);
 
     return std::move(result);
@@ -633,10 +631,7 @@ exprt build_sizeof_expr(
   if(remainder>0)
     result=plus_exprt(result, from_integer(remainder, t));
 
-  if(result.type()!=expr.type())
-    result.make_typecast(expr.type());
-
-  return result;
+  return typecast_exprt::conditional_cast(result, expr.type());
 }
 
 exprt get_subexpression_at_offset(

src/util/pointer_predicates.cpp

@@ -171,17 +171,16 @@ exprt dynamic_object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    const auto object_offset_casted =
+      typecast_exprt::conditional_cast(object_offset, access_size.type());
+
+    sum = plus_exprt(object_offset_casted, access_size);
   }
 
-  if(ns.follow(sum.type())!=
-     ns.follow(malloc_size.type()))
-    sum.make_typecast(malloc_size.type());
+  const auto sum_casted =
+    typecast_exprt::conditional_cast(sum, malloc_size.type());
 
-  return binary_relation_exprt(sum, op, malloc_size);
+  return binary_relation_exprt(sum_casted, op, malloc_size);
 }
 
 exprt object_upper_bound(
@@ -204,18 +203,16 @@ exprt object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
-  }
+    const auto object_offset_casted =
+      typecast_exprt::conditional_cast(object_offset, access_size.type());
 
+    sum = plus_exprt(object_offset_casted, access_size);
+  }
 
-  if(ns.follow(sum.type())!=
-     ns.follow(object_size_expr.type()))
-    sum.make_typecast(object_size_expr.type());
+  const auto sum_casted =
+    typecast_exprt::conditional_cast(sum, object_size_expr.type());
 
-  return binary_relation_exprt(sum, op, object_size_expr);
+  return binary_relation_exprt(sum_casted, op, object_size_expr);
 }
 
 exprt object_lower_bound(

src/util/simplify_expr_array.cpp

@@ -81,10 +81,10 @@ bool simplify_exprt::simplify_index(exprt &expr)
     {
       // Turn (a with i:=x)[j] into (i==j)?x:a[j].
       // watch out that the type of i and j might be different.
-      equal_exprt equality_expr(expr.op1(), with_expr.op1());
+      const exprt rhs_casted =
+        typecast_exprt::conditional_cast(with_expr.op1(), expr.op1().type());
 
-      if(equality_expr.lhs().type()!=equality_expr.rhs().type())
-        equality_expr.rhs().make_typecast(equality_expr.lhs().type());
+      equal_exprt equality_expr(expr.op1(), rhs_casted);
 
       simplify_inequality(equality_expr);