Verilog: fix semantics of relations

regression/ebmc/smv-word-level/verilog1.desc

@@ -4,7 +4,7 @@ verilog1.sv
 ^MODULE main$
 ^VAR x : unsigned word\[32\];$
 ^INIT main\.x = 0ud32_0$
-^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$
+^INVAR Verilog::main\.x_aux0 = main\.x \+ unsigned\(0sd32_1\)$
 ^TRANS next\(main\.x\) = Verilog::main\.x_aux0$
 ^LTLSPEC F main\.x = unsigned\(0sd32_10\)$
 ^EXIT=0$

regression/verilog/assignments/assignment-with-function-call1.sv

@@ -10,8 +10,8 @@ module top(input [7:0] a, input [7:0] b);
   wire [7:0] sum_a_b = fn(a, b),
              sum_1_2 = fn(1, 2),
              sum_2_3 = fn(2, 3);
-  
-  assert property (sum_a_b==a[2:0]+b[2:0]);
+
+  assert property (sum_a_b[2:0]==a[2:0]+b[2:0]);
 
   assert property (sum_1_2==3);
 

regression/verilog/expressions/equality1.desc

@@ -10,7 +10,7 @@ equality1.v
 ^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED .*$
 ^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED .*$
 ^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED .*$
-^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED .*$
+^\[.*\] always 1'sb1 == 2'sb11 === 1: PROVED .*$
 ^\[.*\] always 1\.1 == 1\.1 == 1: PROVED .*$
 ^\[.*\] always 1\.1 == 1 == 0: PROVED .*$
 ^EXIT=0$

regression/verilog/expressions/equality2.desc

@@ -12,7 +12,7 @@ equality2.v
 ^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED .*$
 ^\[.*\] always 1 === 1 == 1: PROVED .*$
 ^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED .*$
-^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED .*$
+^\[.*\] always 3'sb111 === 2'sb11 == 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/shl4.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE broken-smt-backend
 shl4.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

regression/verilog/expressions/wildcard_equality1.desc

@@ -10,7 +10,7 @@ wildcard_equality1.sv
 ^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED .*$
 ^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED .*$
 ^\[main\.property09\] always 1'sb1 ==\? 2'b11 === 0: PROVED .*$
-^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED .*$
+^\[main\.property10\] always 1'sb1 ==\? 2'sb11 === 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/system-functions/past6.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 past6.sv
 
 ^EXIT=10$

src/verilog/verilog_typecheck_expr.cpp

@@ -222,6 +222,39 @@ void verilog_typecheck_exprt::propagate_type(
 
 /*******************************************************************\
 
+Function: zero_extend
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static exprt zero_extend(const exprt &expr, const typet &type)
+{
+  auto old_width = expr.type().id() == ID_bool ? 1
+                   : expr.type().id() == ID_integer
+                     ? 32
+                     : to_bitvector_type(expr.type()).get_width();
+
+  // first make unsigned
+  typet tmp_type;
+
+  if(type.id() == ID_unsignedbv)
+    tmp_type = unsignedbv_typet{old_width};
+  else if(type.id() == ID_verilog_unsignedbv)
+    tmp_type = verilog_unsignedbv_typet{old_width};
+  else
+    PRECONDITION(false);
+
+  return typecast_exprt::conditional_cast(
+    typecast_exprt::conditional_cast(expr, tmp_type), type);
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::downwards_type_progatation
 
   Inputs:
@@ -241,95 +274,69 @@ void verilog_typecheck_exprt::downwards_type_propagation(
 
   // Any context-determined operand of an operator shall be the
   // same type and size as the result of the operator.
-  // Exceptions:
-  // * result type real -- just cast
-  // * relational operators are always 1 bit unsigned
+  // As an exception, if the result type is real, the operands
+  // are just casted.
 
   if(expr.type() == type)
     return;
 
-  vtypet vt_from = vtypet(expr.type());
-  vtypet vt_to = vtypet(type);
-
-  if(!vt_from.is_other() && !vt_to.is_other() && expr.has_operands())
+  if(type.id() == ID_verilog_real || type.id() == ID_verilog_shortreal)
   {
-    // arithmetic
-
-    if(
-      expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
-      expr.id() == ID_div || expr.id() == ID_unary_minus ||
-      expr.id() == ID_unary_plus)
-    {
-      if(type.id() != ID_bool)
-      {
-        Forall_operands(it, expr)
-          propagate_type(*it, type);
-
-        expr.type() = type;
-
-        return;
-      }
-    }
-    else if(
-      expr.id() == ID_bitand || expr.id() == ID_bitor ||
-      expr.id() == ID_bitnand || expr.id() == ID_bitnor ||
-      expr.id() == ID_bitxor || expr.id() == ID_bitxnor ||
-      expr.id() == ID_bitnot)
-    {
-      Forall_operands(it, expr)
-        propagate_type(*it, type);
-
-      expr.type() = type;
-
-      if(type.id() == ID_bool)
-      {
-        if(expr.id() == ID_bitand)
-          expr.id(ID_and);
-        else if(expr.id() == ID_bitor)
-          expr.id(ID_or);
-        else if(expr.id() == ID_bitnand)
-          expr.id(ID_nand);
-        else if(expr.id() == ID_bitnor)
-          expr.id(ID_nor);
-        else if(expr.id() == ID_bitxor)
-          expr.id(ID_xor);
-        else if(expr.id() == ID_bitxnor)
-          expr.id(ID_xnor);
-        else if(expr.id() == ID_bitnot)
-          expr.id(ID_not);
-      }
-
-      return;
-    }
-    else if(expr.id() == ID_if)
-    {
-      if(expr.operands().size() == 3)
-      {
-        propagate_type(to_if_expr(expr).true_case(), type);
-        propagate_type(to_if_expr(expr).false_case(), type);
-
-        expr.type() = type;
-        return;
-      }
-    }
-    else if(expr.id() == ID_shl) // does not work with shr
-    {
-      // does not work with boolean
-      if(type.id() != ID_bool)
-      {
-        if(expr.operands().size() == 2)
-        {
-          propagate_type(to_binary_expr(expr).op0(), type);
-          // not applicable to second operand
+    expr = typecast_exprt{expr, type};
+    return;
+  }
 
-          expr.type() = type;
-          return;
-        }
-      }
-    }
+  // expressions with context-determined width, following
+  // 1800-2017 Table 11-21
+  if(
+    expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
+    expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitand ||
+    expr.id() == ID_bitor || expr.id() == ID_bitxor ||
+    expr.id() == ID_bitxnor || expr.id() == ID_unary_plus ||
+    expr.id() == ID_unary_minus || expr.id() == ID_bitnot)
+  {
+    // All operands are context-determined.
+    for(auto &op : expr.operands())
+      downwards_type_propagation(op, type);
+    expr.type() = type;
+    return;
+  }
+  else if(
+    expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr ||
+    expr.id() == ID_power)
+  {
+    // The LHS is context-determined, the RHS is self-determined
+    auto &binary_expr = to_binary_expr(expr);
+    downwards_type_propagation(binary_expr.lhs(), type);
+    expr.type() = type;
+    return;
+  }
+  else if(expr.id() == ID_if)
+  {
+    // The first operand is self-determined, the others are context-determined
+    auto &if_expr = to_if_expr(expr);
+    downwards_type_propagation(if_expr.op1(), type);
+    downwards_type_propagation(if_expr.op2(), type);
+    expr.type() = type;
+    return;
   }
 
-  implicit_typecast(expr, type);
+  // Just cast the expression, leave any operands as they are.
+  if(
+    (expr.type().id() == ID_signedbv ||
+     expr.type().id() == ID_verilog_signedbv) &&
+    (type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv) &&
+    get_width(expr.type()) < get_width(type))
+  {
+    // "If the operand shall be extended, then it shall be sign-extended only
+    // if the propagated type is signed."
+    // A typecast from signed to a larger unsigned would sign extend.
+    expr = zero_extend(expr, type);
+  }
+  else
+  {
+    expr = typecast_exprt{expr, type};
+  }
 }
 
 /*******************************************************************\
@@ -2535,39 +2542,6 @@ void verilog_typecheck_exprt::tc_binary_expr(
 
 /*******************************************************************\
 
-Function: zero_extend
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-static exprt zero_extend(const exprt &expr, const typet &type)
-{
-  auto old_width = expr.type().id() == ID_bool ? 1
-                   : expr.type().id() == ID_integer
-                     ? 32
-                     : to_bitvector_type(expr.type()).get_width();
-
-  // first make unsigned
-  typet tmp_type;
-
-  if(type.id() == ID_unsignedbv)
-    tmp_type = unsignedbv_typet{old_width};
-  else if(type.id() == ID_verilog_unsignedbv)
-    tmp_type = verilog_unsignedbv_typet{old_width};
-  else
-    PRECONDITION(false);
-
-  return typecast_exprt::conditional_cast(
-    typecast_exprt::conditional_cast(expr, tmp_type), type);
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheck_exprt::convert_relation
 
   Inputs:
@@ -2580,43 +2554,11 @@ Function: verilog_typecheck_exprt::convert_relation
 
 void verilog_typecheck_exprt::convert_relation(binary_exprt &expr)
 {
-  auto &lhs = expr.lhs();
-  auto &rhs = expr.rhs();
-
-  convert_expr(lhs);
-  convert_expr(rhs);
-
-  union_decay(lhs);
-  union_decay(rhs);
-
-  // Relations are special-cased in 1800-2017 11.8.2.
-  const typet new_type =
-    max_type(enum_decay(lhs.type()), enum_decay(rhs.type()));
-
-  if(new_type.is_nil())
-  {
-    throw errort().with_location(expr.source_location())
-      << "expected operands of compatible type but got:\n"
-      << "  " << to_string(lhs.type()) << '\n'
-      << "  " << to_string(rhs.type());
-  }
+  convert_expr(expr.lhs());
+  convert_expr(expr.rhs());
 
-  // If both operands are signed, both are sign-extended to the max width.
-  // Otherwise, both are zero-extended to the max width.
-  // In particular, signed operands are then _not_ sign extended,
-  // which a typecast would do.
-  if(new_type.id() == ID_verilog_unsignedbv || new_type.id() == ID_unsignedbv)
-  {
-    // zero extend both operands
-    lhs = zero_extend(lhs, new_type);
-    rhs = zero_extend(rhs, new_type);
-  }
-  else
-  {
-    // convert
-    implicit_typecast(lhs, new_type);
-    implicit_typecast(rhs, new_type);
-  }
+  // determine the max of the operand types and propagate it downwards
+  tc_binary_expr(expr);
 }
 
 /*******************************************************************\