aval/bval encoding for shifts

This adds an aval/bval encoding for four-valued shift expressions to the
Verilog frontend.

Author: kroening

src/verilog/aval_bval_encoding.cpp

@@ -444,3 +444,29 @@ exprt aval_bval(const typecast_exprt &expr)
   auto op_aval_zero = to_bv_type(op_aval.type()).all_zeros_expr();
   return and_exprt{not_exprt{op_has_xz}, notequal_exprt{op_aval, op_aval_zero}};
 }
+
+exprt aval_bval(const shift_exprt &expr)
+{
+  PRECONDITION(is_four_valued(expr.type()));
+
+  auto distance_has_xz = has_xz(expr.distance());
+  auto distance_aval = aval(expr.distance());
+
+  // the shift distance must have a numerical interpretation
+  auto distance_aval_casted = typecast_exprt{
+    distance_aval,
+    unsignedbv_typet{to_bitvector_type(distance_aval.type()).get_width()}};
+
+  // shift aval and bval separately
+  auto op_aval = aval(expr.op());
+  auto op_bval = bval(expr.op());
+
+  auto aval_shifted = shift_exprt{op_aval, expr.id(), distance_aval_casted};
+  auto bval_shifted = shift_exprt{op_bval, expr.id(), distance_aval_casted};
+
+  auto combined = combine_aval_bval(
+    aval_shifted, bval_shifted, lower_to_aval_bval(expr.type()));
+
+  auto x = make_x(expr.type());
+  return if_exprt{distance_has_xz, x, combined};
+}

src/verilog/aval_bval_encoding.h

@@ -63,5 +63,7 @@ exprt aval_bval(const verilog_iff_exprt &);
 exprt aval_bval(const verilog_implies_exprt &);
 /// lowering for typecasts
 exprt aval_bval(const typecast_exprt &);
+/// lowering for shifts
+exprt aval_bval(const shift_exprt &);
 
 #endif

src/verilog/verilog_lowering.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include "verilog_expr.h"
 #include "verilog_types.h"
 
+#include <iostream>
+
 /// Lowers
 /// * the three Verilog real types to floatbv;
 /// * Verilog integer to signedbv[32]
@@ -608,6 +610,13 @@ exprt verilog_lowering(exprt expr)
 
     return expr;
   }
+  else if(expr.id() == ID_lshr || expr.id() == ID_ashr || expr.id() == ID_shl)
+  {
+    if(is_four_valued(expr.type()))
+      return aval_bval(to_shift_expr(expr));
+    else
+      return expr;
+  }
   else
     return expr; // leave as is
 

src/verilog/verilog_typecheck_expr.cpp

@@ -2868,15 +2868,22 @@ Function: verilog_typecheck_exprt::convert_shl_expr
 
 exprt verilog_typecheck_exprt::convert_shl_expr(shl_exprt expr)
 {
-  convert_expr(expr.op0());
-  convert_expr(expr.op1());
-  
+  convert_expr(expr.lhs());
+  convert_expr(expr.rhs());
+
   no_bool_ops(expr);
 
-  // the bit width of a shift is always the bit width of the left operand
-  const typet &op0_type=expr.op0().type();
-  
-  expr.type()=op0_type;
+  const typet &lhs_type = expr.lhs().type();
+  const typet &rhs_type = expr.rhs().type();
+
+  // The bit width of a shift is always the bit width of the left operand.
+  // The result is four-valued if either of the operands is four-valued.
+  if(is_four_valued(lhs_type))
+    expr.type() = lhs_type;
+  else if(is_four_valued(rhs_type))
+    expr.type() = four_valued(lhs_type);
+  else
+    expr.type() = lhs_type;
 
   return std::move(expr);
 }
@@ -3066,16 +3073,26 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     must_be_integral(expr.rhs());
     no_bool_ops(expr);
 
-    const typet &op0_type = expr.op0().type();
+    const typet &lhs_type = expr.lhs().type();
+    const typet &rhs_type = expr.rhs().type();
 
     if(
-      op0_type.id() == ID_signedbv || op0_type.id() == ID_verilog_signedbv ||
-      op0_type.id() == ID_integer)
+      lhs_type.id() == ID_signedbv || lhs_type.id() == ID_verilog_signedbv ||
+      lhs_type.id() == ID_integer)
+    {
       expr.id(ID_ashr);
+    }
     else
       expr.id(ID_lshr);
 
-    expr.type()=op0_type;
+    // The bit width of a shift is always the bit width of the left operand.
+    // The result is four-valued if either of the operands is four-valued.
+    if(is_four_valued(lhs_type))
+      expr.type() = lhs_type;
+    else if(is_four_valued(rhs_type))
+      expr.type() = four_valued(lhs_type);
+    else
+      expr.type() = lhs_type;
 
     return std::move(expr);
   }
@@ -3092,7 +3109,18 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     must_be_integral(expr.lhs());
     must_be_integral(expr.rhs());
     no_bool_ops(expr);
-    expr.type()=expr.op0().type();
+
+    const typet &lhs_type = expr.lhs().type();
+    const typet &rhs_type = expr.rhs().type();
+
+    // The bit width of a shift is always the bit width of the left operand.
+    // The result is four-valued if either of the operands is four-valued.
+    if(is_four_valued(lhs_type))
+      expr.type() = lhs_type;
+    else if(is_four_valued(rhs_type))
+      expr.type() = four_valued(lhs_type);
+    else
+      expr.type() = lhs_type;
 
     return std::move(expr);
   }