Merge pull request #8182 from diffblue/update_bits_exprt

update_bits_exprt

Author: kroening

src/solvers/Makefile

@@ -128,6 +128,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_unary_minus.cpp \
       flattening/boolbv_union.cpp \
       flattening/boolbv_update.cpp \
+      flattening/boolbv_update_bits.cpp \
       flattening/boolbv_width.cpp \
       flattening/boolbv_with.cpp \
       flattening/bv_dimacs.cpp \

src/solvers/flattening/boolbv.h

@@ -39,6 +39,7 @@ class overflow_result_exprt;
 class replication_exprt;
 class unary_overflow_exprt;
 class union_typet;
+class update_bits_exprt;
 
 class boolbvt:public arrayst
 {
@@ -176,6 +177,7 @@ class boolbvt:public arrayst
   virtual bvt convert_member(const member_exprt &expr);
   virtual bvt convert_with(const with_exprt &expr);
   virtual bvt convert_update(const update_exprt &);
+  virtual bvt convert_update_bits(const update_bits_exprt &);
   virtual bvt convert_case(const exprt &expr);
   virtual bvt convert_cond(const cond_exprt &);
   virtual bvt convert_shift(const binary_exprt &expr);
@@ -196,36 +198,38 @@ class boolbvt:public arrayst
   virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
   virtual bvt convert_overflow_result(const overflow_result_exprt &expr);
 
+  bvt convert_update_bits(bvt src, const exprt &index, const bvt &new_value);
+
   void convert_with(
     const typet &type,
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &where,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_bv(
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &index,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_array(
     const array_typet &type,
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &index,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_union(
     const union_typet &type,
-    const exprt &op2,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 
   void convert_with_struct(
     const struct_typet &type,
-    const exprt &op1,
-    const exprt &op2,
+    const exprt &where,
+    const exprt &new_value,
     const bvt &prev_bv,
     bvt &next_bv);
 

src/solvers/flattening/boolbv_update_bits.cpp

@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/bitvector_expr.h>
+
+#include "boolbv.h"
+
+bvt boolbvt::convert_update_bits(const update_bits_exprt &expr)
+{
+  return convert_bv(expr.lower());
+}

src/solvers/flattening/boolbv_with.cpp

@@ -6,18 +6,30 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include "boolbv.h"
-
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
+#include "boolbv.h"
+
 bvt boolbvt::convert_with(const with_exprt &expr)
 {
+  auto &type = expr.type();
+
+  if(
+    type.id() == ID_bv || type.id() == ID_unsignedbv ||
+    type.id() == ID_signedbv)
+  {
+    PRECONDITION(expr.operands().size() == 3);
+    return convert_bv(
+      update_bits_exprt(expr.old(), expr.where(), expr.new_value()));
+  }
+
   bvt bv = convert_bv(expr.old());
 
-  std::size_t width=boolbv_width(expr.type());
+  std::size_t width = boolbv_width(type);
 
   if(width==0)
   {
@@ -47,8 +59,8 @@ bvt boolbvt::convert_with(const with_exprt &expr)
 
 void boolbvt::convert_with(
   const typet &type,
-  const exprt &op1,
-  const exprt &op2,
+  const exprt &where,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
@@ -57,31 +69,43 @@ void boolbvt::convert_with(
   next_bv.resize(prev_bv.size());
 
   if(type.id()==ID_array)
-    return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
+    return convert_with_array(
+      to_array_type(type), where, new_value, prev_bv, next_bv);
   else if(type.id()==ID_bv ||
           type.id()==ID_unsignedbv ||
           type.id()==ID_signedbv)
-    return convert_with_bv(op1, op2, prev_bv, next_bv);
+  {
+    // already done
+    PRECONDITION(false);
+  }
   else if(type.id()==ID_struct)
-    return
-      convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
+    return convert_with_struct(
+      to_struct_type(type), where, new_value, prev_bv, next_bv);
   else if(type.id() == ID_struct_tag)
     return convert_with(
-      ns.follow_tag(to_struct_tag_type(type)), op1, op2, prev_bv, next_bv);
+      ns.follow_tag(to_struct_tag_type(type)),
+      where,
+      new_value,
+      prev_bv,
+      next_bv);
   else if(type.id()==ID_union)
-    return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
+    return convert_with_union(to_union_type(type), new_value, prev_bv, next_bv);
   else if(type.id() == ID_union_tag)
     return convert_with(
-      ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
+      ns.follow_tag(to_union_tag_type(type)),
+      where,
+      new_value,
+      prev_bv,
+      next_bv);
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
     false, "unexpected with type", irep_pretty_diagnosticst{type});
 }
 
 void boolbvt::convert_with_array(
   const array_typet &type,
-  const exprt &op1,
-  const exprt &op2,
+  const exprt &index,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
@@ -100,89 +124,60 @@ void boolbvt::convert_with_array(
     "convert_with_array expects constant array size",
     irep_pretty_diagnosticst{type});
 
-  const bvt &op2_bv=convert_bv(op2);
+  const bvt &new_value_bv = convert_bv(new_value);
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    *size * op2_bv.size() == prev_bv.size(),
-    "convert_with_array: unexpected operand 2 width",
+    *size * new_value_bv.size() == prev_bv.size(),
+    "convert_with_array: unexpected new_value operand width",
     irep_pretty_diagnosticst{type});
 
   // Is the index a constant?
-  if(const auto op1_value = numeric_cast<mp_integer>(op1))
+  if(const auto index_value_opt = numeric_cast<mp_integer>(index))
   {
     // Yes, it is!
     next_bv=prev_bv;
 
-    if(*op1_value >= 0 && *op1_value < *size) // bounds check
+    if(*index_value_opt >= 0 && *index_value_opt < *size) // bounds check
     {
       const std::size_t offset =
-        numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
+        numeric_cast_v<std::size_t>(*index_value_opt * new_value_bv.size());
 
-      for(std::size_t j=0; j<op2_bv.size(); j++)
-        next_bv[offset+j]=op2_bv[j];
+      for(std::size_t j = 0; j < new_value_bv.size(); j++)
+        next_bv[offset + j] = new_value_bv[j];
     }
 
     return;
   }
 
-  typet counter_type=op1.type();
+  typet counter_type = index.type();
 
   for(mp_integer i=0; i<size; i=i+1)
   {
     exprt counter=from_integer(i, counter_type);
 
-    literalt eq_lit=convert(equal_exprt(op1, counter));
-
-    const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
-
-    for(std::size_t j=0; j<op2_bv.size(); j++)
-      next_bv[offset+j]=
-        prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
-  }
-}
-
-void boolbvt::convert_with_bv(
-  const exprt &op1,
-  const exprt &op2,
-  const bvt &prev_bv,
-  bvt &next_bv)
-{
-  literalt l=convert(op2);
-
-  if(const auto op1_value = numeric_cast<mp_integer>(op1))
-  {
-    next_bv=prev_bv;
-
-    if(*op1_value < next_bv.size())
-      next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
-
-    return;
-  }
-
-  typet counter_type=op1.type();
-
-  for(std::size_t i=0; i<prev_bv.size(); i++)
-  {
-    exprt counter=from_integer(i, counter_type);
+    literalt eq_lit = convert(equal_exprt(index, counter));
 
-    literalt eq_lit=convert(equal_exprt(op1, counter));
+    const std::size_t offset =
+      numeric_cast_v<std::size_t>(i * new_value_bv.size());
 
-    next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
+    for(std::size_t j = 0; j < new_value_bv.size(); j++)
+      next_bv[offset + j] =
+        prop.lselect(eq_lit, new_value_bv[j], prev_bv[offset + j]);
   }
 }
 
 void boolbvt::convert_with_struct(
   const struct_typet &type,
-  const exprt &op1,
-  const exprt &op2,
+  const exprt &where,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
   next_bv=prev_bv;
 
-  const bvt &op2_bv=convert_bv(op2);
+  const bvt &new_value_bv = convert_bv(new_value);
 
-  const irep_idt &component_name=op1.get(ID_component_name);
+  const irep_idt &component_name = where.get(ID_component_name);
   const struct_typet::componentst &components=
     type.components();
 
@@ -197,19 +192,19 @@ void boolbvt::convert_with_struct(
     if(c.get_name() == component_name)
     {
       DATA_INVARIANT_WITH_DIAGNOSTICS(
-        subtype == op2.type(),
+        subtype == new_value.type(),
         "with/struct: component '" + id2string(component_name) +
           "' type does not match",
         irep_pretty_diagnosticst{subtype},
-        irep_pretty_diagnosticst{op2.type()});
+        irep_pretty_diagnosticst{new_value.type()});
 
       DATA_INVARIANT_WITH_DIAGNOSTICS(
-        sub_width == op2_bv.size(),
-        "convert_with_struct: unexpected operand op2 width",
+        sub_width == new_value_bv.size(),
+        "convert_with_struct: unexpected new_value operand width",
         irep_pretty_diagnosticst{type});
 
       for(std::size_t i=0; i<sub_width; i++)
-        next_bv[offset+i]=op2_bv[i];
+        next_bv[offset + i] = new_value_bv[i];
 
       break; // done
     }
@@ -220,22 +215,22 @@ void boolbvt::convert_with_struct(
 
 void boolbvt::convert_with_union(
   const union_typet &type,
-  const exprt &op2,
+  const exprt &new_value,
   const bvt &prev_bv,
   bvt &next_bv)
 {
   next_bv=prev_bv;
 
-  const bvt &op2_bv=convert_bv(op2);
+  const bvt &new_value_bv = convert_bv(new_value);
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    next_bv.size() >= op2_bv.size(),
-    "convert_with_union: unexpected operand op2 width",
+    next_bv.size() >= new_value_bv.size(),
+    "convert_with_union: unexpected new_value operand width",
     irep_pretty_diagnosticst{type});
 
   endianness_mapt map_u = endianness_map(type);
-  endianness_mapt map_op2 = endianness_map(op2.type());
+  endianness_mapt map_new_value = endianness_map(new_value.type());
 
-  for(std::size_t i = 0; i < op2_bv.size(); i++)
-    next_bv[map_u.map_bit(i)] = op2_bv[map_op2.map_bit(i)];
+  for(std::size_t i = 0; i < new_value_bv.size(); i++)
+    next_bv[map_u.map_bit(i)] = new_value_bv[map_new_value.map_bit(i)];
 }