Substitute duplicate invariants with transfer function calls

Remove duplicate invariants, and change some to transfer (cast)
function calls, which provide guarantees about the data types
by construction. Also substitute invariants with exceptions
where appropriate.

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/unicode.h>
@@ -611,6 +612,12 @@ int cbmc_parse_optionst::get_goto_program(
     log.status() << config.object_bits_info() << log.eom;
   }
 
+  catch(incorrect_goto_program_exceptiont &e)
+  {
+    log.error() << e.what() << log.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
   catch(const char *e)
   {
     log.error() << e << log.eom;

src/goto-programs/goto_convert.cpp

@@ -11,10 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_convert.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
+#include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/prefix.h>
@@ -116,10 +115,12 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
       labelst::const_iterator l_it=
         targets.labels.find(goto_label);
 
-      DATA_INVARIANT(
-        l_it != targets.labels.end(),
-        i.code.find_source_location().as_string() + ": goto label '" +
-          id2string(goto_label) + "' not found");
+      if(l_it == targets.labels.end())
+      {
+        throw incorrect_goto_program_exceptiont(
+          "goto label \'" + id2string(goto_label) + "\' not found",
+          i.code.find_source_location());
+      }
 
       i.targets.push_back(l_it->second.first);
     }
@@ -129,10 +130,12 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
 
       labelst::const_iterator l_it=targets.labels.find(goto_label);
 
-      DATA_INVARIANT(
-        l_it != targets.labels.end(),
-        i.code.find_source_location().as_string() + ": goto label '" +
-          id2string(goto_label) + "' not found");
+      if(l_it == targets.labels.end())
+      {
+        throw incorrect_goto_program_exceptiont(
+          "goto label \'" + id2string(goto_label) + "\' not found",
+          i.code.find_source_location());
+      }
 
       i.complete_goto(l_it->second.first);
 
@@ -192,13 +195,8 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
   for(auto &g_it : targets.computed_gotos)
   {
     goto_programt::instructiont &i=*g_it;
-    exprt destination=i.code.op0();
-
-    DATA_INVARIANT(
-      destination.id() == ID_dereference, "dereference ID not allowed here");
-    DATA_INVARIANT(destination.operands().size() == 1, "expected 1 argument");
-
-    exprt pointer=destination.op0();
+    dereference_exprt destination = to_dereference_expr(i.code.op0());
+    exprt pointer = destination.op();
 
     // remember the expression for later checks
     i.type=OTHER;
@@ -516,7 +514,7 @@ void goto_convertt::convert(
     assertion.make_typecast(bool_typet());
     simplify(assertion, ns);
     INVARIANT(
-      assertion.is_false(),
+      !assertion.is_false(),
       code.op0().find_source_location().as_string() + ": static assertion " +
         id2string(get_string_constant(code.op1())));
   }
@@ -580,12 +578,7 @@ void goto_convertt::convert_expression(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  INVARIANT(
-    code.operands().size() == 1,
-    code.find_source_location().as_string() +
-      ": expression statement takes one operand");
-
-  exprt expr=code.op0();
+  exprt expr = code.expression();
 
   if(expr.id()==ID_if)
   {
@@ -622,14 +615,7 @@ void goto_convertt::convert_decl(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  const exprt &op = code.symbol();
-
-  INVARIANT(
-    op.id() == ID_symbol,
-    op.find_source_location().as_string() +
-      ": decl statement expects symbol as operand");
-
-  const irep_idt &identifier = to_symbol_expr(op).get_identifier();
+  const irep_idt &identifier = to_symbol_expr(code.symbol()).get_identifier();
 
   const symbolt &symbol = ns.lookup(identifier);
 
@@ -774,11 +760,8 @@ void goto_convertt::convert_assign(
 
     if(lhs.id()==ID_typecast)
     {
-      INVARIANT(lhs.operands().size() == 1, "typecast takes one operand");
-
       // add a typecast to the rhs
-      exprt new_rhs=rhs;
-      rhs.make_typecast(lhs.op0().type());
+      rhs.make_typecast(to_typecast_expr(lhs).op().type());
 
       // remove typecast from lhs
       exprt tmp=lhs.op0();
@@ -1269,7 +1252,9 @@ void goto_convertt::convert_switch(
   {
     const caset &case_ops=case_pair.second;
 
-    assert(!case_ops.empty());
+    if(case_ops.empty())
+      throw incorrect_goto_program_exceptiont(
+        "switch case range cannot be empty", code.find_source_location());
 
     exprt guard_expr=case_guard(argument, case_ops);
 
@@ -1325,9 +1310,8 @@ void goto_convertt::convert_return(
 {
   if(!targets.return_set)
   {
-    error().source_location=code.find_source_location();
-    error() << "return without target" << eom;
-    throw 0;
+    throw incorrect_goto_program_exceptiont(
+      "return without target", code.find_source_location());
   }
 
   DATA_INVARIANT(
@@ -1763,10 +1747,14 @@ void goto_convertt::generate_conditional_branch(
 {
   if(guard.id()==ID_not)
   {
-    PRECONDITION(guard.operands().size() == 1);
     // simply swap targets
     generate_conditional_branch(
-      guard.op0(), target_false, target_true, source_location, dest, mode);
+      to_not_expr(guard).op(),
+      target_false,
+      target_true,
+      source_location,
+      dest,
+      mode);
     return;
   }
 
@@ -1877,7 +1865,7 @@ irep_idt goto_convertt::get_string_constant(const exprt &expr)
   irep_idt result;
 
   bool res = get_string_constant(expr, result);
-  INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     !res,
     expr.find_source_location().as_string() + ": expected string constant",
     expr.pretty());

src/util/std_code.h

@@ -315,6 +315,9 @@ inline const code_declt &to_code_decl(const codet &code)
   // will be size()==1 in the future
   DATA_INVARIANT(
     code.operands().size() >= 1, "decls must have one or more operands");
+  DATA_INVARIANT(
+    code.op0().id() == ID_symbol, "decls symbols must be a \"symbol\"");
+
   return static_cast<const code_declt &>(code);
 }