From 341f99349eee592a0614b126fcfe8c4fcf734a4e Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Wed, 29 Aug 2018 14:25:09 +0100 Subject: [PATCH] Invariant cleanup --- src/util/mp_arith.cpp | 25 +++++++++++-------------- src/util/namespace.cpp | 17 +++++++++-------- src/util/namespace.h | 9 +++++++-- src/util/pointer_predicates.cpp | 2 +- src/util/rational.cpp | 6 ++++-- src/util/reference_counting.h | 10 +++++----- 6 files changed, 37 insertions(+), 32 deletions(-) diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp index 798ae25de5c..59199adb7a6 100644 --- a/src/util/mp_arith.cpp +++ b/src/util/mp_arith.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "mp_arith.h" -#include #include #include #include @@ -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()<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()<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); diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp index 76f0a8dbc40..ad1c772feda 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #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; } diff --git a/src/util/namespace.h b/src/util/namespace.h index 94fdbe5df1c..6e7059aa37d 100644 --- a/src/util/namespace.h +++ b/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; } diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 668054bc493..93fb6f45c34 100644 --- a/src/util/pointer_predicates.cpp +++ b/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()) { diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 521e7683c1e..37c204bfdf1 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "invariant.h" + rationalt &rationalt::operator+=(const rationalt &n) { rationalt tmp(n); @@ -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); } diff --git a/src/util/reference_counting.h b/src/util/reference_counting.h index 66aacf734c5..9694fdcbdcb 100644 --- a/src/util/reference_counting.h +++ b/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 +#include "invariant.h" template // 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,7 +96,7 @@ 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 std::cout << "COPY " << (&other) << "\n"; @@ -121,7 +121,7 @@ void reference_counting::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 std::cout << "R: " << old_d << " " << old_d->ref_count << '\n'; @@ -172,7 +172,7 @@ void reference_counting::detach() remove_ref(old_d); } - assert(d->ref_count==1); + POSTCONDITION(d->ref_count == 1); #ifdef REFERENCE_COUNTING_DEBUG std::cout << "DETACH2: " << d << '\n'