Verilog: fix assignment context semantics

Author: kroening

regression/verilog/assignments/assignment-context1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 assignment-context1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The variants that enlarge give a wrong answer.

src/verilog/verilog_typecheck.cpp

@@ -41,16 +41,43 @@ void verilog_typecheckt::assignment_conversion(
   exprt &rhs,
   const typet &lhs_type)
 {
-  // Implements 1800-2017 10.7
-  // If the RHS is smaller than the LHS:
-  // * if the RHS is unsigned, it is zero-padded
-  // * if the RHS is signed, it is sign-extended
-  // If the RHS is larger than the LHS, it is truncated.
-
-  // This matches our typecast, but differs from the steps taken
-  // when evaluating binary expressions (11.8.2), where sign
-  // extension only happens when the propagated type is signed.
-  implicit_typecast(rhs, lhs_type);
+  // Implements 1800-2017 10.7 and 1800-2017 11.8.3.
+  //
+  // "The size of the left-hand side of an assignment forms
+  // the context for the right-hand expression."
+
+  // Get the width of LHS and RHS
+  auto lhs_width = get_width(lhs_type);
+  auto rhs_width = get_width(rhs.type());
+
+  if(lhs_width > rhs_width)
+  {
+    // Need to enlarge the RHS.
+    //
+    // "If needed, extend the size of the right-hand side,
+    // performing sign extension if, and only if, the type
+    // of the right-hand side is signed.
+    if((rhs.type().id() == ID_signedbv || rhs.type().id() == ID_verilog_signedbv) &&
+       (lhs_type.id() == ID_unsignedbv || lhs_type.id() == ID_verilog_unsignedbv))
+    {
+      // LHS is unsigned, RHS is signed. Must sign-extend.
+      auto new_rhs_type = to_bitvector_type(rhs.type());
+      new_rhs_type.set_width(numeric_cast_v<std::size_t>(lhs_width));
+
+      downwards_type_propagation(rhs, new_rhs_type);
+
+      // then cast
+      rhs = typecast_exprt::conditional_cast(rhs, lhs_type);
+    }
+    else
+      downwards_type_propagation(rhs, lhs_type);
+  }
+  else
+  {
+    // no need to enlarge
+    rhs = typecast_exprt::conditional_cast(rhs, lhs_type);
+  }
+
 }
 
 /*******************************************************************\