Well-formedness check for goto instructions

Check that targets are well-formed and consistent.

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -683,6 +683,15 @@ void goto_programt::instructiont::validate(
   case NO_INSTRUCTION_TYPE:
     break;
   case GOTO:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      has_target(),
+      "goto instruction expects at least one target",
+      source_location);
+    //get_target checks that targets.size()==1
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      get_target()->is_target() && get_target()->target_number != 0,
+      "goto target has to be a target",
+      source_location);
     break;
   case ASSUME:
     DATA_CHECK_WITH_DIAGNOSTICS(

src/util/std_code.h

@@ -1081,8 +1081,9 @@ class code_function_callt:public codet
     return op2().operands();
   }
 
-  static void check(const codet& code,
-                    const validation_modet vm = validation_modet::INVARIANT)
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
       code.operands().size() == 3,
@@ -1180,8 +1181,9 @@ class code_returnt:public codet
     return return_value().is_not_nil();
   }
 
-  static void check(const codet &code,
-                    const validation_modet vm = validation_modet::INVARIANT)
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(code.operands().size() == 1, "return must have one operand");
   }

unit/Makefile

@@ -16,9 +16,10 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        compound_block_locations.cpp \
        goto-programs/goto_trace_output.cpp \
-       goto-programs/goto_program_declaration.cpp \
        goto-programs/goto_program_assume.cpp \
+       goto-programs/goto_program_goto_target.cpp \
        goto-programs/goto_program_function_call.cpp \
+       goto-programs/goto_program_declaration.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/goto-programs/goto_program_goto_target.cpp

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+  Module: Unit tests for goto_program::validate
+
+  Author: Diffblue Ltd.
+
+ \*******************************************************************/
+
+#include <goto-programs/goto_function.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(
+  "Validation of well-formed goto codes",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one assertion")
+  {
+    symbol_tablet symbol_table;
+    const typet type1 = signedbv_typet(32);
+    symbolt symbol;
+    irep_idt symbol_name = "a";
+    symbol.name = symbol_name;
+    symbol_exprt varx(symbol_name, type1);
+    exprt val10 = from_integer(10, type1);
+    binary_relation_exprt x_le_10(varx, ID_le, val10);
+
+    goto_functiont goto_function;
+    auto &instructions = goto_function.body.instructions;
+    instructions.emplace_back(goto_program_instruction_typet::ASSERT);
+    instructions.back().make_assertion(x_le_10);
+
+    instructions.emplace_back(goto_program_instruction_typet::GOTO);
+    instructions.back().make_goto(instructions.begin());
+
+    symbol.type = type1;
+    symbol_table.insert(symbol);
+    namespacet ns(symbol_table);
+
+    WHEN("Target is a target")
+    {
+      instructions.front().target_number = 1;
+      THEN("The consistency check succeeds")
+      {
+        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Target is not a target")
+    {
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_function.body.validate(ns, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}