Cleanup asserts & throws - replace with invariants Deprecated c-style asserts in favour of cbmc invariants. Some minor refactoring that was relevant to the cleanup.

Author: Sonny Martin

src/util/simplify_expr_int.cpp

@@ -43,7 +43,10 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
     mp_integer new_value=0;
     for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
     {
-      assert(!bytes.empty());
+      INVARIANT(
+        !bytes.empty(),
+        "bytes is not empty because we just pushed just as many elements on "
+        "top of it as we are popping now");
       new_value+=bytes.back()<<bit;
       bytes.pop_back();
     }
@@ -180,7 +183,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
   exprt::operandst::iterator constant;
 
   // true if we have found a constant
-  bool found = false;
+  bool constant_found = false;
 
   typet c_sizeof_type=nil_typet();
 
@@ -212,7 +215,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
         c_sizeof_type=
           static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
 
-      if(found)
+      if(constant_found)
       {
         // update the constant factor
         if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
@@ -222,7 +225,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
       {
         // set it as the constant factor if this is the first
         constant=it;
-        found=true;
+        constant_found = true;
       }
     }
 
@@ -238,7 +241,10 @@ bool simplify_exprt::simplify_mult(exprt &expr)
 
   if(c_sizeof_type.is_not_nil())
   {
-    assert(found);
+    INVARIANT(
+      constant_found,
+      "c_sizeof_type is only set to a non-nil value "
+      "if a constant has been found");
     constant->set(ID_C_c_sizeof_type, c_sizeof_type);
   }
 
@@ -252,7 +258,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
   else
   {
     // if the constant is a one and there are other factors
-    if(found && constant->is_one())
+    if(constant_found && constant->is_one())
     {
       // just delete it
       operands.erase(constant);
@@ -440,6 +446,8 @@ bool simplify_exprt::simplify_mod(exprt &expr)
 
 bool simplify_exprt::simplify_plus(exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_plus);
+
   if(!is_number(expr.type()) &&
      expr.type().id()!=ID_pointer)
     return true;
@@ -448,8 +456,6 @@ bool simplify_exprt::simplify_plus(exprt &expr)
 
   exprt::operandst &operands=expr.operands();
 
-  assert(expr.id()==ID_plus);
-
   // floating-point addition is _NOT_ associative; thus,
   // there is special case for float
 
@@ -523,7 +529,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
                          to_constant_expr(*it)))
             {
               *it=from_integer(0, it->type());
-              assert(it->is_not_nil());
+              CHECK_RETURN(it->is_not_nil());
               result=false;
             }
           }
@@ -556,7 +562,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
       {
         *(itm->second)=from_integer(0, expr.type());
         *it=from_integer(0, expr.type());
-        assert(it->is_not_nil());
+        CHECK_RETURN(it->is_not_nil());
         expr_map.erase(itm);
         result=false;
       }
@@ -583,7 +589,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
   if(operands.empty())
   {
     expr=from_integer(0, expr.type());
-    assert(expr.is_not_nil());
+    CHECK_RETURN(expr.is_not_nil());
     return false;
   }
   else if(operands.size()==1)
@@ -598,14 +604,14 @@ bool simplify_exprt::simplify_plus(exprt &expr)
 
 bool simplify_exprt::simplify_minus(exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_minus);
+
   if(!is_number(expr.type()) &&
      expr.type().id()!=ID_pointer)
     return true;
 
   exprt::operandst &operands=expr.operands();
 
-  assert(expr.id()==ID_minus);
-
   if(operands.size()!=2)
     return true;
 
@@ -646,7 +652,7 @@ bool simplify_exprt::simplify_minus(exprt &expr)
     if(operands[0]==operands[1])
     {
       exprt zero=from_integer(0, expr.type());
-      assert(zero.is_not_nil());
+      CHECK_RETURN(zero.is_not_nil());
       expr=zero;
       return false;
     }
@@ -741,7 +747,9 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     if(expr.op1().type()!=expr.type())
       break;
 
-    assert(a_str.size()==b_str.size());
+    INVARIANT(
+      a_str.size() == b_str.size(),
+      "bitvectors of the same type have the same size");
 
     constant_exprt new_op(expr.type());
     std::string new_value;
@@ -849,32 +857,40 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
 bool simplify_exprt::simplify_extractbit(exprt &expr)
 {
-  const typet &op0_type=expr.op0().type();
-
-  if(!is_bitvector_type(op0_type))
-    return true;
+  PRECONDITION(expr.id() == ID_extractbit);
+  const auto &extractbit_expr = to_extractbit_expr(expr);
 
-  std::size_t width=to_bitvector_type(op0_type).get_width();
+  const typet &src_type = extractbit_expr.src().type();
 
-  assert(expr.operands().size()==2);
+  if(!is_bitvector_type(src_type))
+    return true;
 
-  mp_integer i;
+  const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
 
-  if(to_integer(expr.op1(), i))
+  const auto index_converted_to_int =
+    numeric_cast<mp_integer>(extractbit_expr.index());
+  if(!index_converted_to_int.has_value())
+  {
     return true;
-
-  if(!expr.op0().is_constant())
+  }
+  const mp_integer index_as_int = index_converted_to_int.value();
+  if(!extractbit_expr.src().is_constant())
     return true;
 
-  if(i<0 || i>=width)
+  if(index_as_int < 0 || index_as_int >= src_bit_width)
     return true;
 
-  const irep_idt &value=expr.op0().get(ID_value);
+  const irep_idt &src_value =
+    to_constant_expr(extractbit_expr.src()).get_value();
+
+  std::string src_value_as_string = id2string(src_value);
 
-  if(value.size()!=width)
+  if(src_value_as_string.size() != src_bit_width)
     return true;
 
-  bool bit=(id2string(value)[width-integer2size_t(i)-1]=='1');
+  const bool bit =
+    (src_value_as_string
+       [src_bit_width - numeric_cast_v<std::size_t>(index_as_int) - 1] == '1');
 
   expr.make_bool(bit);
 
@@ -1582,7 +1598,9 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
 
   // now we only have >=, =
 
-  assert(expr.id()==ID_ge || expr.id()==ID_equal);
+  INVARIANT(
+    expr.id() == ID_ge || expr.id() == ID_equal,
+    "we previously converted all other cases to >= or ==");
 
   // syntactically equal?
 
@@ -1664,7 +1682,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
 bool simplify_exprt::simplify_inequality_constant(exprt &expr)
 {
   // the constant is always on the RHS
-  assert(expr.op1().is_constant());
+  PRECONDITION(expr.op1().is_constant());
 
   if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
   {
@@ -1768,7 +1786,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
           {
             constant+=i;
             *it=from_integer(0, it->type());
-            assert(it->is_not_nil());
+            CHECK_RETURN(it->is_not_nil());
             changed=true;
           }
         }
@@ -1908,9 +1926,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     }
     else if(expr.id()==ID_gt)
     {
-      mp_integer i;
-      if(to_integer(expr.op1(), i))
-        throw "bit-vector constant unexpectedly non-integer";
+      mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
 
       if(i==max)
       {
@@ -1934,9 +1950,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     }
     else if(expr.id()==ID_le)
     {
-      mp_integer i;
-      if(to_integer(expr.op1(), i))
-        throw "bit-vector constant unexpectedly non-integer";
+      mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
 
       if(i==max)
       {

src/util/simplify_expr_pointer.cpp

@@ -196,9 +196,8 @@ bool simplify_exprt::simplify_address_of(exprt &expr)
   else if(object.id()==ID_dereference)
   {
     // simplify &*p to p
-    assert(object.operands().size()==1);
-    exprt tmp=object.op0();
-    expr=tmp;
+    auto const &object_as_dereference_expr = to_dereference_expr(object);
+    expr = object_as_dereference_expr.pointer();
     return false;
   }
 
@@ -410,9 +409,10 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
 bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
-  assert(expr.operands().size()==2);
-  assert(expr.id()==ID_equal || expr.id()==ID_notequal);
+  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
+  PRECONDITION(expr.type().id() == ID_bool);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "(in)equalities have two operands");
 
   exprt tmp0=expr.op0();
   if(tmp0.id()==ID_typecast)
@@ -426,8 +426,8 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
   if(tmp1.op0().id()==ID_index &&
      to_index_expr(tmp1.op0()).index().is_zero())
     tmp1=address_of_exprt(to_index_expr(tmp1.op0()).array());
-  assert(tmp0.id()==ID_address_of);
-  assert(tmp1.id()==ID_address_of);
+  INVARIANT(tmp0.id() == ID_address_of, "id must be ID_address_of");
+  INVARIANT(tmp1.id() == ID_address_of, "id must be ID_address_of");
 
   if(tmp0.operands().size()!=1)
     return true;
@@ -450,14 +450,15 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
 
 bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
-  assert(expr.operands().size()==2);
-  assert(expr.id()==ID_equal || expr.id()==ID_notequal);
+  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
+  PRECONDITION(expr.type().id() == ID_bool);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "(in)equalities have two operands");
 
   forall_operands(it, expr)
   {
-    assert(it->id()==ID_pointer_object);
-    assert(it->operands().size()==1);
+    PRECONDITION(it->id() == ID_pointer_object);
+    PRECONDITION(it->operands().size() == 1);
     const exprt &op=it->op0();
 
     if(op.id()==ID_address_of)

src/util/ssa_expr.h

@@ -153,9 +153,9 @@ class ssa_exprt:public symbol_exprt
 */
 inline const ssa_exprt &to_ssa_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_symbol &&
-         expr.get_bool(ID_C_SSA_symbol) &&
-         !expr.has_operands());
+  PRECONDITION(
+    expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) &&
+    !expr.has_operands());
   return static_cast<const ssa_exprt &>(expr);
 }
 
@@ -164,9 +164,9 @@ inline const ssa_exprt &to_ssa_expr(const exprt &expr)
 */
 inline ssa_exprt &to_ssa_expr(exprt &expr)
 {
-  assert(expr.id()==ID_symbol &&
-         expr.get_bool(ID_C_SSA_symbol) &&
-         !expr.has_operands());
+  PRECONDITION(
+    expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) &&
+    !expr.has_operands());
   return static_cast<ssa_exprt &>(expr);
 }
 

src/util/std_expr.cpp

@@ -74,7 +74,7 @@ static void build_object_descriptor_rec(
     build_object_descriptor_rec(ns, index.array(), dest);
 
     exprt sub_size=size_of_expr(expr.type(), ns);
-    assert(sub_size.is_not_nil());
+    CHECK_RETURN(sub_size.is_not_nil());
 
     dest.offset()=
       plus_exprt(dest.offset(),
@@ -89,7 +89,7 @@ static void build_object_descriptor_rec(
     build_object_descriptor_rec(ns, struct_op, dest);
 
     exprt offset=member_offset_expr(member, ns);
-    assert(offset.is_not_nil());
+    CHECK_RETURN(offset.is_not_nil());
 
     dest.offset()=
       plus_exprt(dest.offset(),
@@ -124,15 +124,15 @@ void object_descriptor_exprt::build(
   const exprt &expr,
   const namespacet &ns)
 {
-  assert(object().id()==ID_unknown);
+  PRECONDITION(object().id() == ID_unknown);
   object()=expr;
 
   if(offset().id()==ID_unknown)
     offset()=from_integer(0, index_type());
 
   build_object_descriptor_rec(ns, expr, *this);
 
-  assert(root_object().type().id()!=ID_empty);
+  POSTCONDITION(root_object().type().id() != ID_empty);
 }
 
 shift_exprt::shift_exprt(
@@ -158,7 +158,7 @@ extractbits_exprt::extractbits_exprt(
   const typet &_type):
   exprt(ID_extractbits, _type)
 {
-  assert(_upper>=_lower);
+  PRECONDITION(_upper >= _lower);
   operands().resize(3);
   src()=_src;
   upper()=from_integer(_upper, integer_typet());
@@ -204,7 +204,8 @@ const exprt &object_descriptor_exprt::root_object() const
 
   while(p->id() == ID_member || p->id() == ID_index)
   {
-    assert(!p->operands().empty());
+    DATA_INVARIANT(
+      p->has_operands(), "member and index expressions have operands");
     p = &p->op0();
   }