Verilog: use zero_extend_exprt

regression/ebmc/range_type/range_type1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 range_type1.smv
 --bound 10
 ^EXIT=0$

regression/ebmc/range_type/range_type4.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 range_type4.smv
 --bound 10
 ^EXIT=0$

regression/ebmc/traces/disjunction1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 disjunction1.smv
 --bound 20 --numbered-trace
 ^\[spec1\] G \(X FALSE \| X X FALSE\): REFUTED$

regression/smv/CTL/smv_ctlspec_F1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ctlspec_F1.smv
 --bound 10
 ^\[.*\] AF x = 0: REFUTED$

regression/smv/CTL/smv_ctlspec_G1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ctlspec_G1.smv
 --bound 10
 ^\[.*\] AG x != 5: PROVED up to bound 10$

regression/smv/LTL/smv_ltlspec6.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec6.smv
 
 ^EXIT=0$

regression/smv/LTL/smv_ltlspec_F1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_F1.smv
 --bound 10
 ^EXIT=10$

regression/smv/LTL/smv_ltlspec_F2.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_F2.smv
 --bound 10
 ^EXIT=10$

regression/smv/LTL/smv_ltlspec_F3.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_F3.smv
 --bound 10 --numbered-trace
 ^\[.*\] F x = 0: REFUTED$

regression/smv/LTL/smv_ltlspec_G1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_G1.smv
 --bound 10
 ^EXIT=10$

regression/smv/LTL/smv_ltlspec_G2.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_G2.smv
 --bound 10
 ^EXIT=10$

regression/smv/LTL/smv_ltlspec_G3.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_G3.smv
 --bound 10 --numbered-trace
 ^\[.*\] G X x != 3: REFUTED$

regression/smv/LTL/smv_ltlspec_R1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_R1.smv
 --bound 10
 ^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$

regression/smv/LTL/smv_ltlspec_R3.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_R3.smv
 --bound 1
 ^\[.*\] FALSE R x != 3: PROVED up to bound 1$

regression/smv/LTL/smv_ltlspec_R4.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_R4.smv
 --bound 10
 ^\[.*\] FALSE R x != 0: PROVED up to bound 10$

regression/smv/LTL/smv_ltlspec_U1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_U1.smv
 --bound 3
 \[.*\] TRUE U x = 3: PROVED up to bound 3$

regression/smv/LTL/smv_ltlspec_U2.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_U2.smv
 --bound 10 --numbered-trace
 ^\[.*\] TRUE U x = 0: REFUTED$

regression/smv/expressions/smv_if1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_if1.smv
 
 ^EXIT=0$

regression/verilog/assignments/assignment-to-concatenation1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 assignment-to-concatenation1.v
 --bound 1
 ^EXIT=0$

regression/verilog/assignments/assignment-to-index1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 assignment-to-index1.v
 --bound 1
 ^EXIT=0$

regression/verilog/generate/generate-for2.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 generate-for2.v
 --bound 0
 ^EXIT=0$

regression/verilog/generate/generate-reg1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 generate-reg1.v
 --module main --bound 0
 ^EXIT=0$

regression/verilog/generate1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/multiple_assign1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/part-select/indexed-part-select1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 indexed-part-select1.sv
 --bound 0
 ^EXIT=0$

regression/verilog/primitive_gates/nand1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 nand1.sv
 --bound 0
 ^EXIT=0$

regression/verilog/primitive_gates/xnor3.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 xnor3.sv
 --bound 0
 ^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED up to bound 0$

regression/verilog/system-functions/low1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 low1.sv
 --module main --bound 0
 ^EXIT=0$

src/ebmc/ebmc_parse_options.cpp

@@ -275,8 +275,7 @@ int ebmc_parse_optionst::doit()
         netlistt netlist;
         if(ebmc_base.make_netlist(netlist))
           return 1;
-        auto filename =
-          cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
+        auto filename = cmdline.value_opt("outfile").value_or("-");
         output_filet outfile{filename};
         outfile.stream() << "digraph netlist {\n";
         netlist.output_dot(outfile.stream());
@@ -289,8 +288,7 @@ int ebmc_parse_optionst::doit()
         netlistt netlist;
         if(ebmc_base.make_netlist(netlist))
           return 1;
-        auto filename =
-          cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
+        auto filename = cmdline.value_opt("outfile").value_or("-");
         output_filet outfile{filename};
         outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
         outfile.stream() << "-- Generated from "

src/hw_cbmc_irep_ids.h

@@ -238,7 +238,6 @@ IREP_ID_ONE(verilog_time)
 IREP_ID_ONE(verilog_iff)
 IREP_ID_ONE(verilog_implies)
 IREP_ID_ONE(offset)
-IREP_ID_ONE(xnor)
 IREP_ID_ONE(specify)
 IREP_ID_ONE(x)
 IREP_ID_ONE(verilog_empty_item)

src/verilog/aval_bval_encoding.cpp

@@ -392,3 +392,8 @@ 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 zero_extend_exprt &expr)
+{
+  abort();
+}

src/verilog/aval_bval_encoding.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_VERILOG_AVAL_BVAL_H
 #define CPROVER_VERILOG_AVAL_BVAL_H
 
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/mathematical_expr.h>
 
@@ -58,5 +59,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 zero extension
+exprt aval_bval(const zero_extend_exprt &);
 
 #endif

src/verilog/expr2verilog.cpp

@@ -773,6 +773,25 @@ expr2verilogt::resultt expr2verilogt::convert_explicit_size_cast(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_zero_extend
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt
+expr2verilogt::convert_zero_extend(const zero_extend_exprt &src)
+{
+  // added by the type checker; igore
+  return convert_rec(src.op());
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_index
 
   Inputs:
@@ -1546,6 +1565,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   else if(src.id()==ID_typecast)
     return convert_typecast(to_typecast_expr(src));
 
+  else if(src.id() == ID_zero_extend)
+    return convert_zero_extend(to_zero_extend_expr(src));
+
   else if(src.id()==ID_and)
     return convert_binary(
       to_multi_ary_expr(src), "&&", precedence = verilog_precedencet::AND);

src/verilog/expr2verilog_class.h

@@ -116,6 +116,8 @@ class expr2verilogt
 
   resultt convert_typecast(const typecast_exprt &);
 
+  resultt convert_zero_extend(const zero_extend_exprt &);
+
   resultt
   convert_explicit_size_cast(const class verilog_explicit_size_cast_exprt &);
 

src/verilog/verilog_lowering.cpp

@@ -399,6 +399,20 @@ exprt verilog_lowering(exprt expr)
     else
       return expr;
   }
+  else if(expr.id() == ID_zero_extend)
+  {
+    auto &zero_extend = to_zero_extend_expr(expr);
+
+    if(
+      is_four_valued(zero_extend.type()) ||
+      is_four_valued(zero_extend.op().type()))
+    {
+      // encode into aval/bval
+      return aval_bval(zero_extend);
+    }
+    else
+      return expr; // leave as is
+  }
   else
     return expr; // leave as is
 

src/verilog/verilog_synthesis.cpp

@@ -1572,11 +1572,9 @@ void verilog_synthesist::synth_module_instance_builtin(
       exprt op;
 
       if(instance.type().id() == ID_bool)
-        op = not_exprt{
-          multi_ary_exprt{ID_xor, std::move(operands), instance.type()}};
+        op = not_exprt{xor_exprt{std::move(operands)}};
       else
-        op = bitnot_exprt{
-          multi_ary_exprt{ID_bitxor, std::move(operands), instance.type()}};
+        op = bitnot_exprt{bitxor_exprt{std::move(operands), instance.type()}};
 
       equal_exprt constraint{output, std::move(op)};
       trans.invar().add_to_operands(std::move(constraint));

src/verilog/verilog_typecheck_expr.cpp

@@ -2094,23 +2094,14 @@ Function: zero_extend
 
 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);
+  exprt result = expr;
+
+  if(expr.type().id() == ID_bool)
+    result = typecast_exprt{expr, unsignedbv_typet{1}};
+  else if(expr.type().id() == ID_integer)
+    result = typecast_exprt{expr, unsignedbv_typet{32}};
 
-  return typecast_exprt::conditional_cast(
-    typecast_exprt::conditional_cast(expr, tmp_type), type);
+  return zero_extend_exprt{std::move(result), type};
 }
 
 /*******************************************************************\