Merge pull request #6951 from diffblue/equal_exprt_type_check

equal_exprt now checks types of the operands

Author: kroening

src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

@@ -305,11 +305,13 @@ abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements(
 exprt full_struct_abstract_objectt::to_predicate_internal(
   const exprt &name) const
 {
+  const auto &compound_type = to_struct_union_type(name.type());
   auto all_predicates = exprt::operandst{};
 
   for(auto field : map.get_sorted_view())
   {
-    auto field_name = member_exprt(name, field.first, name.type());
+    auto field_name =
+      member_exprt(name, compound_type.get_component(field.first));
     auto field_expr = field.second->to_predicate(field_name);
 
     if(!field_expr.is_true())

src/cpp/cpp_typecheck_code.cpp

@@ -73,7 +73,8 @@ void cpp_typecheckt::typecheck_code(codet &code)
           shl_exprt shl{from_integer(1, array.type()),
                         to_index_expr(binary_expr.op0()).index()};
           exprt rhs = if_exprt{
-            equal_exprt{binary_expr.op1(), from_integer(0, array.type())},
+            equal_exprt{
+              binary_expr.op1(), from_integer(0, binary_expr.op1().type())},
             bitand_exprt{array, bitnot_exprt{shl}},
             bitor_exprt{array, shl}};
           binary_expr.op0() = to_index_expr(binary_expr.op0()).array();

src/goto-symex/symex_other.cpp

@@ -224,11 +224,13 @@ void goto_symext::symex_other(
     process_array_expr(state, array1);
     process_array_expr(state, array2);
 
-    exprt rhs = equal_exprt(array1, array2);
+    exprt rhs;
 
-    // check for size (or type) mismatch
+    // Types don't match? Make it 'false'.
     if(array1.type() != array2.type())
       rhs = false_exprt();
+    else
+      rhs = equal_exprt(array1, array2);
 
     symex_assign(state, code.op2(), rhs);
   }

src/linking/linking.cpp

@@ -949,6 +949,17 @@ bool linkingt::adjust_object_type_rec(
     }
     else
     {
+      if(new_size.type() != old_size.type())
+      {
+        link_error(
+          info.old_symbol,
+          info.new_symbol,
+          "conflicting array sizes for variable");
+
+        // error logged, continue typechecking other symbols
+        return true;
+      }
+
       equal_exprt eq(old_size, new_size);
 
       if(!simplify_expr(eq, ns).is_true())

src/statement-list/parser.y

@@ -1098,8 +1098,8 @@ Param_Assignment:
     Variable_Name TOK_ASSIGNMENT IL_Operand
     {
       newstack($$);
-      parser_stack($$) = equal_exprt{std::move(parser_stack($1)), 
-        std::move(parser_stack($3))};
+      parser_stack($$) = code_frontend_assignt(std::move(parser_stack($1)),
+        std::move(parser_stack($3)));
     }
     ;
 Opt_Data_Block:

src/statement-list/statement_list_parse_tree_io.cpp

@@ -40,8 +40,9 @@ static void output_constant(std::ostream &os, const constant_exprt &constant)
 /// Prints the assignment of a module parameter to the given output stream.
 /// \param [out] os: Stream that should receive the result.
 /// \param assignment: Assignment that shall be printed.
-static void
-output_parameter_assignment(std::ostream &os, const equal_exprt &assignment)
+static void output_parameter_assignment(
+  std::ostream &os,
+  const code_frontend_assignt &assignment)
 {
   os << assignment.lhs().get(ID_identifier) << " := ";
   const constant_exprt *const constant =
@@ -246,11 +247,10 @@ void output_instruction(
         output_constant(os, *constant);
         continue;
       }
-      const equal_exprt *const equal = expr_try_dynamic_cast<equal_exprt>(expr);
-      if(equal)
+      if(const auto assign = expr_try_dynamic_cast<code_frontend_assignt>(expr))
       {
         os << "\n\t";
-        output_parameter_assignment(os, *equal);
+        output_parameter_assignment(os, *assign);
         continue;
       }
       os << '\t' << expr.id();

src/statement-list/statement_list_typecheck.cpp

@@ -1593,9 +1593,9 @@ void statement_list_typecheckt::typecheck_CPROVER_assert(
   const codet &op_code,
   symbolt &tia_element)
 {
-  const equal_exprt *const assignment =
-    expr_try_dynamic_cast<equal_exprt>(op_code.op1());
-  if(assignment)
+  if(
+    const auto assignment =
+      expr_try_dynamic_cast<code_frontend_assignt>(op_code.op1()))
   {
     const code_assertt assertion{
       typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
@@ -1612,9 +1612,9 @@ void statement_list_typecheckt::typecheck_CPROVER_assume(
   const codet &op_code,
   symbolt &tia_element)
 {
-  const equal_exprt *const assignment =
-    expr_try_dynamic_cast<equal_exprt>(op_code.op1());
-  if(assignment)
+  if(
+    const auto assignment =
+      expr_try_dynamic_cast<code_frontend_assignt>(op_code.op1()))
   {
     const code_assumet assumption{
       typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
@@ -1660,7 +1660,7 @@ void statement_list_typecheckt::typecheck_called_function(
   const code_typet &called_type{to_code_type(called_function_sym.type)};
 
   // Check if function name is followed by data block.
-  if(!can_cast_expr<equal_exprt>(op_code.op1()))
+  if(!can_cast_expr<code_frontend_assignt>(op_code.op1()))
   {
     error() << "Function calls should not address instance data blocks" << eom;
     throw TYPECHECK_ERROR;
@@ -1669,11 +1669,11 @@ void statement_list_typecheckt::typecheck_called_function(
   // Check if function interface matches the call and fill argument list.
   const code_typet::parameterst &params{called_type.parameters()};
   code_function_callt::argumentst args;
-  std::vector<equal_exprt> assignments;
+  std::vector<code_frontend_assignt> assignments;
   for(const auto &expr : op_code.operands())
   {
-    if(can_cast_expr<equal_exprt>(expr))
-      assignments.push_back(to_equal_expr(expr));
+    if(auto assign = expr_try_dynamic_cast<code_frontend_assignt>(expr))
+      assignments.push_back(*assign);
   }
 
   for(const code_typet::parametert &param : params)
@@ -1706,13 +1706,13 @@ void statement_list_typecheckt::typecheck_called_function_block(
 }
 
 exprt statement_list_typecheckt::typecheck_function_call_arguments(
-  const std::vector<equal_exprt> &assignments,
+  const std::vector<code_frontend_assignt> &assignments,
   const code_typet::parametert &param,
   const symbolt &tia_element)
 {
   const irep_idt &param_name = param.get_base_name();
   const typet &param_type = param.type();
-  for(const equal_exprt &assignment : assignments)
+  for(const auto &assignment : assignments)
   {
     const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
     if(param_name == lhs.get_identifier())
@@ -1752,11 +1752,11 @@ exprt statement_list_typecheckt::typecheck_function_call_argument_rhs(
 }
 
 exprt statement_list_typecheckt::typecheck_return_value_assignment(
-  const std::vector<equal_exprt> &assignments,
+  const std::vector<code_frontend_assignt> &assignments,
   const typet &return_type,
   const symbolt &tia_element)
 {
-  for(const equal_exprt &assignment : assignments)
+  for(const auto &assignment : assignments)
   {
     const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
     if(ID_statement_list_return_value_id == lhs.get_identifier())

src/statement-list/statement_list_typecheck.h

@@ -719,7 +719,7 @@ class statement_list_typecheckt : public typecheckt
   /// \param tia_element: Symbol representation of the TIA element.
   /// \return Expression including the assigned symbol's name and type.
   exprt typecheck_function_call_arguments(
-    const std::vector<equal_exprt> &assignments,
+    const std::vector<code_frontend_assignt> &assignments,
     const code_typet::parametert &param,
     const symbolt &tia_element);
 
@@ -740,7 +740,7 @@ class statement_list_typecheckt : public typecheckt
   /// \param tia_element: Symbol representation of the TIA element.
   /// \return Expression including the assigned symbol's name and type.
   exprt typecheck_return_value_assignment(
-    const std::vector<equal_exprt> &assignments,
+    const std::vector<code_frontend_assignt> &assignments,
     const typet &return_type,
     const symbolt &tia_element);
 

src/util/std_expr.h

@@ -1308,6 +1308,7 @@ class equal_exprt:public binary_relation_exprt
   equal_exprt(exprt _lhs, exprt _rhs)
     : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
   {
+    PRECONDITION(lhs().type() == rhs().type());
   }
 
   static void check(

unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp

@@ -29,8 +29,7 @@ full_array_abstract_objectt::full_array_pointert build_array(
 {
   const typet type = signedbv_typet(32);
 
-  const array_typet array_type(
-    integer_typet(), from_integer(array.size(), type));
+  const array_typet array_type(type, from_integer(array.size(), type));
 
   exprt::operandst element_ops;
 

unit/goto-symex/try_evaluate_pointer_comparisons.cpp

@@ -80,16 +80,14 @@ SCENARIO(
       }
     }
 
-    WHEN("Evaluating ptr1 == (long*)(short*)&value1")
+    WHEN("Evaluating ptr1 == (int*)(short*)&value1")
     {
       const signedbv_typet long_type{64};
       const signedbv_typet short_type{16};
-      const pointer_typet ptr_long_type = pointer_type(long_type);
       const pointer_typet ptr_short_type = pointer_type(short_type);
       const equal_exprt comparison{
         ptr1,
-        typecast_exprt{typecast_exprt{address1, ptr_short_type},
-                       ptr_long_type}};
+        typecast_exprt{typecast_exprt{address1, ptr_short_type}, ptr_type}};
       const renamedt<exprt, L2> renamed_comparison =
         state.rename(comparison, ns);
       auto result = try_evaluate_pointer_comparisons(