bump CBMC dependency

src/ebmc/output_verilog.cpp

@@ -279,13 +279,11 @@ void output_verilog_rtlt::assign_symbol(
     auto &lhs_extractbits = to_extractbits_expr(lhs);
 
     // redundant?
-    mp_integer from, to;
+    mp_integer index;
 
-    if(
-      !to_integer_non_constant(lhs_extractbits.upper(), to) &&
-      !to_integer_non_constant(lhs_extractbits.lower(), from))
+    if(!to_integer_non_constant(lhs_extractbits.index(), index))
     {
-      if(from == 0 && to == width(lhs_extractbits.src().type()) - 1)
+      if(index == 0 && width(lhs_extractbits.src().type()) == width(lhs.type()))
       {
         assign_symbol(lhs_extractbits.src(), rhs);
         return;
@@ -429,25 +427,17 @@ std::string output_verilog_netlistt::symbol_string(const exprt &expr)
   else if(expr.id()==ID_extractbits)
   {
     auto &src = to_extractbits_expr(expr).src();
-    auto &upper = to_extractbits_expr(expr).upper();
-    auto &lower = to_extractbits_expr(expr).lower();
+    auto &index = to_extractbits_expr(expr).index();
 
     mp_integer from;
-    if(to_integer_non_constant(upper, from))
+    if(to_integer_non_constant(index, from))
     {
-      error().source_location = upper.find_source_location();
-      error() << "failed to convert constant " << upper.pretty() << eom;
-      throw 0;
-    }
-
-    mp_integer to;
-    if(to_integer_non_constant(lower, to))
-    {
-      error().source_location = lower.find_source_location();
-      error() << "failed to convert constant " << lower.pretty() << eom;
+      error().source_location = index.find_source_location();
+      error() << "failed to convert constant " << index.pretty() << eom;
       throw 0;
     }
 
+    auto to = from + width(expr.type());
     std::size_t offset = atoi(src.type().get("#offset").c_str());
 
     assert(from>=offset);

src/hw-cbmc/hw_cbmc_parse_options.cpp

@@ -15,10 +15,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/unicode.h>
 #include <util/version.h>
 
-#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/goto_verifier.h>
 #include <goto-checker/multi_path_symex_checker.h>

src/trans-netlist/trans_to_netlist.cpp

@@ -570,17 +570,12 @@ void convert_trans_to_netlistt::convert_lhs_rec(
   }
   else if(expr.id()==ID_extractbits)
   {
-    mp_integer new_from, new_to;
+    mp_integer new_from;
 
-    assert(expr.operands().size()==3);
-
-    if(
-      !to_integer_non_constant(to_extractbits_expr(expr).upper(), new_from) &&
-      !to_integer_non_constant(to_extractbits_expr(expr).lower(), new_to))
+    if(!to_integer_non_constant(to_extractbits_expr(expr).index(), new_from))
     {
-      if(new_from>new_to) std::swap(new_from, new_to);
-
-      assert(new_from<=new_to);
+      boolbv_widtht boolbv_width(ns);
+      mp_integer new_to = new_from + boolbv_width(expr.type());
 
       from = new_from.to_ulong();
       to = new_to.to_ulong();
@@ -747,19 +742,16 @@ void convert_trans_to_netlistt::add_equality_rec(
   }
   else if(lhs.id()==ID_extractbits)
   {
-    mp_integer op1, op2;
-
-    if(to_integer_non_constant(to_extractbits_expr(lhs).upper(), op1))
-      throw std::string("failed to convert extractbits upper");
+    mp_integer index;
 
-    if(to_integer_non_constant(to_extractbits_expr(lhs).lower(), op2))
-      throw std::string("failed to convert extractbits lower");
+    if(to_integer_non_constant(to_extractbits_expr(lhs).index(), index))
+      throw std::string("failed to convert extractbits index");
 
-    if(op1<op2)
-      throw std::string("extractbits op1<op2");
+    boolbv_widtht boolbv_width(ns);
 
-    std::size_t new_lhs_to = lhs_from + op1.to_ulong();
-    std::size_t new_lhs_from = lhs_from + op2.to_ulong();
+    std::size_t new_lhs_from = lhs_from + index.to_ulong();
+    std::size_t new_lhs_to =
+      lhs_from + index.to_ulong() + boolbv_width(lhs.type());
 
     add_equality_rec(
       src, to_extractbits_expr(lhs).src(), new_lhs_from, new_lhs_to, rhs_entry);

src/verilog/expr2verilog.cpp

@@ -640,10 +640,24 @@ std::string expr2verilogt::convert_extractbits(
   dest+=op;
   if(precedence>p) dest+=')';
 
+  auto width = to_bitvector_type(src.type()).get_width();
+
   dest+='[';
-  dest += convert(src.upper());
+
+  if(src.index().is_constant())
+  {
+    auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(src.index()));
+    dest += integer2string(index_int + width);
+  }
+  else
+  {
+    dest += convert(src.index());
+    dest += " + ";
+    dest += std::to_string(width);
+  }
+
   dest+=':';
-  dest += convert(src.lower());
+  dest += convert(src.index());
   dest+=']';
 
   return dest;

src/verilog/verilog_synthesis.cpp

@@ -144,10 +144,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
     // Construct the extractbits expression
     return extractbits_exprt{
-      src_padded,
-      from_integer(op1, integer_typet()),
-      from_integer(op2, integer_typet()),
-      expr.type()}
+      src_padded, from_integer(op2, integer_typet()), expr.type()}
       .with_source_location(expr.source_location());
   }
   else if(
@@ -187,10 +184,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
       }
 
       return extractbits_exprt{
-        std::move(src),
-        from_integer(top, integer_typet{}),
-        from_integer(bottom, integer_typet{}),
-        expr.type()}
+        std::move(src), from_integer(bottom, integer_typet{}), expr.type()}
         .with_source_location(expr);
     }
     else
@@ -203,10 +197,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
       auto src_shifted = lshr_exprt(src, index_adjusted);
 
       return extractbits_exprt{
-        std::move(src_shifted),
-        from_integer(width - 1, integer_typet{}),
-        from_integer(0, integer_typet{}),
-        expr.type()}
+        std::move(src_shifted), from_integer(0, integer_typet{}), expr.type()}
         .with_source_location(expr);
     }
   }
@@ -507,17 +498,11 @@ void verilog_synthesist::assignment_rec(
       else if(it->type().id()==ID_signedbv ||
               it->type().id()==ID_unsignedbv)
       {
-        auto width = get_width(it->type());
-
-        auto offset_constant2 =
-          from_integer(offset + width - 1, natural_typet{});
-
-        // extractbits requires that upper >= lower, i.e. op1 >= op2
-        extractbits_exprt bit_extract(rhs, offset_constant2, offset_constant,
-                                      it->type());
+        extractbits_exprt bit_extract(rhs, offset_constant, it->type());
 
         assignment_rec(*it, bit_extract, blocking);
 
+        auto width = get_width(it->type());
         offset+=width;
       }
       else
@@ -2006,9 +1991,7 @@ void verilog_synthesist::synth_force_rec(
               it->type().id()==ID_unsignedbv)
       {
         auto width = get_width(it->type());
-        auto sum_constant = from_integer(offset + width - 1, natural_typet{});
-        extractbits_exprt bit_extract(
-          rhs, offset_constant, sum_constant, it->type());
+        extractbits_exprt bit_extract(rhs, offset_constant, it->type());
         synth_force_rec(*it, bit_extract);
         offset+=width;
       }

src/vhdl/expr2vhdl.cpp

@@ -343,10 +343,24 @@ std::string expr2vhdlt::convert_extractbits(
   dest+=op;
   if(precedence>p) dest+=')';
 
+  auto width = to_bitvector_type(src.type()).get_width();
+
   dest+='[';
-  dest += convert(src.upper());
+
+  if(src.index().is_constant())
+  {
+    auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(src.index()));
+    dest += integer2string(index_int + width);
+  }
+  else
+  {
+    dest += convert(src.index());
+    dest += " + ";
+    dest += std::to_string(width);
+  }
+
   dest+=':';
-  dest += convert(src.lower());
+  dest += convert(src.index());
   dest+=']';
 
   return dest;