Invariant cleanup

Author: Sonny Martin

src/util/mp_arith.cpp

@@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "mp_arith.h"
 
-#include <cassert>
 #include <cctype>
 #include <cstdlib>
 #include <limits>
@@ -257,9 +256,9 @@ mp_integer arith_left_shift(
   std::size_t true_size)
 {
   PRECONDITION(a.is_long() && b.is_ulong());
+  PRECONDITION(b <= true_size || a == 0);
+
   ullong_t shift=b.to_ulong();
-  if(shift>true_size && a!=mp_integer(0))
-    throw "shift value out of range";
 
   llong_t result=a.to_long()<<shift;
   llong_t mask=
@@ -280,8 +279,7 @@ mp_integer arith_right_shift(
   PRECONDITION(a.is_long() && b.is_ulong());
   llong_t number=a.to_long();
   ullong_t shift=b.to_ulong();
-  if(shift>true_size)
-    throw "shift value out of range";
+  PRECONDITION(shift <= true_size);
 
   const llong_t sign = (1LL << (true_size - 1)) & number;
   const llong_t pad = (sign == 0) ? 0 : ~((1LL << (true_size - shift)) - 1);
@@ -298,9 +296,9 @@ mp_integer logic_left_shift(
   std::size_t true_size)
 {
   PRECONDITION(a.is_long() && b.is_ulong());
+  PRECONDITION(b <= true_size || a == 0);
+
   ullong_t shift=b.to_ulong();
-  if(shift>true_size && a!=mp_integer(0))
-    throw "shift value out of range";
   llong_t result=a.to_long()<<shift;
   if(true_size<(sizeof(llong_t)*8))
   {
@@ -324,10 +322,9 @@ mp_integer logic_right_shift(
   std::size_t true_size)
 {
   PRECONDITION(a.is_long() && b.is_ulong());
-  ullong_t shift=b.to_ulong();
-  if(shift>true_size)
-    throw "shift value out of range";
+  PRECONDITION(b <= true_size);
 
+  ullong_t shift = b.to_ulong();
   ullong_t result=((ullong_t)a.to_long()) >> shift;
   return result;
 }
@@ -341,10 +338,10 @@ mp_integer rotate_right(
   std::size_t true_size)
 {
   PRECONDITION(a.is_ulong() && b.is_ulong());
+  PRECONDITION(b <= true_size);
+
   ullong_t number=a.to_ulong();
   ullong_t shift=b.to_ulong();
-  if(shift>true_size)
-    throw "shift value out of range";
 
   ullong_t revShift=true_size-shift;
   const ullong_t filter = 1ULL << (true_size - 1);
@@ -361,10 +358,10 @@ mp_integer rotate_left(
   std::size_t true_size)
 {
   PRECONDITION(a.is_ulong() && b.is_ulong());
+  PRECONDITION(b <= true_size);
+
   ullong_t number=a.to_ulong();
   ullong_t shift=b.to_ulong();
-  if(shift>true_size)
-    throw "shift value out of range";
 
   ullong_t revShift=true_size-shift;
   const ullong_t filter = 1ULL << (true_size - 1);

src/util/namespace.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <algorithm>
 
-#include <cassert>
-
 #include "prefix.h"
 #include "std_expr.h"
 #include "std_types.h"
@@ -80,24 +78,27 @@ const typet &namespace_baset::follow(const typet &src) const
 const typet &namespace_baset::follow_tag(const union_tag_typet &src) const
 {
   const symbolt &symbol=lookup(src.get_identifier());
-  assert(symbol.is_type);
-  assert(symbol.type.id()==ID_union || symbol.type.id()==ID_incomplete_union);
+  CHECK_RETURN(symbol.is_type);
+  CHECK_RETURN(
+    symbol.type.id() == ID_union || symbol.type.id() == ID_incomplete_union);
   return symbol.type;
 }
 
 const typet &namespace_baset::follow_tag(const struct_tag_typet &src) const
 {
   const symbolt &symbol=lookup(src.get_identifier());
-  assert(symbol.is_type);
-  assert(symbol.type.id()==ID_struct || symbol.type.id()==ID_incomplete_struct);
+  CHECK_RETURN(symbol.is_type);
+  CHECK_RETURN(
+    symbol.type.id() == ID_struct || symbol.type.id() == ID_incomplete_struct);
   return symbol.type;
 }
 
 const typet &namespace_baset::follow_tag(const c_enum_tag_typet &src) const
 {
   const symbolt &symbol=lookup(src.get_identifier());
-  assert(symbol.is_type);
-  assert(symbol.type.id()==ID_c_enum || symbol.type.id()==ID_incomplete_c_enum);
+  CHECK_RETURN(symbol.is_type);
+  CHECK_RETURN(
+    symbol.type.id() == ID_c_enum || symbol.type.id() == ID_incomplete_c_enum);
   return symbol.type;
 }
 

src/util/namespace.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_NAMESPACE_H
 #define CPROVER_UTIL_NAMESPACE_H
 
+#include "invariant.h"
 #include "irep.h"
 
 class symbol_tablet;
@@ -33,8 +34,12 @@ class namespace_baset
   const symbolt &lookup(const irep_idt &name) const
   {
     const symbolt *symbol;
-    if(lookup(name, symbol))
-      throw "identifier "+id2string(name)+" not found";
+    bool not_found = lookup(name, symbol);
+    INVARIANT(
+      !not_found,
+      "we are assuming that a name exists in the namespace "
+      "when this function is called - identifier " +
+        id2string(name) + " was not found");
     return *symbol;
   }
 

src/util/pointer_predicates.cpp

@@ -226,7 +226,7 @@ exprt object_lower_bound(
   exprt p_offset=pointer_offset(pointer);
 
   exprt zero=from_integer(0, p_offset.type());
-  assert(zero.is_not_nil());
+  CHECK_RETURN(zero.is_not_nil());
 
   if(offset.is_not_nil())
   {

src/util/rational.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "rational.h"
 
+#include "invariant.h"
+
 #include <algorithm>
 #include <ostream>
 
@@ -48,7 +50,7 @@ rationalt &rationalt::operator*=(const rationalt &n)
 
 rationalt &rationalt::operator/=(const rationalt &n)
 {
-  assert(!n.numerator.is_zero());
+  PRECONDITION(!n.numerator.is_zero());
   numerator*=n.denominator;
   denominator*=n.numerator;
   normalize();
@@ -90,7 +92,7 @@ void rationalt::same_denominator(rationalt &n)
 
 void rationalt::invert()
 {
-  assert(numerator!=0);
+  PRECONDITION(numerator != 0);
   std::swap(numerator, denominator);
 }
 

src/util/reference_counting.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_REFERENCE_COUNTING_H
 #define CPROVER_UTIL_REFERENCE_COUNTING_H
 
-#include <cassert>
+#include "invariant.h"
 
 template<typename T>
 // NOLINTNEXTLINE(readability/identifiers)
@@ -33,7 +33,7 @@ class reference_counting
   {
     if(d!=nullptr)
     {
-      assert(d->ref_count!=0);
+      PRECONDITION(d->ref_count != 0);
       d->ref_count++;
       #ifdef REFERENCE_COUNTING_DEBUG
       std::cout << "COPY " << d << " " << d->ref_count << '\n';
@@ -96,9 +96,9 @@ class reference_counting
 
   void copy_from(const reference_counting &other)
   {
-    assert(&other!=this); // check if we assign to ourselves
+    PRECONDITION(&other != this); // check if we assign to ourselves
 
-    #ifdef REFERENCE_COUNTING_DEBUG
+#ifdef REFERENCE_COUNTING_DEBUG
     std::cout << "COPY " << (&other) << "\n";
     #endif
 
@@ -121,9 +121,9 @@ void reference_counting<T>::remove_ref(dt *old_d)
   if(old_d==nullptr)
     return;
 
-  assert(old_d->ref_count!=0);
+  PRECONDITION(old_d->ref_count != 0);
 
-  #ifdef REFERENCE_COUNTING_DEBUG
+#ifdef REFERENCE_COUNTING_DEBUG
   std::cout << "R: " << old_d << " " << old_d->ref_count << '\n';
   #endif
 
@@ -172,9 +172,9 @@ void reference_counting<T>::detach()
     remove_ref(old_d);
   }
 
-  assert(d->ref_count==1);
+  POSTCONDITION(d->ref_count == 1);
 
-  #ifdef REFERENCE_COUNTING_DEBUG
+#ifdef REFERENCE_COUNTING_DEBUG
   std::cout << "DETACH2: " << d << '\n'
   #endif
 }