From ccce5d752793fa5ba4ecd7298ab7626b6e752cb0 Mon Sep 17 00:00:00 2001
From: Andreas Paschos <andreas.paschos@diffblue.com>
Date: Tue, 21 Aug 2018 11:08:22 +0100
Subject: [PATCH 1/5] Convert throws and asserts to INVARIANTs for
 goto_convert.cpp

---
 src/goto-programs/goto_convert.cpp | 300 +++++++++++------------------
 1 file changed, 112 insertions(+), 188 deletions(-)

diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index fc45aa43707..dccce82f9e7 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -116,12 +116,10 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
       labelst::const_iterator l_it=
         targets.labels.find(goto_label);
 
-      if(l_it==targets.labels.end())
-      {
-        error().source_location=i.code.find_source_location();
-        error() << "goto label `" << goto_label << "' not found" << eom;
-        throw 0;
-      }
+      DATA_INVARIANT(
+        l_it != targets.labels.end(),
+        i.code.find_source_location().as_string() + ": goto label '" +
+          id2string(goto_label) + "' not found");
 
       i.targets.push_back(l_it->second.first);
     }
@@ -131,12 +129,10 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
 
       labelst::const_iterator l_it=targets.labels.find(goto_label);
 
-      if(l_it==targets.labels.end())
-      {
-        error().source_location=i.code.find_source_location();
-        error() << "goto label `" << goto_label << "' not found" << eom;
-        throw 0;
-      }
+      DATA_INVARIANT(
+        l_it != targets.labels.end(),
+        i.code.find_source_location().as_string() + ": goto label '" +
+          id2string(goto_label) + "' not found");
 
       i.complete_goto(l_it->second.first);
 
@@ -184,9 +180,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
     }
     else
     {
-      error().source_location=i.code.find_source_location();
-      error() << "finish_gotos: unexpected goto" << eom;
-      throw 0;
+      UNREACHABLE;
     }
   }
 
@@ -200,8 +194,9 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
     goto_programt::instructiont &i=*g_it;
     exprt destination=i.code.op0();
 
-    assert(destination.id()==ID_dereference);
-    assert(destination.operands().size()==1);
+    DATA_INVARIANT(
+      destination.id() == ID_dereference, "dereference ID not allowed here");
+    DATA_INVARIANT(destination.operands().size() == 1, "expected 1 argument");
 
     exprt pointer=destination.op0();
 
@@ -310,12 +305,10 @@ void goto_convertt::convert_label(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "label statement expected to have one operand" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().size() == 1,
+    code.find_source_location().as_string() +
+      ": label statement expected to have one operand");
 
   // grab the label
   const irep_idt &label=code.get_label();
@@ -395,25 +388,20 @@ void goto_convertt::convert_gcc_switch_case_range(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=3)
-  {
-    error().source_location=code.find_source_location();
-    error() << "GCC's switch-case-range statement expected to have "
-            << "three operands" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().size() == 3,
+    code.find_source_location().as_string() +
+      ": GCC's switch-case-range statement expected to have three operands");
 
   const auto lb = numeric_cast<mp_integer>(code.op0());
   const auto ub = numeric_cast<mp_integer>(code.op1());
 
-  if(!lb.has_value() || !ub.has_value())
-  {
-    error().source_location = code.find_source_location();
-    error() << "GCC's switch-case-range statement requires constant bounds"
-            << eom;
-    throw 0;
-  }
-  else if(*lb > *ub)
+  DATA_INVARIANT(
+    lb.has_value() && ub.has_value(),
+    code.find_source_location().as_string() +
+      ": GCC's switch-case-range statement requires constant bounds");
+
+  if(*lb > *ub)
   {
     warning().source_location = code.find_source_location();
     warning() << "GCC's switch-case-range statement with empty case range"
@@ -523,24 +511,14 @@ void goto_convertt::convert(
     convert_asm(to_code_asm(code), dest);
   else if(statement==ID_static_assert)
   {
-    assert(code.operands().size()==2);
+    PRECONDITION(code.operands().size() == 2);
     exprt assertion=code.op0();
     assertion.make_typecast(bool_typet());
     simplify(assertion, ns);
-    if(assertion.is_false())
-    {
-      error().source_location=code.op0().find_source_location();
-      error() << "static assertion "
-              << get_string_constant(code.op1()) << eom;
-      throw 0;
-    }
-    else if(assertion.is_true())
-    {
-    }
-    else
-    {
-      // we may wish to complain
-    }
+    INVARIANT(
+      assertion.is_false(),
+      code.op0().find_source_location().as_string() + ": static assertion " +
+        id2string(get_string_constant(code.op1())));
   }
   else if(statement==ID_dead)
     copy(code, DEAD, dest);
@@ -602,12 +580,10 @@ void goto_convertt::convert_expression(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "expression statement takes one operand" << eom;
-    throw 0;
-  }
+  INVARIANT(
+    code.operands().size() == 1,
+    code.find_source_location().as_string() +
+      ": expression statement takes one operand");
 
   exprt expr=code.op0();
 
@@ -648,12 +624,10 @@ void goto_convertt::convert_decl(
 {
   const exprt &op = code.symbol();
 
-  if(op.id() != ID_symbol)
-  {
-    error().source_location = op.find_source_location();
-    error() << "decl statement expects symbol as operand" << eom;
-    throw 0;
-  }
+  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();
 
@@ -729,12 +703,10 @@ void goto_convertt::convert_assign(
   if(rhs.id()==ID_side_effect &&
      rhs.get(ID_statement)==ID_function_call)
   {
-    if(rhs.operands().size()!=2)
-    {
-      error().source_location=rhs.find_source_location();
-      error() << "function_call sideeffect takes two operands" << eom;
-      throw 0;
-    }
+    INVARIANT(
+      rhs.operands().size() == 2,
+      rhs.find_source_location().as_string() +
+        ": function_call sideeffect takes two operands");
 
     Forall_operands(it, rhs)
       clean_expr(*it, dest, mode);
@@ -802,7 +774,7 @@ void goto_convertt::convert_assign(
 
     if(lhs.id()==ID_typecast)
     {
-      assert(lhs.operands().size()==1);
+      INVARIANT(lhs.operands().size() == 1, "typecast takes one operand");
 
       // add a typecast to the rhs
       exprt new_rhs=rhs;
@@ -826,12 +798,10 @@ void goto_convertt::convert_init(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=2)
-  {
-    error().source_location=code.find_source_location();
-    error() <<"init statement takes two operands" << eom;
-    throw 0;
-  }
+  INVARIANT(
+    code.operands().size() == 2,
+    code.find_source_location().as_string() +
+      ": init statement takes two operands");
 
   // make it an assignment
   codet assignment=code;
@@ -844,12 +814,10 @@ void goto_convertt::convert_cpp_delete(
   const codet &code,
   goto_programt &dest)
 {
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "cpp_delete statement takes one operand" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().size() == 1,
+    code.find_source_location().as_string() +
+      ": cpp_delete statement takes one operand");
 
   exprt tmp_op=code.op0();
 
@@ -890,7 +858,9 @@ void goto_convertt::convert_cpp_delete(
   // now do "free"
   exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr();
 
-  assert(to_code_type(delete_symbol.type()).parameters().size()==1);
+  DATA_INVARIANT(
+    to_code_type(delete_symbol.type()).parameters().size() == 1,
+    "delete statement takes 1 parameter");
 
   typet arg_type=
     to_code_type(delete_symbol.type()).parameters().front().type();
@@ -955,14 +925,13 @@ void goto_convertt::convert_loop_invariant(
 
   goto_programt no_sideeffects;
   clean_expr(invariant, no_sideeffects, mode);
-  if(!no_sideeffects.instructions.empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "loop invariant is not side-effect free" << eom;
-    throw 0;
-  }
 
-  assert(loop->is_goto());
+  INVARIANT(
+    no_sideeffects.instructions.empty(),
+    code.find_source_location().as_string() +
+      ": loop invariant is not side-effect free");
+
+  PRECONDITION(loop->is_goto());
   loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
 }
 
@@ -1132,6 +1101,10 @@ void goto_convertt::convert_dowhile(
   goto_programt &dest,
   const irep_idt &mode)
 {
+  INVARIANT(
+    code.operands().size() == 2,
+    code.find_source_location().as_string() + ": dowhile takes two operands");
+
   // save source location
   source_locationt condition_location=code.cond().find_source_location();
 
@@ -1208,7 +1181,7 @@ exprt goto_convertt::case_guard(
     dest.move_to_operands(eq_expr);
   }
 
-  assert(!dest.operands().empty());
+  CHECK_RETURN(!dest.operands().empty());
 
   if(dest.operands().size()==1)
   {
@@ -1331,12 +1304,9 @@ void goto_convertt::convert_break(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(!targets.break_set)
-  {
-    error().source_location=code.find_source_location();
-    error() << "break without target" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    targets.break_set,
+    code.find_source_location().as_string() + ": break without target");
 
   // need to process destructor stack
   unwind_destructor_stack(
@@ -1360,13 +1330,10 @@ void goto_convertt::convert_return(
     throw 0;
   }
 
-  if(!code.operands().empty() &&
-     code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "return takes none or one operand" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().empty() || code.operands().size() == 1,
+    code.find_source_location().as_string() +
+      ": return takes none or one operand");
 
   code_returnt new_code(code);
 
@@ -1386,12 +1353,10 @@ void goto_convertt::convert_return(
 
   if(targets.has_return_value)
   {
-    if(!new_code.has_return_value())
-    {
-      error().source_location=new_code.find_source_location();
-      error() << "function must return value" << eom;
-      throw 0;
-    }
+    INVARIANT(
+      new_code.has_return_value(),
+      new_code.find_source_location().as_string() +
+        ": function must return value");
 
     // Now add a return node to set the return value.
     goto_programt::targett t=dest.add_instruction();
@@ -1401,13 +1366,11 @@ void goto_convertt::convert_return(
   }
   else
   {
-    if(new_code.has_return_value() &&
-       new_code.return_value().type().id()!=ID_empty)
-    {
-      error().source_location=new_code.find_source_location();
-      error() << "function must not return value" << eom;
-      throw 0;
-    }
+    INVARIANT(
+      !new_code.has_return_value() ||
+        new_code.return_value().type().id() == ID_empty,
+      code.find_source_location().as_string() +
+        ": function must not return value");
   }
 
   // Need to process _entire_ destructor stack.
@@ -1424,12 +1387,9 @@ void goto_convertt::convert_continue(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(!targets.continue_set)
-  {
-    error().source_location=code.find_source_location();
-    error() << "continue without target" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    targets.continue_set,
+    code.find_source_location().as_string() + ": continue without target");
 
   // need to process destructor stack
   unwind_destructor_stack(
@@ -1483,12 +1443,10 @@ void goto_convertt::convert_end_thread(
   const codet &code,
   goto_programt &dest)
 {
-  if(!code.operands().empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "end_thread expects no operands" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().empty(),
+    code.find_source_location().as_string() +
+      ": end_thread expects no operands");
 
   copy(code, END_THREAD, dest);
 }
@@ -1497,12 +1455,10 @@ void goto_convertt::convert_atomic_begin(
   const codet &code,
   goto_programt &dest)
 {
-  if(!code.operands().empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "atomic_begin expects no operands" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().empty(),
+    code.find_source_location().as_string() +
+      ": atomic_begin expects no operands");
 
   copy(code, ATOMIC_BEGIN, dest);
 }
@@ -1511,12 +1467,10 @@ void goto_convertt::convert_atomic_end(
   const codet &code,
   goto_programt &dest)
 {
-  if(!code.operands().empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "atomic_end expects no operands" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().empty(),
+    code.find_source_location().as_string() +
+      ": atomic_end expects no operands");
 
   copy(code, ATOMIC_END, dest);
 }
@@ -1526,14 +1480,12 @@ void goto_convertt::convert_ifthenelse(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=3)
-  {
-    error().source_location=code.find_source_location();
-    error() << "ifthenelse takes three operands" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT(
+    code.operands().size() == 3,
+    code.find_source_location().as_string() +
+      ": ifthenelse takes three operands");
 
-  assert(code.then_case().is_not_nil());
+  DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
 
   bool has_else=
     !code.else_case().is_nil();
@@ -1733,7 +1685,7 @@ void goto_convertt::generate_ifthenelse(
 
   // x: goto z;
   x->make_goto(z);
-  assert(!tmp_w.instructions.empty());
+  CHECK_RETURN(!tmp_w.instructions.empty());
   x->source_location=tmp_w.instructions.back().source_location;
 
   dest.destructive_append(tmp_v);
@@ -1811,7 +1763,7 @@ void goto_convertt::generate_conditional_branch(
 {
   if(guard.id()==ID_not)
   {
-    assert(guard.operands().size()==1);
+    PRECONDITION(guard.operands().size() == 1);
     // simply swap targets
     generate_conditional_branch(
       guard.op0(), target_false, target_true, source_location, dest, mode);
@@ -1924,14 +1876,11 @@ irep_idt goto_convertt::get_string_constant(const exprt &expr)
 {
   irep_idt result;
 
-  if(get_string_constant(expr, result))
-  {
-    error().source_location=expr.find_source_location();
-    error() << "expected string constant, but got: "
-      << expr.pretty() << eom;
-
-    throw 0;
-  }
+  bool res = get_string_constant(expr, result);
+  INVARIANT(
+    !res,
+    expr.find_source_location().as_string() + ": expected string constant",
+    expr.pretty());
 
   return result;
 }
@@ -2013,33 +1962,8 @@ void goto_convert(
   message_handlert &message_handler,
   const irep_idt &mode)
 {
-  const std::size_t errors_before=
-    message_handler.get_message_count(messaget::M_ERROR);
-
   goto_convertt goto_convert(symbol_table, message_handler);
-
-  try
-  {
-    goto_convert.goto_convert(code, dest, mode);
-  }
-
-  catch(int)
-  {
-    goto_convert.error();
-  }
-
-  catch(const char *e)
-  {
-    goto_convert.error() << e << messaget::eom;
-  }
-
-  catch(const std::string &e)
-  {
-    goto_convert.error() << e << messaget::eom;
-  }
-
-  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
-    throw 0;
+  goto_convert.goto_convert(code, dest, mode);
 }
 
 void goto_convert(
@@ -2051,8 +1975,8 @@ void goto_convert(
   const symbol_tablet::symbolst::const_iterator s_it=
     symbol_table.symbols.find("main");
 
-  if(s_it==symbol_table.symbols.end())
-    throw "failed to find main symbol";
+  DATA_INVARIANT(
+    s_it != symbol_table.symbols.end(), "failed to find main symbol");
 
   const symbolt &symbol=s_it->second;
 

From 40b2355210b2b7e61f05a5d58a00be770cef0c29 Mon Sep 17 00:00:00 2001
From: Petr Bauch <petr.bauch@DB0276.ox.diffblue.com>
Date: Tue, 25 Sep 2018 16:12:56 +0100
Subject: [PATCH 2/5] 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.
---
 src/cbmc/cbmc_parse_options.cpp    |  7 +++
 src/goto-programs/goto_convert.cpp | 74 +++++++++++++-----------------
 src/util/std_code.h                |  3 ++
 3 files changed, 41 insertions(+), 43 deletions(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 09cc717343d..ead2b6d80cd 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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;
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index dccce82f9e7..9a5e0f90b94 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -11,10 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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());
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 5e282b95c49..2367849b6ca 100644
--- a/src/util/std_code.h
+++ b/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);
 }
 

From e0dca08dddc0a20f63fb979422b15ebbdfd57597 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 27 Sep 2018 16:37:52 +0100
Subject: [PATCH 3/5] Provide tests for goto_convert

---
 regression/ansi-c/goto_convert_break/main.c      |  5 +++++
 regression/ansi-c/goto_convert_break/test.desc   |  8 ++++++++
 regression/ansi-c/goto_convert_continue/main.c   |  5 +++++
 .../ansi-c/goto_convert_continue/test.desc       |  8 ++++++++
 .../goto_convert_invalid_goto_label/main.c       |  8 ++++++++
 .../goto_convert_invalid_goto_label/test.desc    |  8 ++++++++
 .../goto_convert_switch_range_bounds/main.c      | 13 +++++++++++++
 .../goto_convert_switch_range_bounds/test.desc   |  8 ++++++++
 .../goto_convert_switch_range_case_valid/main.c  | 16 ++++++++++++++++
 .../test.desc                                    |  8 ++++++++
 .../goto_convert_switch_range_empty/main.c       | 12 ++++++++++++
 .../goto_convert_switch_range_empty/test.desc    |  8 ++++++++
 .../main.c                                       | 12 ++++++++++++
 .../test.desc                                    |  8 ++++++++
 14 files changed, 127 insertions(+)
 create mode 100644 regression/ansi-c/goto_convert_break/main.c
 create mode 100644 regression/ansi-c/goto_convert_break/test.desc
 create mode 100644 regression/ansi-c/goto_convert_continue/main.c
 create mode 100644 regression/ansi-c/goto_convert_continue/test.desc
 create mode 100644 regression/ansi-c/goto_convert_invalid_goto_label/main.c
 create mode 100644 regression/ansi-c/goto_convert_invalid_goto_label/test.desc
 create mode 100644 regression/ansi-c/goto_convert_switch_range_bounds/main.c
 create mode 100644 regression/ansi-c/goto_convert_switch_range_bounds/test.desc
 create mode 100644 regression/ansi-c/goto_convert_switch_range_case_valid/main.c
 create mode 100644 regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
 create mode 100644 regression/ansi-c/goto_convert_switch_range_empty/main.c
 create mode 100644 regression/ansi-c/goto_convert_switch_range_empty/test.desc
 create mode 100644 regression/ansi-c/goto_convert_switch_range_operands_count/main.c
 create mode 100644 regression/ansi-c/goto_convert_switch_range_operands_count/test.desc

diff --git a/regression/ansi-c/goto_convert_break/main.c b/regression/ansi-c/goto_convert_break/main.c
new file mode 100644
index 00000000000..42c65e6175e
--- /dev/null
+++ b/regression/ansi-c/goto_convert_break/main.c
@@ -0,0 +1,5 @@
+int main()
+{
+  break;
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_break/test.desc b/regression/ansi-c/goto_convert_break/test.desc
new file mode 100644
index 00000000000..20185aa29ee
--- /dev/null
+++ b/regression/ansi-c/goto_convert_break/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/ansi-c/goto_convert_continue/main.c b/regression/ansi-c/goto_convert_continue/main.c
new file mode 100644
index 00000000000..a226cb128b6
--- /dev/null
+++ b/regression/ansi-c/goto_convert_continue/main.c
@@ -0,0 +1,5 @@
+int main()
+{
+  continue;
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_continue/test.desc b/regression/ansi-c/goto_convert_continue/test.desc
new file mode 100644
index 00000000000..988f44bb507
--- /dev/null
+++ b/regression/ansi-c/goto_convert_continue/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring
diff --git a/regression/ansi-c/goto_convert_invalid_goto_label/main.c b/regression/ansi-c/goto_convert_invalid_goto_label/main.c
new file mode 100644
index 00000000000..002a4382e7c
--- /dev/null
+++ b/regression/ansi-c/goto_convert_invalid_goto_label/main.c
@@ -0,0 +1,8 @@
+int main()
+{
+  goto x;
+
+  // x:
+
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_invalid_goto_label/test.desc b/regression/ansi-c/goto_convert_invalid_goto_label/test.desc
new file mode 100644
index 00000000000..92d37c3047e
--- /dev/null
+++ b/regression/ansi-c/goto_convert_invalid_goto_label/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^CONVERSION ERROR$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/ansi-c/goto_convert_switch_range_bounds/main.c b/regression/ansi-c/goto_convert_switch_range_bounds/main.c
new file mode 100644
index 00000000000..2335d8d8210
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_bounds/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int x;
+  int n = 5;
+  switch(x)
+  {
+  case 0 ... n:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_bounds/test.desc b/regression/ansi-c/goto_convert_switch_range_bounds/test.desc
new file mode 100644
index 00000000000..92d37c3047e
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_bounds/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^CONVERSION ERROR$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/ansi-c/goto_convert_switch_range_case_valid/main.c b/regression/ansi-c/goto_convert_switch_range_case_valid/main.c
new file mode 100644
index 00000000000..d46f19d2100
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_case_valid/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+#define false 0
+
+int main(void)
+{
+  int x = 5;
+  switch (x)
+  {
+    case 0 ... 10:
+      break;
+    default:
+      assert(false);
+      break;
+  }
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc b/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
new file mode 100644
index 00000000000..936c704a3e2
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed
diff --git a/regression/ansi-c/goto_convert_switch_range_empty/main.c b/regression/ansi-c/goto_convert_switch_range_empty/main.c
new file mode 100644
index 00000000000..4e6ed4c28cd
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_empty/main.c
@@ -0,0 +1,12 @@
+int main()
+{
+  int x;
+  switch(x)
+  {
+  case 10 ... 0:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_empty/test.desc b/regression/ansi-c/goto_convert_switch_range_empty/test.desc
new file mode 100644
index 00000000000..2718746733c
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_empty/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed
diff --git a/regression/ansi-c/goto_convert_switch_range_operands_count/main.c b/regression/ansi-c/goto_convert_switch_range_operands_count/main.c
new file mode 100644
index 00000000000..7a553052182
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_operands_count/main.c
@@ -0,0 +1,12 @@
+int main()
+{
+  int x;
+  switch(x)
+  {
+  case 0 ... 10 20:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_operands_count/test.desc b/regression/ansi-c/goto_convert_switch_range_operands_count/test.desc
new file mode 100644
index 00000000000..035bb37fe27
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_operands_count/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^PARSING ERROR$
+--
+^warning: ignoring
\ No newline at end of file

From e67b6d0a141e6d633cf9942658706616d3ceb80a Mon Sep 17 00:00:00 2001
From: Petr Bauch <petr.bauch@DB0276.ox.diffblue.com>
Date: Tue, 25 Sep 2018 16:14:17 +0100
Subject: [PATCH 4/5] Refactor goto_convertt::case_guard

Refactor a function in goto_convertt so that it becomes
more comprehensible.
---
 src/goto-programs/goto_convert.cpp | 33 +++++++++++++++---------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 9a5e0f90b94..9c2d5e97066 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -1153,27 +1153,28 @@ exprt goto_convertt::case_guard(
   const exprt &value,
   const exprt::operandst &case_op)
 {
-  exprt dest=exprt(ID_or, bool_typet());
-  dest.reserve_operands(case_op.size());
+  PRECONDITION(!case_op.empty());
 
-  forall_expr(it, case_op)
+  if(case_op.size() == 1)
+    return equal_exprt(value, case_op.at(0));
+  else
   {
-    equal_exprt eq_expr;
-    eq_expr.lhs()=value;
-    eq_expr.rhs()=*it;
-    dest.move_to_operands(eq_expr);
-  }
+    exprt dest = exprt(ID_or, bool_typet());
+    dest.reserve_operands(case_op.size());
 
-  CHECK_RETURN(!dest.operands().empty());
+    forall_expr(it, case_op)
+    {
+      equal_exprt eq_expr;
+      eq_expr.lhs() = value;
+      eq_expr.rhs() = *it;
+      dest.move_to_operands(eq_expr);
+    }
+    INVARIANT(
+      case_op.size() == dest.operands().size(),
+      "case guard conversion should preserve the number of cases");
 
-  if(dest.operands().size()==1)
-  {
-    exprt tmp;
-    tmp.swap(dest.op0());
-    dest.swap(tmp);
+    return dest;
   }
-
-  return dest;
 }
 
 void goto_convertt::convert_switch(

From 552381869c6f82102a7233ce69b951e92d8b8cb6 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 27 Sep 2018 12:17:58 +0100
Subject: [PATCH 5/5] Change data_invariants to invariants_with_diagnostics

Change some data_invariants to invariants_with_diagnostics
where they are more appropriate, and remove some duplicate
invariants, where they are guaranteed by construction of the
types themselves.
---
 src/goto-programs/goto_convert.cpp | 118 +++++++++++++----------------
 1 file changed, 54 insertions(+), 64 deletions(-)

diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 9c2d5e97066..12837784077 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -196,7 +196,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
   {
     goto_programt::instructiont &i=*g_it;
     dereference_exprt destination = to_dereference_expr(i.code.op0());
-    exprt pointer = destination.op();
+    const exprt pointer = destination.pointer();
 
     // remember the expression for later checks
     i.type=OTHER;
@@ -303,11 +303,6 @@ void goto_convertt::convert_label(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
-    code.operands().size() == 1,
-    code.find_source_location().as_string() +
-      ": label statement expected to have one operand");
-
   // grab the label
   const irep_idt &label=code.get_label();
 
@@ -320,8 +315,8 @@ void goto_convertt::convert_label(
   {
     // the body of the thread is expected to be
     // in the operand.
-    INVARIANT(code.op0().is_not_nil(),
-      "op0 in magic thread creation label is null");
+    DATA_INVARIANT(
+      code.op0().is_not_nil(), "op0 in magic thread creation label is null");
 
     // replace the magic thread creation label with a
     // thread block (START_THREAD...END_THREAD).
@@ -386,18 +381,18 @@ void goto_convertt::convert_gcc_switch_case_range(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 3,
-    code.find_source_location().as_string() +
-      ": GCC's switch-case-range statement expected to have three operands");
+    "GCC's switch-case-range statement expected to have three operands",
+    code.find_source_location());
 
   const auto lb = numeric_cast<mp_integer>(code.op0());
   const auto ub = numeric_cast<mp_integer>(code.op1());
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     lb.has_value() && ub.has_value(),
-    code.find_source_location().as_string() +
-      ": GCC's switch-case-range statement requires constant bounds");
+    "GCC's switch-case-range statement requires constant bounds",
+    code.find_source_location());
 
   if(*lb > *ub)
   {
@@ -513,10 +508,10 @@ void goto_convertt::convert(
     exprt assertion=code.op0();
     assertion.make_typecast(bool_typet());
     simplify(assertion, ns);
-    INVARIANT(
+    INVARIANT_WITH_DIAGNOSTICS(
       !assertion.is_false(),
-      code.op0().find_source_location().as_string() + ": static assertion " +
-        id2string(get_string_constant(code.op1())));
+      "static assertion " + id2string(get_string_constant(code.op1())),
+      code.op0().find_source_location());
   }
   else if(statement==ID_dead)
     copy(code, DEAD, dest);
@@ -689,10 +684,10 @@ void goto_convertt::convert_assign(
   if(rhs.id()==ID_side_effect &&
      rhs.get(ID_statement)==ID_function_call)
   {
-    INVARIANT(
+    INVARIANT_WITH_DIAGNOSTICS(
       rhs.operands().size() == 2,
-      rhs.find_source_location().as_string() +
-        ": function_call sideeffect takes two operands");
+      "function_call sideeffect takes two operands",
+      rhs.find_source_location());
 
     Forall_operands(it, rhs)
       clean_expr(*it, dest, mode);
@@ -781,10 +776,10 @@ void goto_convertt::convert_init(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 2,
-    code.find_source_location().as_string() +
-      ": init statement takes two operands");
+    "init statement takes two operands",
+    code.find_source_location());
 
   // make it an assignment
   codet assignment=code;
@@ -797,10 +792,10 @@ void goto_convertt::convert_cpp_delete(
   const codet &code,
   goto_programt &dest)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 1,
-    code.find_source_location().as_string() +
-      ": cpp_delete statement takes one operand");
+    "cpp_delete statement takes one operand",
+    code.find_source_location());
 
   exprt tmp_op=code.op0();
 
@@ -909,10 +904,10 @@ void goto_convertt::convert_loop_invariant(
   goto_programt no_sideeffects;
   clean_expr(invariant, no_sideeffects, mode);
 
-  INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     no_sideeffects.instructions.empty(),
-    code.find_source_location().as_string() +
-      ": loop invariant is not side-effect free");
+    "loop invariant is not side-effect free",
+    code.find_source_location());
 
   PRECONDITION(loop->is_goto());
   loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
@@ -1084,9 +1079,10 @@ void goto_convertt::convert_dowhile(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().size() == 2,
-    code.find_source_location().as_string() + ": dowhile takes two operands");
+    "dowhile takes two operands",
+    code.find_source_location());
 
   // save source location
   source_locationt condition_location=code.cond().find_source_location();
@@ -1253,9 +1249,7 @@ void goto_convertt::convert_switch(
   {
     const caset &case_ops=case_pair.second;
 
-    if(case_ops.empty())
-      throw incorrect_goto_program_exceptiont(
-        "switch case range cannot be empty", code.find_source_location());
+    assert(!case_ops.empty());
 
     exprt guard_expr=case_guard(argument, case_ops);
 
@@ -1290,9 +1284,8 @@ void goto_convertt::convert_break(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
-    targets.break_set,
-    code.find_source_location().as_string() + ": break without target");
+  INVARIANT_WITH_DIAGNOSTICS(
+    targets.break_set, "break without target", code.find_source_location());
 
   // need to process destructor stack
   unwind_destructor_stack(
@@ -1315,10 +1308,10 @@ void goto_convertt::convert_return(
       "return without target", code.find_source_location());
   }
 
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().empty() || code.operands().size() == 1,
-    code.find_source_location().as_string() +
-      ": return takes none or one operand");
+    "return takes none or one operand",
+    code.find_source_location());
 
   code_returnt new_code(code);
 
@@ -1338,10 +1331,10 @@ void goto_convertt::convert_return(
 
   if(targets.has_return_value)
   {
-    INVARIANT(
+    INVARIANT_WITH_DIAGNOSTICS(
       new_code.has_return_value(),
-      new_code.find_source_location().as_string() +
-        ": function must return value");
+      "function must return value",
+      new_code.find_source_location());
 
     // Now add a return node to set the return value.
     goto_programt::targett t=dest.add_instruction();
@@ -1351,11 +1344,11 @@ void goto_convertt::convert_return(
   }
   else
   {
-    INVARIANT(
+    INVARIANT_WITH_DIAGNOSTICS(
       !new_code.has_return_value() ||
         new_code.return_value().type().id() == ID_empty,
-      code.find_source_location().as_string() +
-        ": function must not return value");
+      "function must not return value",
+      code.find_source_location());
   }
 
   // Need to process _entire_ destructor stack.
@@ -1372,9 +1365,10 @@ void goto_convertt::convert_continue(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     targets.continue_set,
-    code.find_source_location().as_string() + ": continue without target");
+    "continue without target",
+    code.find_source_location());
 
   // need to process destructor stack
   unwind_destructor_stack(
@@ -1428,10 +1422,10 @@ void goto_convertt::convert_end_thread(
   const codet &code,
   goto_programt &dest)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().empty(),
-    code.find_source_location().as_string() +
-      ": end_thread expects no operands");
+    "end_thread expects no operands",
+    code.find_source_location());
 
   copy(code, END_THREAD, dest);
 }
@@ -1440,10 +1434,10 @@ void goto_convertt::convert_atomic_begin(
   const codet &code,
   goto_programt &dest)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().empty(),
-    code.find_source_location().as_string() +
-      ": atomic_begin expects no operands");
+    "atomic_begin expects no operands",
+    code.find_source_location());
 
   copy(code, ATOMIC_BEGIN, dest);
 }
@@ -1452,10 +1446,10 @@ void goto_convertt::convert_atomic_end(
   const codet &code,
   goto_programt &dest)
 {
-  DATA_INVARIANT(
+  INVARIANT_WITH_DIAGNOSTICS(
     code.operands().empty(),
-    code.find_source_location().as_string() +
-      ": atomic_end expects no operands");
+    ": atomic_end expects no operands",
+    code.find_source_location());
 
   copy(code, ATOMIC_END, dest);
 }
@@ -1465,11 +1459,6 @@ void goto_convertt::convert_ifthenelse(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  DATA_INVARIANT(
-    code.operands().size() == 3,
-    code.find_source_location().as_string() +
-      ": ifthenelse takes three operands");
-
   DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
 
   bool has_else=
@@ -1865,10 +1854,11 @@ irep_idt goto_convertt::get_string_constant(const exprt &expr)
 {
   irep_idt result;
 
-  bool res = get_string_constant(expr, result);
+  const bool res = get_string_constant(expr, result);
   INVARIANT_WITH_DIAGNOSTICS(
     !res,
-    expr.find_source_location().as_string() + ": expected string constant",
+    "expected string constant",
+    expr.find_source_location(),
     expr.pretty());
 
   return result;