Merge pull request #735 from diffblue/power1-fix

Verilog: four-valued power

regression/verilog/expressions/power1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE broken-smt-backend
 power1.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Lowering for power on three-valued logic is missing.

src/verilog/aval_bval_encoding.cpp

@@ -122,6 +122,22 @@ exprt aval(const exprt &src)
   }
 }
 
+exprt aval_underlying(const exprt &src)
+{
+  if(is_aval_bval(src.type()))
+  {
+    auto type = aval_bval_underlying(src.type());
+    if(type.id() == ID_bool)
+      return extractbit_exprt{src, 0};
+    else
+      return extractbits_exprt{src, 0, type};
+  }
+  else
+  {
+    return src;
+  }
+}
+
 exprt bval(const exprt &src)
 {
   if(is_aval_bval(src.type()))
@@ -225,10 +241,11 @@ exprt has_xz(const exprt &expr)
 }
 
 /// return 'x', one bit
-exprt make_x()
+exprt make_x(const typet &type)
 {
-  auto type = verilog_unsignedbv_typet{1};
-  return lower_to_aval_bval(constant_exprt{ID_x, type});
+  PRECONDITION(is_four_valued(type));
+  auto width = to_bitvector_type(type).get_width();
+  return lower_to_aval_bval(constant_exprt{std::string(width, 'x'), type});
 }
 
 exprt aval_bval(const verilog_logical_equality_exprt &expr)
@@ -239,7 +256,9 @@ exprt aval_bval(const verilog_logical_equality_exprt &expr)
   auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())};
   auto equality = equal_exprt{expr.lhs(), expr.rhs()};
   return if_exprt{
-    has_xz, make_x(), aval_bval_conversion(equality, lower_to_aval_bval(type))};
+    has_xz,
+    make_x(type),
+    aval_bval_conversion(equality, lower_to_aval_bval(type))};
 }
 
 exprt aval_bval(const verilog_logical_inequality_exprt &expr)
@@ -250,7 +269,9 @@ exprt aval_bval(const verilog_logical_inequality_exprt &expr)
   auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())};
   auto equality = notequal_exprt{expr.lhs(), expr.rhs()};
   return if_exprt{
-    has_xz, make_x(), aval_bval_conversion(equality, lower_to_aval_bval(type))};
+    has_xz,
+    make_x(type),
+    aval_bval_conversion(equality, lower_to_aval_bval(type))};
 }
 
 exprt aval_bval(const verilog_wildcard_equality_exprt &expr)
@@ -289,12 +310,26 @@ exprt aval_bval(const verilog_wildcard_inequality_exprt &expr)
 
 exprt aval_bval(const not_exprt &expr)
 {
-  PRECONDITION(is_four_valued(expr.type()));
+  auto &type = expr.type();
+  PRECONDITION(is_four_valued(type));
   PRECONDITION(is_aval_bval(expr.op()));
 
   auto has_xz = ::has_xz(expr.op());
   auto not_expr =
     not_exprt{extractbit_exprt{expr.op(), natural_typet{}.zero_expr()}};
-  auto x = make_x();
+  auto x = make_x(type);
   return if_exprt{has_xz, x, aval_bval_conversion(not_expr, x.type())};
 }
+
+exprt aval_bval(const power_exprt &expr)
+{
+  PRECONDITION(is_four_valued(expr.type()));
+  PRECONDITION(is_aval_bval(expr.lhs()));
+  PRECONDITION(is_aval_bval(expr.rhs()));
+
+  auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())};
+  auto power_expr =
+    power_exprt{aval_underlying(expr.lhs()), aval_underlying(expr.rhs())};
+  auto x = make_x(expr.type());
+  return if_exprt{has_xz, x, aval_bval_conversion(power_expr, x.type())};
+}

src/verilog/aval_bval_encoding.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_VERILOG_AVAL_BVAL_H
 
 #include <util/bitvector_types.h>
+#include <util/mathematical_expr.h>
 
 #include "verilog_expr.h"
 
@@ -47,5 +48,7 @@ exprt aval_bval(const not_exprt &);
 exprt aval_bval(const verilog_wildcard_equality_exprt &);
 /// lowering for !=?
 exprt aval_bval(const verilog_wildcard_inequality_exprt &);
+/// lowering for **
+exprt aval_bval(const power_exprt &);
 
 #endif

src/verilog/verilog_synthesis.cpp

@@ -246,28 +246,35 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
   }
   else if(expr.id() == ID_power)
   {
-    auto &power_expr = to_binary_expr(expr);
+    auto &power_expr = to_power_expr(expr);
     DATA_INVARIANT(
       power_expr.lhs().type() == power_expr.type(),
       "power expression type consistency");
     power_expr.lhs() = synth_expr(power_expr.lhs(), symbol_state);
     power_expr.rhs() = synth_expr(power_expr.rhs(), symbol_state);
-    auto rhs_int = numeric_cast<std::size_t>(power_expr.rhs());
-    if(rhs_int.has_value())
+
+    // encode into aval/bval
+    if(is_four_valued(expr.type()))
+      return aval_bval(power_expr);
+    else
     {
-      if(*rhs_int == 0)
-        return from_integer(1, expr.type());
-      else if(*rhs_int == 1)
-        return power_expr.lhs();
-      else // >= 2
+      auto rhs_int = numeric_cast<std::size_t>(power_expr.rhs());
+      if(rhs_int.has_value())
       {
-        auto factors = exprt::operandst{rhs_int.value(), power_expr.lhs()};
-        // would prefer appropriate mult_exprt constructor
-        return multi_ary_exprt{ID_mult, factors, expr.type()};
+        if(*rhs_int == 0)
+          return from_integer(1, expr.type());
+        else if(*rhs_int == 1)
+          return power_expr.lhs();
+        else // >= 2
+        {
+          auto factors = exprt::operandst{rhs_int.value(), power_expr.lhs()};
+          // would prefer appropriate mult_exprt constructor
+          return multi_ary_exprt{ID_mult, factors, expr.type()};
+        }
       }
+      else
+        return expr;
     }
-    else
-      return expr;
   }
   else if(expr.id()==ID_typecast)
   {

src/verilog/verilog_typecheck_base.cpp

@@ -265,3 +265,44 @@ typet verilog_typecheck_baset::index_type(const array_typet &array_type)
   return unsignedbv_typet(address_bits(
       (array_size(array_type) + array_offset(array_type)).to_ulong()));
 }
+
+/*******************************************************************\
+
+Function: verilog_typecheck_baset::is_four_valued
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool verilog_typecheck_baset::is_four_valued(const typet &type)
+{
+  return type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv;
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_baset::four_valued
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet verilog_typecheck_baset::four_valued(const typet &type)
+{
+  if(type.id() == ID_signedbv)
+    return verilog_signedbv_typet{to_signedbv_type(type).get_width()};
+  else if(type.id() == ID_unsignedbv)
+    return verilog_unsignedbv_typet{to_unsignedbv_type(type).get_width()};
+  else if(type.id() == ID_bool)
+    return verilog_unsignedbv_typet{1};
+  else
+    return type;
+}

src/verilog/verilog_typecheck_base.h

@@ -55,6 +55,13 @@ class verilog_typecheck_baset:public typecheckt
   static mp_integer array_size(const array_typet &);
   static mp_integer array_offset(const array_typet &);
   static typet index_type(const array_typet &);
+
+  /// is the given type four-valued?
+  static bool is_four_valued(const typet &);
+
+  /// create the four-valued type with same width and signedness
+  /// as the given type
+  static typet four_valued(const typet &);
 };
 
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/bitvector_expr.h>
 #include <util/ebmc_util.h>
 #include <util/expr_util.h>
+#include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
@@ -123,14 +124,11 @@ void verilog_typecheck_exprt::propagate_type(
      expr.has_operands())
   {
     // arithmetic
-
-    if(expr.id()==ID_plus ||
-       expr.id()==ID_minus ||
-       expr.id()==ID_mult || 
-       expr.id()==ID_div || 
-       expr.id()==ID_power ||
-       expr.id()==ID_unary_minus ||
-       expr.id()==ID_unary_plus)
+
+    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)
       {
@@ -2611,6 +2609,44 @@ Function: verilog_typecheck_exprt::convert_shl_expr
 
 \*******************************************************************/
 
+exprt verilog_typecheck_exprt::convert_power_expr(power_exprt expr)
+{
+  convert_expr(expr.op0());
+  convert_expr(expr.op1());
+
+  no_bool_ops(expr);
+
+  // Is one of the operands four-valued?
+  if(is_four_valued(expr.op0().type()))
+  {
+    // We make the other operand also four-valued, if needed
+    expr.op1() = typecast_exprt{expr.op1(), four_valued(expr.op1().type())};
+  }
+  else if(is_four_valued(expr.op1().type()))
+  {
+    // We make the other operand also four-valued, if needed
+    expr.op0() = typecast_exprt{expr.op0(), four_valued(expr.op0().type())};
+  }
+
+  // 1800-2017 Table 11-21
+  // The width of a power is the width of the left operand
+  expr.type() = expr.op0().type();
+
+  return std::move(expr);
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::convert_shl_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 exprt verilog_typecheck_exprt::convert_shl_expr(shl_exprt expr)
 {
   convert_expr(expr.op0());
@@ -2760,6 +2796,8 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_power)
+    return convert_power_expr(to_power_expr(expr));
   else if(expr.id()==ID_shl)
     return convert_shl_expr(to_shl_expr(expr));
   else if(expr.id()==ID_shr)

src/verilog/verilog_typecheck_expr.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <stack>
 
 class function_call_exprt;
+class power_exprt;
 
 class verilog_typecheck_exprt:public verilog_typecheck_baset
 {
@@ -168,6 +169,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   convert_system_function(const irep_idt &identifier, function_call_exprt);
   [[nodiscard]] exprt convert_bit_select_expr(binary_exprt);
   [[nodiscard]] exprt convert_replication_expr(replication_exprt);
+  [[nodiscard]] exprt convert_power_expr(power_exprt);
   [[nodiscard]] exprt convert_shl_expr(shl_exprt);
   void implicit_typecast(exprt &, const typet &type);
   void tc_binary_expr(exprt &);