Merge pull request #783 from diffblue/avalbval-to-bool

Verilog: aval/bval lowering for casts to Bool

regression/verilog/SVA/sequence5.desc

@@ -1,14 +1,12 @@
-KNOWNBUG
+CORE broken-smt-backend
 sequence5.sv
 --bound 0
 ^\[main\.p0\] 1: PROVED up to bound 0$
 ^\[main\.p1\] 0: REFUTED$
-^\[main\.p2\] 1'bx: PROVED up to bound 0$
-^\[main\.p3\] 1'bz: PROVED up to bound 0$
+^\[main\.p2\] 1'bx: REFUTED$
+^\[main\.p3\] 1'bz: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-x and z are recognized as 'true', but 'true' is defined as a "nonzero known
-value" (1800-2017 12.4).

regression/verilog/SVA/sva_and1.desc

@@ -3,7 +3,7 @@ sva_and1.sv
 --bound 0
 ^\[main\.p0\] always \(1 and 1\): PROVED up to bound 0$
 ^\[main\.p1\] always \(1 and 0\): REFUTED$
-^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): PROVED up to bound 0$
+^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sva_iff1.desc

@@ -3,7 +3,7 @@ sva_iff1.sv
 --bound 0
 ^\[main\.p0\] always \(1 iff 1\): PROVED up to bound 0$
 ^\[main\.p1\] always \(1 iff 0\): REFUTED$
-^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): PROVED up to bound 0$
+^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sva_implies1.desc

@@ -3,7 +3,7 @@ sva_implies1.sv
 --bound 0
 ^\[main\.p0\] always \(1 implies 1\): PROVED up to bound 0$
 ^\[main\.p1\] always \(1 implies 0\): REFUTED$
-^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): PROVED up to bound 0$
+^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/verilog/aval_bval_encoding.cpp

@@ -21,6 +21,11 @@ bool is_four_valued(const typet &type)
   return type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv;
 }
 
+bool is_four_valued(const exprt &expr)
+{
+  return is_four_valued(expr.type());
+}
+
 bv_typet aval_bval_type(std::size_t width, irep_idt source_type)
 {
   PRECONDITION(!source_type.empty());
@@ -333,3 +338,15 @@ exprt aval_bval(const power_exprt &expr)
   auto x = make_x(expr.type());
   return if_exprt{has_xz, x, aval_bval_conversion(power_expr, x.type())};
 }
+
+exprt aval_bval(const typecast_exprt &expr)
+{
+  // 'true' is defined as a "nonzero known value" (1800-2017 12.4).
+  PRECONDITION(is_aval_bval(expr.op()));
+  PRECONDITION(expr.type().id() == ID_bool);
+
+  auto op_has_xz = ::has_xz(expr.op());
+  auto op_aval = aval(expr.op());
+  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}};
+}

src/verilog/aval_bval_encoding.h

@@ -24,7 +24,9 @@ Author: Daniel Kroening, [email protected]
 //   1    1  |   Z
 
 bool is_four_valued(const typet &);
+bool is_four_valued(const exprt &);
 bool is_aval_bval(const typet &);
+bool is_aval_bval(const exprt &);
 std::size_t aval_bval_width(const typet &);
 typet aval_bval_underlying(const typet &);
 
@@ -50,5 +52,7 @@ exprt aval_bval(const verilog_wildcard_equality_exprt &);
 exprt aval_bval(const verilog_wildcard_inequality_exprt &);
 /// lowering for **
 exprt aval_bval(const power_exprt &);
+/// lowering for typecasts
+exprt aval_bval(const typecast_exprt &);
 
 #endif

src/verilog/verilog_synthesis.cpp

@@ -304,6 +304,13 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
   }
   else if(expr.id()==ID_typecast)
   {
+    // When casting a four-valued scalar to bool,
+    // 'true' is defined as a "nonzero known value" (1800-2017 12.4).
+    if(is_aval_bval(to_typecast_expr(expr).op()) && expr.type().id() == ID_bool)
+    {
+      expr = aval_bval(to_typecast_expr(expr));
+    }
+    else
     {
       auto &op = to_typecast_expr(expr).op();