Verilog: default aval/bval lowering

This introduces a default lowering for four-valued expressions.
If any operand has x/z, then the result is 'x'.

Otherwise, the result is the expression applied to the aval of the operands.

Author: kroening

regression/verilog/expressions/minus1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 minus1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The result is wrong.

regression/verilog/expressions/mult1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 mult1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The result is wrong.

regression/verilog/expressions/plus1.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 plus1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The result is wrong.

src/verilog/aval_bval_encoding.cpp

@@ -36,8 +36,7 @@ bv_typet aval_bval_type(std::size_t width, irep_idt source_type)
 
 bv_typet lower_to_aval_bval(const typet &src)
 {
-  PRECONDITION(
-    src.id() == ID_verilog_unsignedbv || src.id() == ID_verilog_signedbv);
+  PRECONDITION(is_four_valued(src));
   return aval_bval_type(to_bitvector_type(src).get_width(), src.id());
 }
 
@@ -75,9 +74,7 @@ typet aval_bval_underlying(const typet &src)
 
 constant_exprt lower_to_aval_bval(const constant_exprt &src)
 {
-  PRECONDITION(
-    src.type().id() == ID_verilog_signedbv ||
-    src.type().id() == ID_verilog_unsignedbv);
+  PRECONDITION(is_four_valued(src.type()));
 
   auto new_type = lower_to_aval_bval(src.type());
   auto width = aval_bval_width(new_type);
@@ -256,7 +253,7 @@ exprt has_xz(const exprt &expr)
     return false_exprt{}; // it's two-valued
 }
 
-/// return 'x', one bit, in aval_bval encoding
+/// return 'x'
 exprt make_x(const typet &type)
 {
   PRECONDITION(is_four_valued(type));
@@ -470,3 +467,33 @@ exprt aval_bval(const shift_exprt &expr)
   auto x = make_x(expr.type());
   return if_exprt{distance_has_xz, x, combined};
 }
+
+exprt default_aval_bval_lowering(const exprt &expr)
+{
+  auto &type = expr.type();
+
+  PRECONDITION(is_four_valued(type));
+
+  exprt::operandst disjuncts;
+  for(auto &op : expr.operands())
+    disjuncts.push_back(has_xz(op));
+
+  auto has_xz = disjunction(disjuncts);
+
+  exprt two_valued_expr = expr; // copy
+
+  for(auto &op : two_valued_expr.operands())
+    op = aval_underlying(op); // replace by aval
+
+  if(type.id() == ID_verilog_unsignedbv)
+    two_valued_expr.type() = unsignedbv_typet{to_bitvector_type(type).width()};
+  else if(type.id() == ID_verilog_signedbv)
+    two_valued_expr.type() = signedbv_typet{to_bitvector_type(type).width()};
+  else
+    PRECONDITION(false);
+
+  return if_exprt{
+    has_xz,
+    make_x(type),
+    aval_bval_conversion(two_valued_expr, lower_to_aval_bval(type))};
+}

src/verilog/aval_bval_encoding.h

@@ -66,4 +66,9 @@ exprt aval_bval(const typecast_exprt &);
 /// lowering for shifts
 exprt aval_bval(const shift_exprt &);
 
+/// If any operand has x/z, then the result is 'x'.
+/// Otherwise, the result is the expression applied to the aval
+/// of the operands.
+exprt default_aval_bval_lowering(const exprt &);
+
 #endif

src/verilog/verilog_lowering.cpp

@@ -614,9 +614,23 @@ exprt verilog_lowering(exprt expr)
     {
       // turn into floatbv
       expr.type() = verilog_lowering(expr.type());
+      return expr;
     }
-
-    return expr;
+    else if(is_four_valued(expr))
+    {
+      return default_aval_bval_lowering(expr);
+    }
+    else
+      return expr;
+  }
+  else if(
+    expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
+    expr.id() == ID_div || expr.id() == ID_mod)
+  {
+    if(is_four_valued(expr))
+      return default_aval_bval_lowering(expr);
+    else
+      return expr;
   }
   else if(expr.id() == ID_lshr || expr.id() == ID_ashr || expr.id() == ID_shl)
   {