Use diagnostics in boolbvt

instead of throw 0.

Author: peterschrammel

src/solvers/flattening/boolbv.cpp

@@ -191,7 +191,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_member)
     return convert_member(to_member_expr(expr));
   else if(expr.id()==ID_with)
-    return convert_with(expr);
+    return convert_with(to_with_expr(expr));
   else if(expr.id()==ID_update)
     return convert_update(expr);
   else if(expr.id()==ID_width)

src/solvers/flattening/boolbv.h

@@ -159,7 +159,7 @@ class boolbvt:public arrayst
   virtual bvt convert_floatbv_op(const exprt &expr);
   virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr);
   virtual bvt convert_member(const member_exprt &expr);
-  virtual bvt convert_with(const exprt &expr);
+  virtual bvt convert_with(const with_exprt &expr);
   virtual bvt convert_update(const exprt &expr);
   virtual bvt convert_case(const exprt &expr);
   virtual bvt convert_cond(const cond_exprt &);

src/solvers/flattening/boolbv_constant.cpp

@@ -31,13 +31,10 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
     {
       const bvt &tmp=convert_bv(*it);
 
-      if(tmp.size()!=op_width)
-      {
-        log.error().source_location = expr.find_source_location();
-        log.error() << "convert_constant: unexpected operand width"
-                    << messaget::eom;
-        throw 0;
-      }
+      DATA_INVARIANT_WITH_DIAGNOSTICS(
+        tmp.size() == op_width,
+        "convert_constant: unexpected operand width",
+        irep_pretty_diagnosticst{expr});
 
       for(std::size_t j=0; j<op_width; j++)
         bv[offset+j]=tmp[j];
@@ -100,13 +97,10 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
   {
     const std::string &binary=id2string(expr.get_value());
 
-    if(binary.size()*2!=width)
-    {
-      log.error().source_location = expr.find_source_location();
-      log.error() << "wrong value length in constant: " << expr.pretty()
-                  << messaget::eom;
-      throw 0;
-    }
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      binary.size() * 2 == width,
+      "wrong value length in constant",
+      irep_pretty_diagnosticst{expr});
 
     for(std::size_t i=0; i<binary.size(); i++)
     {
@@ -136,10 +130,10 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
         break;
 
       default:
-        log.error().source_location = expr.find_source_location();
-        log.error() << "unknown character in Verilog constant:" << expr.pretty()
-                    << messaget::eom;
-        throw 0;
+        DATA_INVARIANT_WITH_DIAGNOSTICS(
+          false,
+          "unknown character in Verilog constant",
+          irep_pretty_diagnosticst{expr});
       }
     }
 

src/solvers/flattening/boolbv_with.cpp

@@ -15,23 +15,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "bv_endianness_map.h"
 
-bvt boolbvt::convert_with(const exprt &expr)
+bvt boolbvt::convert_with(const with_exprt &expr)
 {
-  if(expr.operands().size()<3)
-  {
-    log.error().source_location = expr.find_source_location();
-    log.error() << "with takes at least three operands" << messaget::eom;
-    throw 0;
-  }
-
-  if((expr.operands().size()%2)!=1)
-  {
-    log.error().source_location = expr.find_source_location();
-    log.error() << "with takes an odd number of operands" << messaget::eom;
-    throw 0;
-  }
-
-  bvt bv=convert_bv(expr.op0());
+  bvt bv = convert_bv(expr.old());
 
   std::size_t width=boolbv_width(expr.type());
 
@@ -44,12 +30,10 @@ bvt boolbvt::convert_with(const exprt &expr)
       return conversion_failed(expr);
   }
 
-  if(bv.size()!=width)
-  {
-    log.error().source_location = expr.find_source_location();
-    log.error() << "unexpected operand 0 width" << messaget::eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    bv.size() == width,
+    "unexpected operand 0 width",
+    irep_pretty_diagnosticst{expr});
 
   bvt prev_bv;
   prev_bv.resize(width);
@@ -60,12 +44,7 @@ bvt boolbvt::convert_with(const exprt &expr)
   {
     bv.swap(prev_bv);
 
-    convert_with(
-      expr.op0().type(),
-      ops[op_no],
-      ops[op_no+1],
-      prev_bv,
-      bv);
+    convert_with(expr.old().type(), ops[op_no], ops[op_no + 1], prev_bv, bv);
   }
 
   return bv;
@@ -100,9 +79,8 @@ void boolbvt::convert_with(
     return convert_with(
       ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
 
-  log.error().source_location = type.source_location();
-  log.error() << "unexpected with type: " << type.id() << messaget::eom;
-  throw 0;
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    false, "unexpected with type", irep_pretty_diagnosticst{type});
 }
 
 void boolbvt::convert_with_array(
@@ -112,36 +90,27 @@ void boolbvt::convert_with_array(
   const bvt &prev_bv,
   bvt &next_bv)
 {
-  if(is_unbounded_array(type))
-  {
-    // can't do this
-    log.error().source_location = type.source_location();
-    log.error() << "convert_with_array called for unbounded array"
-                << messaget::eom;
-    throw 0;
-  }
+  // can't do this
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    !is_unbounded_array(type),
+    "convert_with_array called for unbounded array",
+    irep_pretty_diagnosticst{type});
 
   const exprt &array_size=type.size();
 
   const auto size = numeric_cast<mp_integer>(array_size);
 
-  if(!size.has_value())
-  {
-    log.error().source_location = type.source_location();
-    log.error() << "convert_with_array expects constant array size"
-                << messaget::eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    size.has_value(),
+    "convert_with_array expects constant array size",
+    irep_pretty_diagnosticst{type});
 
   const bvt &op2_bv=convert_bv(op2);
 
-  if(*size * op2_bv.size() != prev_bv.size())
-  {
-    log.error().source_location = type.source_location();
-    log.error() << "convert_with_array: unexpected operand 2 width"
-                << messaget::eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    *size * op2_bv.size() == prev_bv.size(),
+    "convert_with_array: unexpected operand 2 width",
+    irep_pretty_diagnosticst{type});
 
   // Is the index a constant?
   if(const auto op1_value = numeric_cast<mp_integer>(op1))
@@ -232,22 +201,17 @@ void boolbvt::convert_with_struct(
 
     if(c.get_name() == component_name)
     {
-      if(subtype != op2.type())
-      {
-        log.error().source_location = type.source_location();
-        log.error() << "with/struct: component `" << component_name
-                    << "' type does not match: " << subtype.pretty() << " vs. "
-                    << op2.type().pretty() << messaget::eom;
-        throw 0;
-      }
-
-      if(sub_width!=op2_bv.size())
-      {
-        log.error().source_location = type.source_location();
-        log.error() << "convert_with_struct: unexpected operand op2 width"
-                    << messaget::eom;
-        throw 0;
-      }
+      DATA_INVARIANT_WITH_DIAGNOSTICS(
+        subtype == op2.type(),
+        "with/struct: component `" + id2string(component_name) +
+          "' type does not match",
+        irep_pretty_diagnosticst{subtype},
+        irep_pretty_diagnosticst{op2.type()});
+
+      DATA_INVARIANT_WITH_DIAGNOSTICS(
+        sub_width == op2_bv.size(),
+        "convert_with_struct: unexpected operand op2 width",
+        irep_pretty_diagnosticst{type});
 
       for(std::size_t i=0; i<sub_width; i++)
         next_bv[offset+i]=op2_bv[i];
@@ -269,13 +233,10 @@ void boolbvt::convert_with_union(
 
   const bvt &op2_bv=convert_bv(op2);
 
-  if(next_bv.size()<op2_bv.size())
-  {
-    log.error().source_location = type.source_location();
-    log.error() << "convert_with_union: unexpected operand op2 width"
-                << messaget::eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    next_bv.size() >= op2_bv.size(),
+    "convert_with_union: unexpected operand op2 width",
+    irep_pretty_diagnosticst{type});
 
   if(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
   {