Merge pull request #3770 from tautschnig/cleanup-promotion

Move promotion rule application to C front-end [blocks: #3725, #3800]

Author: tautschnig

regression/cbmc/Overflow_Addition3/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --signed-overflow-check --conversion-check
 ^EXIT=10$

regression/cbmc/complex1/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  #ifdef __GNUC__
+#ifdef __GNUC__
   _Complex c; // this is usually '_Complex double'
   c=1.0i+2;
 
@@ -21,10 +21,10 @@ int main()
 
   // The real part is stored first in memory on i386.
   // Need to find out about other architectures.
-  #if defined(__i386__) || defined(__amd64__)
+#if defined(__i386__) || defined(__amd64__)
   assert(((signed char *)&char_complex)[0]==-2);
   assert(((signed char *)&char_complex)[1]==3);
-  #endif
+#endif
 
   assert(__real__ char_complex == -2);
   assert(__imag__ char_complex == 3);
@@ -44,18 +44,35 @@ int main()
   char_complex++;
   assert(__real__ char_complex == 101);
   assert(__imag__ char_complex == 3);
+  ++char_complex;
+  assert(__real__ char_complex == 102);
+  assert(__imag__ char_complex == 3);
+  char_complex += 1;
+  assert(__real__ char_complex == 103);
+  assert(__imag__ char_complex == 3);
 
   // also separately
   (__real__ char_complex)++;
-  assert(__real__ char_complex == 102);
+  assert(__real__ char_complex == 104);
   assert(__imag__ char_complex == 3);
 
   // casts to reals produce the real part
-  assert((int) char_complex == 102);
+  assert((int)char_complex == 104);
+
+  // can be decremented
+  char_complex--;
+  assert(__real__ char_complex == 103);
+  assert(__imag__ char_complex == 3);
+  --char_complex;
+  assert(__real__ char_complex == 102);
+  assert(__imag__ char_complex == 3);
+  char_complex -= 1;
+  assert(__real__ char_complex == 101);
+  assert(__imag__ char_complex == 3);
 
-  #else
+#else
 
   // Visual studio doesn't have it
 
-  #endif
+#endif
 }

regression/cbmc/enum8/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+enum E
+{
+  A = 1,
+  B = 16
+};
+
+int main()
+{
+  enum E e = A;
+  e <<= 4;
+  assert(e == B);
+  e >>= 4;
+  assert(e == A);
+  e |= B;
+  e ^= A;
+  assert(e == B);
+  e -= 15;
+  assert(e == A);
+  return 0;
+}

regression/cbmc/enum8/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -1855,16 +1855,19 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
 
     if(type0.id() == ID_c_enum_tag)
     {
-      if(follow_tag(to_c_enum_tag_type(type0)).is_incomplete())
+      const c_enum_typet &enum_type = follow_tag(to_c_enum_tag_type(type0));
+      if(enum_type.is_incomplete())
       {
         error().source_location = expr.source_location();
         error() << "operator `" << statement
                 << "' given incomplete type `"
                 << to_string(type0) << "'" << eom;
         throw 0;
       }
-      else
-        expr.type()=type0;
+
+      // increment/decrement on underlying type
+      expr.op0() = typecast_exprt(expr.op0(), enum_type.subtype());
+      expr.type() = enum_type.subtype();
     }
     else if(type0.id() == ID_c_bit_field)
     {
@@ -1873,6 +1876,11 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
       expr.op0() = typecast_exprt(expr.op0(), underlying_type);
       expr.type()=underlying_type;
     }
+    else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
+    {
+      implicit_typecast_arithmetic(expr.op0());
+      expr.type() = expr.op0().type();
+    }
     else if(is_numeric_type(type0))
     {
       expr.type()=type0;
@@ -3321,6 +3329,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
   else if(statement==ID_assign_shl ||
           statement==ID_assign_shr)
   {
+    implicit_typecast_arithmetic(op0);
     implicit_typecast_arithmetic(op1);
 
     if(is_number(op1.type()))
@@ -3335,12 +3344,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
 
         typet underlying_type=op0.type();
 
-        if(underlying_type.id()==ID_c_enum_tag)
-        {
-          const auto &c_enum_type = to_c_enum_tag_type(underlying_type);
-          underlying_type=c_enum_type.subtype();
-        }
-
         if(underlying_type.id()==ID_unsignedbv ||
            underlying_type.id()==ID_c_bool)
         {
@@ -3363,7 +3366,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
     if(o_type0.id()==ID_bool ||
        o_type0.id()==ID_c_bool)
     {
-      implicit_typecast_arithmetic(op1);
+      implicit_typecast_arithmetic(op0, op1);
       if(op1.type().id()==ID_bool ||
          op1.type().id()==ID_c_bool ||
          op1.type().id()==ID_c_enum_tag ||
@@ -3376,7 +3379,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
             o_type0.id()==ID_signedbv ||
             o_type0.id()==ID_c_bit_field)
     {
-      implicit_typecast(op1, o_type0);
+      implicit_typecast_arithmetic(op0, op1);
       return;
     }
     else if(o_type0.id()==ID_vector &&
@@ -3413,7 +3416,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
     else if(o_type0.id()==ID_bool ||
             o_type0.id()==ID_c_bool)
     {
-      implicit_typecast_arithmetic(op1);
+      implicit_typecast_arithmetic(op0, op1);
       if(op1.type().id()==ID_bool ||
          op1.type().id()==ID_c_bool ||
          op1.type().id()==ID_c_enum_tag ||

src/goto-programs/goto_convert_side_effect.cpp

@@ -44,10 +44,13 @@ void goto_convertt::remove_assignment(
 
   if(statement==ID_assign)
   {
-    exprt tmp=expr;
-    tmp.id(ID_code);
-    // just interpret as code
-    convert_assign(to_code_assign(to_code(tmp)), dest, mode);
+    exprt new_lhs = skip_typecast(expr.op0());
+    exprt new_rhs =
+      typecast_exprt::conditional_cast(expr.op1(), new_lhs.type());
+    code_assignt assign(std::move(new_lhs), std::move(new_rhs));
+    assign.add_source_location() = expr.source_location();
+
+    convert_assign(assign, dest, mode);
   }
   else if(statement==ID_assign_plus ||
           statement==ID_assign_minus ||
@@ -99,33 +102,19 @@ void goto_convertt::remove_assignment(
 
     const typet &op0_type = expr.op0().type();
 
-    if(op0_type.id()==ID_c_bool)
-    {
-      // C/C++ Booleans get very special treatment.
-      binary_exprt tmp(expr.op0(), new_id, expr.op1(), expr.op1().type());
-      tmp.op0().make_typecast(expr.op1().type());
-      rhs=typecast_exprt(is_not_zero(tmp, ns), expr.op0().type());
-    }
-    else if(op0_type.id() == ID_c_enum_tag)
-    {
-      // We convert c_enums to their underlying type, do the
-      // operation, and then convert back
-      const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(op0_type));
-      auto underlying_type = enum_type.subtype();
-      auto op0 = typecast_exprt(expr.op0(), underlying_type);
-      auto op1 = typecast_exprt(expr.op1(), underlying_type);
-      binary_exprt tmp(op0, new_id, op1, underlying_type);
-      rhs = typecast_exprt(tmp, expr.op0().type());
-    }
-    else
-    {
-      rhs.id(new_id);
-      rhs.copy_to_operands(expr.op0(), expr.op1());
-      rhs.type()=expr.op0().type();
-      rhs.add_source_location()=expr.source_location();
-    }
+    PRECONDITION(
+      op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
+      op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);
+    rhs.id(new_id);
+    rhs.copy_to_operands(expr.op0(), expr.op1());
+    rhs.type() = expr.op0().type();
+    rhs.add_source_location() = expr.source_location();
+
+    exprt new_lhs = skip_typecast(expr.op0());
+    rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
+    rhs.add_source_location() = expr.source_location();
 
-    code_assignt assignment(expr.op0(), rhs);
+    code_assignt assignment(new_lhs, rhs);
     assignment.add_source_location()=expr.source_location();
 
     convert(assignment, dest, mode);
@@ -171,45 +160,34 @@ void goto_convertt::remove_pre(
 
   const typet &op_type = expr.op0().type();
 
-  if(op_type.id()==ID_bool)
-  {
-    rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
-    rhs.op0().make_typecast(signed_int_type());
-    rhs.type()=signed_int_type();
-    rhs=is_not_zero(rhs, ns);
-  }
-  else if(op_type.id()==ID_c_bool)
+  PRECONDITION(
+    op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
+    op_type.id() != ID_c_bool && op_type.id() != ID_bool);
+
+  typet constant_type;
+
+  if(op_type.id() == ID_pointer)
+    constant_type = index_type();
+  else if(is_number(op_type))
+    constant_type = op_type;
+  else
   {
-    rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
-    rhs.op0().make_typecast(signed_int_type());
-    rhs.type()=signed_int_type();
-    rhs=is_not_zero(rhs, ns);
-    rhs.make_typecast(op_type);
+    UNREACHABLE;
   }
-  else if(op_type.id()==ID_c_enum ||
-          op_type.id()==ID_c_enum_tag)
+
+  exprt constant;
+
+  if(constant_type.id() == ID_complex)
   {
-    rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
-    rhs.op0().make_typecast(signed_int_type());
-    rhs.type()=signed_int_type();
-    rhs.make_typecast(op_type);
+    exprt real = from_integer(1, constant_type.subtype());
+    exprt imag = from_integer(0, constant_type.subtype());
+    constant = complex_exprt(real, imag, to_complex_type(constant_type));
   }
   else
-  {
-    typet constant_type;
-
-    if(op_type.id()==ID_pointer)
-      constant_type=index_type();
-    else if(is_number(op_type) || op_type.id()==ID_c_bool)
-      constant_type=op_type;
-    else
-    {
-      UNREACHABLE;
-    }
+    constant = from_integer(1, constant_type);
 
-    rhs.add_to_operands(expr.op0(), from_integer(1, constant_type));
-    rhs.type()=expr.op0().type();
-  }
+  rhs.add_to_operands(expr.op0(), std::move(constant));
+  rhs.type() = expr.op0().type();
 
   code_assignt assignment(expr.op0(), rhs);
   assignment.add_source_location()=expr.find_source_location();
@@ -257,56 +235,34 @@ void goto_convertt::remove_post(
 
   const typet &op_type = expr.op0().type();
 
-  if(op_type.id()==ID_bool)
-  {
-    rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
-    rhs.op0().make_typecast(signed_int_type());
-    rhs.type()=signed_int_type();
-    rhs=is_not_zero(rhs, ns);
-  }
-  else if(op_type.id()==ID_c_bool)
+  PRECONDITION(
+    op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
+    op_type.id() != ID_c_bool && op_type.id() != ID_bool);
+
+  typet constant_type;
+
+  if(op_type.id() == ID_pointer)
+    constant_type = index_type();
+  else if(is_number(op_type))
+    constant_type = op_type;
+  else
   {
-    rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
-    rhs.op0().make_typecast(signed_int_type());
-    rhs.type()=signed_int_type();
-    rhs=is_not_zero(rhs, ns);
-    rhs.make_typecast(op_type);
+    UNREACHABLE;
   }
-  else if(op_type.id()==ID_c_enum ||
-          op_type.id()==ID_c_enum_tag)
+
+  exprt constant;
+
+  if(constant_type.id() == ID_complex)
   {
-    rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
-    rhs.op0().make_typecast(signed_int_type());
-    rhs.type()=signed_int_type();
-    rhs.make_typecast(op_type);
+    exprt real = from_integer(1, constant_type.subtype());
+    exprt imag = from_integer(0, constant_type.subtype());
+    constant = complex_exprt(real, imag, to_complex_type(constant_type));
   }
   else
-  {
-    typet constant_type;
+    constant = from_integer(1, constant_type);
 
-    if(op_type.id()==ID_pointer)
-      constant_type=index_type();
-    else if(is_number(op_type) || op_type.id()==ID_c_bool)
-      constant_type=op_type;
-    else
-    {
-      UNREACHABLE;
-    }
-
-    exprt constant;
-
-    if(constant_type.id()==ID_complex)
-    {
-      exprt real=from_integer(1, constant_type.subtype());
-      exprt imag=from_integer(0, constant_type.subtype());
-      constant=complex_exprt(real, imag, to_complex_type(constant_type));
-    }
-    else
-      constant=from_integer(1, constant_type);
-
-    rhs.add_to_operands(expr.op0(), std::move(constant));
-    rhs.type()=expr.op0().type();
-  }
+  rhs.add_to_operands(expr.op0(), std::move(constant));
+  rhs.type() = expr.op0().type();
 
   code_assignt assignment(expr.op0(), rhs);
   assignment.add_source_location()=expr.find_source_location();