From d786c91cfad2191a2ae241e305d2c7676f517035 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Thu, 27 Sep 2018 14:00:16 +0100 Subject: [PATCH] Cleanup asserts & throws - replace with invariants * Deprecated c-style asserts in favour of cbmc invariants. * Some minor refactoring that was relevant to the cleanup. --- src/util/tempdir.cpp | 22 +++++++++++++++------- src/util/tempfile.cpp | 6 ++++-- src/util/type_eq.cpp | 9 +++------ src/util/union_find.cpp | 16 ++++++---------- src/util/union_find.h | 8 ++++++-- src/util/xml.cpp | 3 ++- src/util/xml_expr.cpp | 22 ++++++++++------------ 7 files changed, 46 insertions(+), 40 deletions(-) diff --git a/src/util/tempdir.cpp b/src/util/tempdir.cpp index 8ea7d163d61..7a5b4527fd4 100644 --- a/src/util/tempdir.cpp +++ b/src/util/tempdir.cpp @@ -32,7 +32,7 @@ Author: CM Wintersteiger #include #endif -#include "invariant.h" +#include "exception_utils.h" #include "file_util.h" std::string get_temporary_directory(const std::string &name_template) @@ -45,7 +45,9 @@ std::string get_temporary_directory(const std::string &name_template) DWORD dwRetVal = GetTempPathA(dwBufSize, lpPathBuffer); if(dwRetVal > dwBufSize || (dwRetVal == 0)) - throw "GetTempPath failed"; // NOLINT(readability/throw) + { + throw system_exceptiont("Couldn't get temporary path"); + } // GetTempFileNameA produces \
.TMP
     // where 
 = "TLO"
@@ -54,12 +56,18 @@ std::string get_temporary_directory(const std::string &name_template)
     char t[MAX_PATH];
     UINT uRetVal=GetTempFileNameA(lpPathBuffer, "TLO", 0, t);
     if(uRetVal == 0)
-      throw "GetTempFileName failed"; // NOLINT(readability/throw)
+    {
+      throw system_exceptiont(
+        std::string("Couldn't get new temporary file name in directory") +
+        lpPathBuffer);
+    }
 
     unlink(t);
-    if(_mkdir(t)!=0)
-      throw "_mkdir failed";
-
+    if(_mkdir(t) != 0)
+    {
+      throw system_exceptiont(
+        std::string("Couldn't create temporary directory at ") + t);
+    }
     result=std::string(t);
 
   #else
@@ -75,7 +83,7 @@ std::string get_temporary_directory(const std::string &name_template)
     t.push_back('\0'); // add the zero
     const char *td = mkdtemp(t.data());
     if(!td)
-      throw "mkdtemp failed";
+      throw system_exceptiont("Failed to create temporary directory");
     result=std::string(td);
   #endif
 
diff --git a/src/util/tempfile.cpp b/src/util/tempfile.cpp
index 1c0c4aad385..bfd97941e47 100644
--- a/src/util/tempfile.cpp
+++ b/src/util/tempfile.cpp
@@ -31,6 +31,8 @@ Author: Daniel Kroening
 #include 
 #include 
 
+#include "exception_utils.h"
+
 #if defined(__linux__) || \
     defined(__FreeBSD_kernel__) || \
     defined(__GNU__) || \
@@ -104,7 +106,7 @@ std::string get_temporary_file(
       lpTempPathBuffer); // buffer for path
 
   if(dwRetVal>MAX_PATH || (dwRetVal==0))
-    throw "GetTempPath failed"; // NOLINT(readability/throw)
+    throw system_exceptiont("Failed to get temporary directory");
 
   // the path returned by GetTempPath ends with a backslash
   std::string t_template=
@@ -127,7 +129,7 @@ std::string get_temporary_file(
   int fd=mkstemps(t_ptr, suffix.size());
 
   if(fd<0)
-    throw "mkstemps failed";
+    throw system_exceptiont("Failed to open temporary file");
 
   close(fd);
 
diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp
index 57e838116f0..05a69204f41 100644
--- a/src/util/type_eq.cpp
+++ b/src/util/type_eq.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "type_eq.h"
 
+#include "invariant.h"
 #include "namespace.h"
 #include "std_types.h"
 #include "symbol.h"
@@ -35,18 +36,14 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
   if(const auto symbol_type1 = type_try_dynamic_cast(type1))
   {
     const symbolt &symbol = ns.lookup(*symbol_type1);
-    if(!symbol.is_type)
-      throw "symbol "+id2string(symbol.name)+" is not a type";
-
+    CHECK_RETURN(symbol.is_type);
     return type_eq(symbol.type, type2, ns);
   }
 
   if(const auto symbol_type2 = type_try_dynamic_cast(type2))
   {
     const symbolt &symbol = ns.lookup(*symbol_type2);
-    if(!symbol.is_type)
-      throw "symbol "+id2string(symbol.name)+" is not a type";
-
+    CHECK_RETURN(symbol.is_type);
     return type_eq(type1, symbol.type, ns);
   }
 
diff --git a/src/util/union_find.cpp b/src/util/union_find.cpp
index e30744c7c24..c0d1f4af4d3 100644
--- a/src/util/union_find.cpp
+++ b/src/util/union_find.cpp
@@ -46,16 +46,15 @@ void unsigned_union_find::isolate(size_type a)
   if(is_root(a))
   {
     size_type c=nodes[a].count;
+    DATA_INVARIANT(c != 0, "a root cannot have a node count of zero");
 
     // already isolated?
     if(c==1)
       return;
 
-    assert(c>=2);
-
     // find a new root
     size_type new_root=get_other(a);
-    assert(new_root!=a);
+    CHECK_RETURN(new_root != a);
 
     re_root(a, new_root);
   }
@@ -64,8 +63,6 @@ void unsigned_union_find::isolate(size_type a)
   // get its root
   size_type r=find(a);
 
-  // assert(r!=a);
-
   nodes[r].count--;
   nodes[a].parent=a;
   nodes[a].count=1;
@@ -80,13 +77,11 @@ void unsigned_union_find::re_root(size_type old_root, size_type new_root)
   old_root=find(old_root);
 
   // same set?
-  // assert(find(new_root)==old_root);
   if(find(new_root)!=old_root)
     return;
 
-  // make sure we actually do something
-  assert(new_root!=old_root);
-  assert(nodes[old_root].count>=2);
+  PRECONDITION(!is_root(new_root));
+  PRECONDITION(nodes[old_root].count >= 2);
 
   nodes[new_root].parent=new_root;
   nodes[new_root].count=nodes[old_root].count;
@@ -110,7 +105,8 @@ unsigned_union_find::size_type unsigned_union_find::get_other(size_type a)
   check_index(a);
   a=find(a);
 
-  assert(nodes[a].count>=2);
+  // Cannot find another node in a singleton set
+  PRECONDITION(nodes[a].count >= 2);
 
   // find a different member of the same set
   for(size_type i=0; i
 #include 
 
+#include "invariant.h"
 #include "numbering.h"
 
 // Standard union find with weighting and path compression.
@@ -63,8 +64,11 @@ class unsigned_union_find
 
   void resize(size_type size)
   {
-    // We only enlarge. Shrinking is yet to be implemented.
-    assert(nodes.size()<=size);
+    if(size < nodes.size())
+    {
+      INVARIANT(false, "we don't implement shrinking yet");
+    }
+
     nodes.reserve(size);
     while(nodes.size()
 
+#include "exception_utils.h"
 #include "string2int.h"
 
 void xmlt::clear()
@@ -240,7 +241,7 @@ std::string xmlt::unescape(const std::string &str)
         result+=c;
       }
       else
-        throw "XML escape code not implemented"; // NOLINT(readability/throw)
+        throw deserialization_exceptiont("unknown XML escape code: " + tmp);
     }
     else
       result+=*it;
diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp
index 62af30a1299..89f7e5c28b9 100644
--- a/src/util/xml_expr.cpp
+++ b/src/util/xml_expr.cpp
@@ -13,14 +13,15 @@ Author: Daniel Kroening
 
 #include "xml_expr.h"
 
-#include "namespace.h"
-#include "expr.h"
-#include "xml.h"
 #include "arith_tools.h"
-#include "ieee_float.h"
+#include "config.h"
+#include "expr.h"
 #include "fixedbv.h"
+#include "ieee_float.h"
+#include "invariant.h"
+#include "namespace.h"
 #include "std_expr.h"
-#include "config.h"
+#include "xml.h"
 
 xmlt xml(const source_locationt &location)
 {
@@ -273,7 +274,7 @@ xmlt xml(
     {
       const struct_typet &struct_type=to_struct_type(type);
       const struct_typet::componentst &components=struct_type.components();
-      assert(components.size()==expr.operands().size());
+      PRECONDITION(components.size() == expr.operands().size());
 
       for(unsigned m=0; m