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.cpp

@@ -8,7 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "simplify_expr.h"
 
-#include <cassert>
 #include <algorithm>
 
 #include "arith_tools.h"
@@ -19,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "endianness_map.h"
 #include "expr_util.h"
 #include "fixedbv.h"
+#include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "rational.h"
@@ -225,7 +225,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     inequality.add_source_location()=expr.source_location();
     inequality.lhs()=expr.op0();
     inequality.rhs()=from_integer(0, op_type);
-    assert(inequality.rhs().is_not_nil());
+    CHECK_RETURN(inequality.rhs().is_not_nil());
     simplify_node(inequality);
     expr.swap(inequality);
     return false;
@@ -260,7 +260,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     inequality.add_source_location()=expr.source_location();
     inequality.lhs()=expr.op0();
     inequality.rhs()=from_integer(0, op_type);
-    assert(inequality.rhs().is_not_nil());
+    CHECK_RETURN(inequality.rhs().is_not_nil());
     simplify_node(inequality);
     expr.op0()=inequality;
     simplify_typecast(expr); // recursive call
@@ -488,13 +488,13 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
         if(operand.is_true())
         {
           expr=from_integer(1, expr_type);
-          assert(expr.is_not_nil());
+          CHECK_RETURN(expr.is_not_nil());
           return false;
         }
         else if(operand.is_false())
         {
           expr=from_integer(0, expr_type);
-          assert(expr.is_not_nil());
+          CHECK_RETURN(expr.is_not_nil());
           return false;
         }
       }
@@ -1365,17 +1365,13 @@ bool simplify_exprt::simplify_update(exprt &expr)
     {
       const irep_idt &component_name=
         e.get(ID_component_name);
-
-      if(!to_struct_type(value_ptr_type).
-         has_component(component_name))
+      const struct_typet &value_ptr_struct_type =
+        to_struct_type(value_ptr_type);
+      if(!value_ptr_struct_type.has_component(component_name))
         return true;
-
-      std::size_t number=to_struct_type(value_ptr_type).
-        component_number(component_name);
-
-      assert(number<value_ptr->operands().size());
-
-      value_ptr=&value_ptr->operands()[number];
+      auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
+      value_ptr = &designator_as_struct_expr.component(component_name, ns);
+      CHECK_RETURN(value_ptr->is_not_nil());
     }
     else
       return true; // give up, unknown designator
@@ -1407,16 +1403,13 @@ bool simplify_exprt::simplify_object(exprt &expr)
   }
   else if(expr.id()==ID_typecast)
   {
-    const typet &op_type=ns.follow(expr.op0().type());
-
-    assert(expr.operands().size()==1);
+    auto const &typecast_expr = to_typecast_expr(expr);
+    const typet &op_type = ns.follow(typecast_expr.op().type());
 
     if(op_type.id()==ID_pointer)
     {
       // cast from pointer to pointer
-      exprt tmp;
-      tmp.swap(expr.op0());
-      expr.swap(tmp);
+      expr = typecast_expr.op();
       simplify_object(expr);
       return false;
     }
@@ -1427,10 +1420,12 @@ bool simplify_exprt::simplify_object(exprt &expr)
       // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
       // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.
 
-      exprt tmp=expr.op0();
-      if(tmp.id()==ID_plus && tmp.operands().size()==2)
+      const exprt &casted_expr = typecast_expr.op();
+      if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2)
       {
-        exprt cand=tmp.op0().id()==ID_typecast?tmp.op0():tmp.op1();
+        const exprt &cand = casted_expr.op0().id() == ID_typecast ? casted_expr
+          .op0()
+                                                           : casted_expr.op1();
 
         if(cand.id()==ID_typecast &&
            cand.operands().size()==1 &&
@@ -1545,7 +1540,7 @@ exprt simplify_exprt::bits2expr(
     for(const auto &component : components)
     {
       mp_integer m_size=pointer_offset_bits(component.type(), ns);
-      assert(m_size>=0);
+      CHECK_RETURN(m_size >= 0);
 
       std::string comp_bits=
         std::string(
@@ -1573,7 +1568,7 @@ exprt simplify_exprt::bits2expr(
 
     std::size_t el_size=
       integer2size_t(pointer_offset_bits(type.subtype(), ns));
-    assert(el_size>0);
+    CHECK_RETURN(el_size > 0);
 
     array_exprt result(array_type);
     result.reserve_operands(n_el);
@@ -1829,10 +1824,10 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
         op_type_ptr->id()==ID_array;
         op_type_ptr=&(ns.follow(*op_type_ptr).subtype()))
     {
-      // no arrays of zero-sized objects
-      assert(el_size>0);
-      // no arrays of non-byte sized objects
-      assert(el_size%8==0);
+      DATA_INVARIANT(el_size > 0, "arrays must not have zero-sized objects");
+      DATA_INVARIANT(
+        el_size % 8 == 0,
+        "array elements have a size in bits which is a multiple of bytes");
       mp_integer el_bytes=el_size/8;
 
       if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns) ||

src/util/simplify_expr_boolean.cpp

@@ -8,10 +8,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "simplify_expr_class.h"
 
-#include <cassert>
 #include <unordered_set>
 
 #include "expr.h"
+#include "invariant.h"
 #include "namespace.h"
 #include "std_expr.h"
 
@@ -213,13 +213,10 @@ bool simplify_exprt::simplify_not(exprt &expr)
   }
   else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
   {
-    assert(op.operands().size()==2);
-    exprt tmp;
-    tmp.swap(op);
-    expr.swap(tmp);
-    expr.id(ID_forall);
-    expr.op1().make_not();
-    simplify_node(expr.op1());
+    auto const &op_as_exists = to_exists_expr(op);
+    forall_exprt rewritten_op(op_as_exists.symbol(), not_exprt(op_as_exists.where()));
+    simplify_node(rewritten_op.where());
+    expr = rewritten_op;
     return false;
   }
 

src/util/simplify_expr_floatbv.cpp

@@ -8,13 +8,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "simplify_expr_class.h"
 
-#include <cassert>
-
+#include "arith_tools.h"
 #include "expr.h"
-#include "namespace.h"
 #include "ieee_float.h"
+#include "invariant.h"
+#include "namespace.h"
 #include "std_expr.h"
-#include "arith_tools.h"
 
 bool simplify_exprt::simplify_isinf(exprt &expr)
 {
@@ -142,7 +141,9 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
 {
   // These casts usually reduce precision, and thus, usually round.
 
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.id() == ID_floatbv_typecast);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "float typecast has two operands");
 
   const typet &dest_type=ns.follow(expr.type());
   const typet &src_type=ns.follow(expr.op0().type());
@@ -286,17 +287,25 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
 {
   const typet &type=ns.follow(expr.type());
 
-  if(type.id()!=ID_floatbv)
-    return true;
-
-  assert(expr.operands().size()==3);
+  PRECONDITION(type.id() == ID_floatbv);
+  PRECONDITION(
+    expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
+    expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div);
+  DATA_INVARIANT(
+    expr.operands().size() == 3,
+    "binary operations have two operands, here an addtional parameter "
+    "is for the rounding mode");
 
   exprt op0=expr.op0();
   exprt op1=expr.op1();
   exprt op2=expr.op2(); // rounding mode
 
-  assert(ns.follow(op0.type())==type);
-  assert(ns.follow(op1.type())==type);
+  INVARIANT(
+    ns.follow(op0.type()) == type,
+    "expression type of operand must match type of expression");
+  INVARIANT(
+    ns.follow(op1.type()) == type,
+    "expression type of operand must match type of expression");
 
   // Remember that floating-point addition is _NOT_ associative.
   // Thus, we don't re-sort the operands.
@@ -347,8 +356,8 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
 
 bool simplify_exprt::simplify_ieee_float_relation(exprt &expr)
 {
-  assert(expr.id()==ID_ieee_float_equal ||
-         expr.id()==ID_ieee_float_notequal);
+  PRECONDITION(
+    expr.id() == ID_ieee_float_equal || expr.id() == ID_ieee_float_notequal);
 
   exprt::operandst &operands=expr.operands();
 

src/util/std_expr.h

@@ -4512,6 +4512,24 @@ class exists_exprt:public quantifier_exprt
   }
 };
 
+inline const exists_exprt &to_exists_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_exists);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "exists expressions have exactly two operands");
+  return static_cast<const exists_exprt &>(expr);
+}
+
+inline exists_exprt &to_exists_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_exists);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "exists expressions have exactly two operands");
+  return static_cast<exists_exprt &>(expr);
+}
+
 /// \brief The popcount (counting the number of bits set to 1) expression
 class popcount_exprt: public unary_exprt
 {