Translate asserts and throws to PRECONDITIONS and INVARIANTS

Author: NlightNFotis

src/goto-symex/build_goto_trace.cpp

@@ -91,10 +91,10 @@ exprt build_full_lhs_rec(
   else if(id==ID_byte_extract_little_endian ||
           id==ID_byte_extract_big_endian)
   {
-    exprt tmp=src_original;
     DATA_INVARIANT(
-      tmp.operands().size() == 2,
-      "byte_extract_exprt should have two operands.");
+      src_original.operands().size() == 2,
+      "byte extract expressions require two operands");
+    exprt tmp=src_original;
     tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
 
     // re-write into big case-split
@@ -231,7 +231,7 @@ void build_goto_trace(
       else if(it->is_atomic_end() && current_time<0)
         current_time*=-1;
 
-      assert(current_time>=0);
+      INVARIANT(current_time >= 0, "time keeping inconsistency");
       // move any steps gathered in an atomic section
 
       if(time_before<0)

src/goto-symex/goto_symex_state.cpp

@@ -14,10 +14,11 @@ Author: Daniel Kroening, [email protected]
 #include <cstdlib>
 #include <iostream>
 
-#include <util/invariant.h>
 #include <util/base_exceptions.h>
-#include <util/std_expr.h>
+#include <util/exception_utils.h>
+#include <util/invariant.h>
 #include <util/prefix.h>
+#include <util/std_expr.h>
 
 #include <analyses/dirty.h>
 
@@ -51,8 +52,7 @@ void goto_symex_statet::level0t::operator()(
 
   const symbolt *s;
   const bool found_l0 = !ns.lookup(obj_identifier, s);
-  DATA_INVARIANT(
-    found_l0, "level0: failed to find " + id2string(obj_identifier));
+  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id()==ID_code ||
@@ -188,7 +188,7 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   else if(expr.id()==ID_member)
   {
     DATA_INVARIANT(
-      expr.operands().size() == 1, "member_exprt takes one operand.");
+      expr.operands().size() == 1, "member expression expects one operand");
 
     return constant_propagation_reference(expr.op0());
   }
@@ -345,7 +345,8 @@ void goto_symex_statet::assignment(
 
   // see #305 on GitHub for a simple example and possible discussion
   if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
-    throw "pointer handling for concurrency is unsound";
+    throw unsupported_operation_exceptiont(
+      "pointer handling for concurrency is unsound");
 
   // for value propagation -- the RHS is L2
 
@@ -495,12 +496,12 @@ void goto_symex_statet::rename(
   }
   else if(expr.id()==ID_address_of)
   {
+    DATA_INVARIANT(
+      expr.type().id() == ID_pointer,
+      "type of expression required to be pointer");
     DATA_INVARIANT(
       expr.operands().size() == 1, "address_of should have a single operand");
     rename_address(expr.op0(), ns, level);
-    DATA_INVARIANT(
-      expr.type().id() == ID_pointer,
-      "type of address_of should be ID_pointer");
     expr.type().subtype()=expr.op0().type();
   }
   else

src/goto-symex/partial_order_concurrency.cpp

@@ -142,8 +142,8 @@ symbol_exprt partial_order_concurrencyt::clock(
   event_it event,
   axiomt axiom)
 {
-  irep_idt identifier;
   PRECONDITION(!numbering.empty());
+  irep_idt identifier;
 
   if(event->is_shared_write())
     identifier=rw_clock_id(event, axiom);
@@ -198,7 +198,7 @@ exprt partial_order_concurrencyt::before(
         binary_relation_exprt(clock(e1, ax), ID_lt, clock(e2, ax)));
   }
 
-  assert(!ops.empty());
+  POSTCONDITION(!ops.empty());
 
   return conjunction(ops);
 }

src/goto-symex/postcondition.cpp

@@ -77,22 +77,23 @@ bool postconditiont::is_used_address_of(
   else if(expr.id()==ID_index)
   {
     DATA_INVARIANT(
-      expr.operands().size() == 2, "index_exprt takes two operands.");
-
+      expr.operands().size() == 2, "index expression should have two operands");
     return
       is_used_address_of(expr.op0(), identifier) ||
       is_used(expr.op1(), identifier);
   }
   else if(expr.id()==ID_member)
   {
     DATA_INVARIANT(
-      expr.operands().size() == 1, "member_exprt takes one operand.");
+      expr.operands().size() == 1,
+      "member expression should only have one operand");
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_dereference)
   {
     DATA_INVARIANT(
-      expr.operands().size() == 1, "dereference_exprt takes one operand.");
+      expr.operands().size() == 1,
+      "dereference expression should only have one operand");
     return is_used(expr.op0(), identifier);
   }
 
@@ -159,7 +160,8 @@ bool postconditiont::is_used(
   {
     // only do index!
     DATA_INVARIANT(
-      expr.operands().size() == 1, "address_of_exprt takes one operand.");
+      expr.operands().size() == 1,
+      "address_of expression expected to have one operand at this point");
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_symbol &&
@@ -174,7 +176,8 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     DATA_INVARIANT(
-      expr.operands().size() == 1, "dereference_exprt takes one operand.");
+      expr.operands().size() == 1,
+      "dereference expression expected to have one operand");
 
     // aliasing may happen here
 

src/goto-symex/precondition.cpp

@@ -79,20 +79,23 @@ void preconditiont::compute_address_of(exprt &dest)
   else if(dest.id()==ID_index)
   {
     DATA_INVARIANT(
-      dest.operands().size() == 2, "index_exprt takes two operands.");
+      dest.operands().size() == 2,
+      "index expression expected to have two operands");
     compute_address_of(dest.op0());
     compute(dest.op1());
   }
   else if(dest.id()==ID_member)
   {
     DATA_INVARIANT(
-      dest.operands().size() == 1, "member_exprt takes one operand.");
+      dest.operands().size() == 1,
+      "member expression expected to have one operand");
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
     DATA_INVARIANT(
-      dest.operands().size() == 1, "dereference_exprt takes one operand.");
+      dest.operands().size() == 1,
+      "dereference expression expected to have 1 operand");
     compute(dest.op0());
   }
 }
@@ -108,13 +111,15 @@ void preconditiont::compute_rec(exprt &dest)
   {
     // only do index!
     DATA_INVARIANT(
-      dest.operands().size() == 1, "address_of_exprt takes one operand.");
+      dest.operands().size() == 1,
+      "address_of expression expected to have one operand at this point");
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
     DATA_INVARIANT(
-      dest.operands().size() == 1, "dereference_exprt takes one operand.");
+      dest.operands().size() == 1,
+      "dereference expression expected to have one operand at this point");
 
     const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
 

src/goto-symex/show_vcc.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
 
+#include <util/exception_utils.h>
 #include <util/json.h>
 #include <util/json_expr.h>
 #include <util/ui_message.h>
@@ -165,7 +166,8 @@ void show_vcc(
   {
     of.open(filename);
     if(!of)
-      throw "failed to open file " + filename;
+      throw invalid_user_input_exceptiont(
+        "invalid file to read trace from: " + filename, "--outfile");
   }
 
   std::ostream &out = have_file ? of : std::cout;

src/goto-symex/slice_by_trace.cpp

@@ -16,12 +16,13 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 
-#include <util/string2int.h>
-#include <util/simplify_expr.h>
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
-#include <util/guard.h>
+#include <util/exception_utils.h>
 #include <util/format_expr.h>
+#include <util/guard.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/string2int.h>
 
 void symex_slice_by_tracet::slice_by_trace(
   std::string trace_files,
@@ -79,6 +80,11 @@ void symex_slice_by_tracet::slice_by_trace(
   {
     exprt g_copy(*i);
 
+    DATA_INVARIANT(
+      g_copy.id() == ID_symbol || g_copy.id() == ID_not ||
+        g_copy.id() == ID_and || g_copy.id() == ID_constant,
+      "guards should only be and, symbol, constant, or `not'");
+
     if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
     {
       g_copy.make_not();
@@ -92,10 +98,6 @@ void symex_slice_by_tracet::slice_by_trace(
       simplify(copy_last, ns);
       implications.insert(copy_last);
     }
-    else if(!(g_copy.id()==ID_constant))
-    {
-      throw "guards should only be and, symbol, constant, or `not'";
-    }
   }
 
   slice_SSA_steps(equation, implications); // Slice based on implications
@@ -122,7 +124,8 @@ void symex_slice_by_tracet::read_trace(std::string filename)
   std::cout << "Reading trace from file " << filename << '\n';
   std::ifstream file(filename);
   if(file.fail())
-    throw "failed to read from trace file";
+    throw invalid_user_input_exceptiont(
+      "invalid file to read trace from: " + filename, "");
 
   // In case not the first trace read
   alphabet.clear();
@@ -219,9 +222,10 @@ void symex_slice_by_tracet::parse_events(std::string read_line)
     const std::string::size_type vnext=read_line.find(",", vidx);
     std::string event=read_line.substr(vidx, vnext - vidx);
     eis.insert(event);
-    if((!alphabet.empty()) &&
-       ((alphabet.count(event)!=0)!=alphabet_parity))
-      throw "trace uses symbol not in alphabet: "+event;
+    PRECONDITION(!alphabet.empty());
+    INVARIANT(
+      (alphabet.count(event) != 0) == alphabet_parity,
+      "trace uses symbol not in alphabet: " + event);
     if(vnext==std::string::npos)
       break;
     vidx=vnext;