Merge pull request #3 from xbauch/cleanup_goto_convert

Cleanup goto convert

Author: NlightNFotis

regression/ansi-c/goto_convert/convert_break/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  break;
+  return 0;
+}

regression/ansi-c/goto_convert/convert_break/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/goto_convert/convert_continue/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  continue;
+  return 0;
+}

regression/ansi-c/goto_convert/convert_continue/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/goto_convert/invalid_goto_label/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  goto x;
+
+  // x:
+
+  return 0;
+}

regression/ansi-c/goto_convert/invalid_goto_label/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

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;
+}

regression/ansi-c/goto_convert/switch_range_bounds/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

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;
+}

regression/ansi-c/goto_convert/switch_range_empty/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=134$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed

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;
+}

regression/ansi-c/goto_convert/switch_range_operands_count/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+^PARSING ERROR$

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();
@@ -1170,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(
@@ -1269,7 +1253,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 +1311,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 +1748,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 +1866,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);
 }