Invariant 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;
         }
       }
@@ -1373,7 +1373,7 @@ bool simplify_exprt::simplify_update(exprt &expr)
       std::size_t number=to_struct_type(value_ptr_type).
         component_number(component_name);
 
-      assert(number<value_ptr->operands().size());
+      CHECK_RETURN(number < value_ptr->operands().size());
 
       value_ptr=&value_ptr->operands()[number];
     }
@@ -1409,7 +1409,9 @@ bool simplify_exprt::simplify_object(exprt &expr)
   {
     const typet &op_type=ns.follow(expr.op0().type());
 
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      "typecasts must have exactly one argument");
 
     if(op_type.id()==ID_pointer)
     {
@@ -1545,7 +1547,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 +1575,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 +1831,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,7 +213,9 @@ bool simplify_exprt::simplify_not(exprt &expr)
   }
   else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
   {
-    assert(op.operands().size()==2);
+    DATA_INVARIANT(
+      op.operands().size() == 2,
+      "exists expression has two parameters");
     exprt tmp;
     tmp.swap(op);
     expr.swap(tmp);

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();