Error handling cleanup in solvers/flattening

Files equality.cpp to pointer_logic.h

Author: danpoe

src/solvers/flattening/equality.cpp

@@ -24,10 +24,9 @@ literalt equalityt::equality(const exprt &e1, const exprt &e2)
 
 literalt equalityt::equality2(const exprt &e1, const exprt &e2)
 {
-  const typet &type=e1.type();
+  PRECONDITION(e1.type() == e2.type());
 
-  if(e2.type()!=e1.type())
-    throw "equality got different types";
+  const typet &type = e1.type();
 
   // check for syntactical equality
 
@@ -36,9 +35,8 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2)
 
   // check for boolean equality
 
-  if(type.id()==ID_bool)
-    throw "equalityt got boolean equality";
-  // return lequal(convert(e1), convert(e2));
+  INVARIANT(
+    type.id() != ID_bool, "method shall not be used to compare Boolean types");
 
   // look it up
 

src/solvers/flattening/flatten_byte_operators.cpp

@@ -51,12 +51,15 @@ static exprt unpack_rec(
     mp_integer element_width=pointer_offset_bits(subtype, ns);
     // this probably doesn't really matter
     #if 0
-    if(element_width<=0)
-      throw "cannot unpack array with non-constant element width:\n"+
-        type.pretty();
-    else if(element_width%8!=0)
-      throw "cannot unpack array of non-byte aligned elements:\n"+
-        type.pretty();
+    INVARIANT(
+      element_width > 0,
+      "element width of array should be constant",
+      irep_pretty_diagnosticst(type));
+
+    INVARIANT(
+      element_width % 8 == 0,
+      "elements in array should be byte-aligned",
+      irep_pretty_diagnosticst(type));
     #endif
 
     if(!unpack_byte_array && element_width==8)
@@ -199,8 +202,6 @@ exprt flatten_byte_extract(
   // big-endian: (short)concatenation(01,02)=0x0102
   // little-endian: (short)concatenation(03,04)=0x0304
 
-  assert(src.operands().size()==2);
-
   PRECONDITION(
     src.id() == ID_byte_extract_little_endian ||
     src.id() == ID_byte_extract_big_endian);
@@ -345,14 +346,14 @@ exprt flatten_byte_update(
   const namespacet &ns,
   bool negative_offset)
 {
-  assert(src.operands().size()==3);
+  mp_integer element_size = pointer_offset_size(src.value().type(), ns);
 
-  mp_integer element_size=
-    pointer_offset_size(src.op2().type(), ns);
-  if(element_size<0)
-    throw "byte_update of unknown width:\n"+src.pretty();
+  INVARIANT_WITH_DIAGNOSTICS(
+    element_size >= 0,
+    "size of type in bytes must be known",
+    irep_pretty_diagnosticst(src));
 
-  const typet &t=ns.follow(src.op0().type());
+  const typet &t = ns.follow(src.op().type());
 
   if(t.id()==ID_array)
   {
@@ -368,44 +369,48 @@ exprt flatten_byte_update(
     {
       mp_integer sub_size=pointer_offset_size(subtype, ns);
 
-      if(sub_size==-1)
-        throw "can't flatten byte_update for sub-type without size";
+      INVARIANT(
+        sub_size >= 0,
+        "bit width (rounded to full bytes) of subtype must be known");
 
       // byte array?
       if(sub_size==1)
       {
         // apply 'array-update-with' element_size times
-        exprt result=src.op0();
+        exprt result = src.op();
 
         for(mp_integer i=0; i<element_size; ++i)
         {
-          exprt i_expr=from_integer(i, ns.follow(src.op1().type()));
+          exprt i_expr = from_integer(i, ns.follow(src.offset().type()));
 
           exprt new_value;
 
           if(i==0 && element_size==1) // bytes?
           {
-            new_value=src.op2();
+            new_value = src.value();
             if(new_value.type()!=subtype)
               new_value.make_typecast(subtype);
           }
           else
           {
+            INVARIANT(
+              src.id() == ID_byte_update_little_endian ||
+                src.id() == ID_byte_update_big_endian,
+              "byte update expression should either be little or big endian");
+
             byte_extract_exprt byte_extract_expr(
-              src.id()==ID_byte_update_little_endian?
-                ID_byte_extract_little_endian:
-                src.id()==ID_byte_update_big_endian?
-                  ID_byte_extract_big_endian:
-                    throw "unexpected src.id() in flatten_byte_update",
+              src.id() == ID_byte_update_little_endian
+                ? ID_byte_extract_little_endian
+                : ID_byte_extract_big_endian,
               subtype);
 
-            byte_extract_expr.op()=src.op2();
+            byte_extract_expr.op() = src.value();
             byte_extract_expr.offset()=i_expr;
 
             new_value=flatten_byte_extract(byte_extract_expr, ns);
           }
 
-          const plus_exprt where(src.op1(), i_expr);
+          const plus_exprt where(src.offset(), i_expr);
 
           with_exprt with_expr(result, where, new_value);
           with_expr.type()=src.type();
@@ -417,34 +422,34 @@ exprt flatten_byte_update(
       }
       else // sub_size!=1
       {
-        exprt result=src.op0();
+        exprt result = src.op();
 
         // Number of potentially affected array cells:
         mp_integer num_elements=
           element_size/sub_size+((element_size%sub_size==0)?1:2);
 
-        const auto &offset_type=ns.follow(src.op1().type());
+        const auto &offset_type = ns.follow(src.offset().type());
         exprt zero_offset=from_integer(0, offset_type);
 
         exprt sub_size_expr=from_integer(sub_size, offset_type);
         exprt element_size_expr=from_integer(element_size, offset_type);
 
         // First potentially affected cell:
-        div_exprt first_cell(src.op1(), sub_size_expr);
+        div_exprt first_cell(src.offset(), sub_size_expr);
 
         for(mp_integer i=0; i<num_elements; ++i)
         {
           plus_exprt cell_index(first_cell, from_integer(i, offset_type));
           mult_exprt cell_offset(cell_index, sub_size_expr);
-          index_exprt old_cell_value(src.op0(), cell_index, subtype);
+          index_exprt old_cell_value(src.op(), cell_index, subtype);
           bool is_first_cell=i==0;
           bool is_last_cell=i==num_elements-1;
 
           exprt new_value;
           exprt stored_value_offset;
           if(element_size<=sub_size)
           {
-            new_value=src.op2();
+            new_value = src.value();
             stored_value_offset=zero_offset;
           }
           else
@@ -458,19 +463,20 @@ exprt flatten_byte_update(
               stored_value_offset=
                 from_integer(element_size-sub_size, offset_type);
             else
-              stored_value_offset=minus_exprt(cell_offset, src.op1());
-
-            auto extract_opcode=
-              src.id()==ID_byte_update_little_endian ?
-              ID_byte_extract_little_endian :
-              src.id()==ID_byte_update_big_endian ?
-              ID_byte_extract_big_endian :
-              throw "unexpected src.id() in flatten_byte_update";
+              stored_value_offset = minus_exprt(cell_offset, src.offset());
+
+            INVARIANT(
+              src.id() == ID_byte_update_little_endian ||
+                src.id() == ID_byte_update_big_endian,
+              "byte update expression should either be little or big endian");
+
             byte_extract_exprt byte_extract_expr(
-              extract_opcode,
-              element_size<sub_size ? src.op2().type() : subtype);
+              src.id() == ID_byte_update_little_endian
+                ? ID_byte_extract_little_endian
+                : ID_byte_extract_big_endian,
+              element_size < sub_size ? src.value().type() : subtype);
 
-            byte_extract_expr.op()=src.op2();
+            byte_extract_expr.op() = src.value();
             byte_extract_expr.offset()=stored_value_offset;
 
             new_value=flatten_byte_extract(byte_extract_expr, ns);
@@ -482,15 +488,13 @@ exprt flatten_byte_update(
           // target array cell.
           exprt overwrite_offset;
           if(is_first_cell)
-            overwrite_offset=mod_exprt(src.op1(), sub_size_expr);
+            overwrite_offset = mod_exprt(src.offset(), sub_size_expr);
           else if(is_last_cell)
           {
             // This is intentionally negated; passing is_last_cell
             // to flatten below leads to it being negated again later.
-            overwrite_offset=
-              minus_exprt(
-                minus_exprt(cell_offset, src.op1()),
-                stored_value_offset);
+            overwrite_offset = minus_exprt(
+              minus_exprt(cell_offset, src.offset()), stored_value_offset);
           }
           else
             overwrite_offset=zero_offset;
@@ -517,9 +521,10 @@ exprt flatten_byte_update(
     }
     else
     {
-      throw
-        "flatten_byte_update can only do arrays of scalars right now, "
-        "but got "+subtype.id_string();
+      PRECONDITION_WITH_DIAGNOSTICS(
+        false,
+        "flatten_byte_update can only do arrays of scalars right now",
+        subtype.id_string());
     }
   }
   else if(t.id()==ID_signedbv ||
@@ -530,11 +535,12 @@ exprt flatten_byte_update(
   {
     // do a shift, mask and OR
     mp_integer type_width=pointer_offset_bits(t, ns);
-    assert(type_width>0);
+    CHECK_RETURN(type_width > 0);
     std::size_t width=integer2size_t(type_width);
 
-    if(element_size*8>width)
-      throw "flatten_byte_update to update element that is too large";
+    INVARIANT(
+      element_size * 8 <= width,
+      "element bit width must not be larger than width indicated by type");
 
     // build mask
     exprt mask=
@@ -544,16 +550,16 @@ exprt flatten_byte_update(
     exprt value_extended;
 
     if(width>integer2unsigned(element_size)*8)
-      value_extended=
-        concatenation_exprt(
-          from_integer(
-            0, unsignedbv_typet(width-integer2unsigned(element_size)*8)),
-          src.op2(), t);
+      value_extended = concatenation_exprt(
+        from_integer(
+          0, unsignedbv_typet(width - integer2unsigned(element_size) * 8)),
+        src.value(),
+        t);
     else
-      value_extended=src.op2();
+      value_extended = src.value();
 
-    const typet &offset_type=ns.follow(src.op1().type());
-    mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type));
+    const typet &offset_type = ns.follow(src.offset().type());
+    mult_exprt offset_times_eight(src.offset(), from_integer(8, offset_type));
 
     binary_predicate_exprt offset_ge_zero(
       offset_times_eight,
@@ -578,7 +584,7 @@ exprt flatten_byte_update(
     }
 
     // original_bits &= ~mask
-    bitand_exprt bitand_expr(src.op0(), bitnot_exprt(mask_shifted));
+    bitand_exprt bitand_expr(src.op(), bitnot_exprt(mask_shifted));
 
     // original_bits |= newvalue
     bitor_exprt bitor_expr(bitand_expr, value_shifted);
@@ -587,8 +593,10 @@ exprt flatten_byte_update(
   }
   else
   {
-    throw "flatten_byte_update can only do array and scalars "
-          "right now, but got "+t.id_string();
+    PRECONDITION_WITH_DIAGNOSTICS(
+      false,
+      "flatten_byte_update can only do arrays and scalars right now",
+      t.id_string());
   }
 }
 

src/solvers/flattening/functions.cpp

@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "functions.h"
 
-#include <cassert>
-
 #include <util/std_types.h>
 #include <util/std_expr.h>
 
@@ -32,7 +30,7 @@ void functionst::add_function_constraints()
 exprt functionst::arguments_equal(const exprt::operandst &o1,
                                   const exprt::operandst &o2)
 {
-  assert(o1.size()==o2.size());
+  PRECONDITION(o1.size() == o2.size());
 
   if(o1.empty())
     return true_exprt();

src/solvers/flattening/pointer_logic.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "pointer_logic.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/invariant.h>
@@ -52,13 +50,11 @@ std::size_t pointer_logict::add_object(const exprt &expr)
 
   if(expr.id()==ID_index)
   {
-    assert(expr.operands().size()==2);
-    return add_object(expr.op0());
+    return add_object(to_index_expr(expr).array());
   }
   else if(expr.id()==ID_member)
   {
-    assert(expr.operands().size()==1);
-    return add_object(expr.op0());
+    return add_object(to_member_expr(expr).compound());
   }
 
   return objects.number(expr);
@@ -149,12 +145,15 @@ exprt pointer_logict::object_rec(
 
     for(const auto &c : components)
     {
-      assert(offset>=current_offset);
+      INVARIANT(
+        offset >= current_offset,
+        "when the object has not been found yet its offset must not be smaller"
+        "than the offset of the current struct component");
 
       const typet &subtype=c.type();
 
       mp_integer sub_size=pointer_offset_size(subtype, ns);
-      assert(sub_size>0);
+      CHECK_RETURN(sub_size > 0);
       mp_integer new_offset=current_offset+sub_size;
 
       if(new_offset>offset)
@@ -166,9 +165,7 @@ exprt pointer_logict::object_rec(
           offset-current_offset, pointer_type, tmp);
       }
 
-      assert(new_offset<=offset);
       current_offset=new_offset;
-      assert(current_offset<=offset);
     }
 
     return src;
@@ -183,7 +180,7 @@ pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns)
 {
   // add NULL
   null_object=objects.number(exprt(ID_NULL));
-  assert(null_object==0);
+  CHECK_RETURN(null_object == 0);
 
   // add INVALID
   invalid_object=objects.number(exprt("INVALID"));