Merge pull request #3188 from xbauch/well-formedness-checking-goto

Well formedness checking goto

Author: petr-bauch

src/goto-programs/goto_program.cpp

@@ -676,15 +676,38 @@ void goto_programt::instructiont::validate(
   validate_full_code(code, ns, vm);
   validate_full_expr(guard, ns, vm);
 
+  const symbolt *table_symbol;
+
   switch(type)
   {
   case NO_INSTRUCTION_TYPE:
     break;
   case GOTO:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      has_target(),
+      "goto instruction expects at least one target",
+      source_location);
+    // get_target checks that targets.size()==1
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      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(
+      vm,
+      targets.empty(),
+      "assume instruction should not have a target",
+      source_location);
     break;
   case ASSERT:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      targets.empty(),
+      "assert instruction should not have a target",
+      source_location);
     break;
   case OTHER:
     break;
@@ -703,6 +726,11 @@ void goto_programt::instructiont::validate(
   case ATOMIC_END:
     break;
   case RETURN:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      code.get_statement() == ID_return,
+      "return instruction should contain a return statement",
+      source_location);
     break;
   case ASSIGN:
     DATA_CHECK(
@@ -713,10 +741,37 @@ void goto_programt::instructiont::validate(
       vm, targets.empty(), "assign instruction should not have a target");
     break;
   case DECL:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      code.get_statement() == ID_decl,
+      "declaration instructions should contain a declaration statement",
+      source_location);
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      !ns.lookup(to_code_decl(code).get_identifier(), table_symbol),
+      "declared symbols should be known",
+      id2string(to_code_decl(code).get_identifier()),
+      source_location);
     break;
   case DEAD:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      code.get_statement() == ID_dead,
+      "dead instructions should contain a dead statement",
+      source_location);
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      !ns.lookup(to_code_dead(code).get_identifier(), table_symbol),
+      "removed symbols should be known",
+      id2string(to_code_dead(code).get_identifier()),
+      source_location);
     break;
   case FUNCTION_CALL:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      code.get_statement() == ID_function_call,
+      "function call instruction should contain a call statement",
+      source_location);
     break;
   case THROW:
     break;

src/util/std_code.h

@@ -371,6 +371,19 @@ class code_declt:public codet
   {
     return symbol().get_identifier();
   }
+
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm, code.operands().size() == 1, "declaration must have one operand");
+    DATA_CHECK(
+      vm,
+      code.op0().id() == ID_symbol,
+      "declaring a non-symbol: " +
+        id2string(to_symbol_expr(code.op0()).get_identifier()));
+  }
 };
 
 template<> inline bool can_cast_expr<code_declt>(const exprt &base)
@@ -430,6 +443,21 @@ class code_deadt:public codet
   {
     return symbol().get_identifier();
   }
+
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm,
+      code.operands().size() == 1,
+      "removal (code_deadt) must have one operand");
+    DATA_CHECK(
+      vm,
+      code.op0().id() == ID_symbol,
+      "removing a non-symbol: " +
+        id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope");
+  }
 };
 
 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
@@ -510,6 +538,11 @@ inline code_assumet &to_code_assume(codet &code)
   return static_cast<code_assumet &>(code);
 }
 
+inline void validate_expr(const code_assumet &x)
+{
+  validate_operands(x, 1, "assume must have one operand");
+}
+
 /// A non-fatal assertion, which checks a condition then permits execution to
 /// continue.
 class code_assertt:public codet
@@ -557,6 +590,11 @@ inline code_assertt &to_code_assert(codet &code)
   return static_cast<code_assertt &>(code);
 }
 
+inline void validate_expr(const code_assertt &x)
+{
+  validate_operands(x, 1, "assert must have one operand");
+}
+
 /// Create a fatal assertion, which checks a condition and then halts if it does
 /// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`.
 ///
@@ -1046,6 +1084,51 @@ class code_function_callt:public codet
   {
     return op2().operands();
   }
+
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm,
+      code.operands().size() == 3,
+      "function calls must have three operands:\n1) expression to store the "
+      "returned values\n2) the function being called\n3) the vector of "
+      "arguments");
+  }
+
+  static void validate(
+    const codet &code,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(code, vm);
+
+    if(code.op0().id() == ID_nil)
+      DATA_CHECK(
+        vm,
+        to_code_type(code.op1().type()).return_type().id() == ID_empty,
+        "void function should not return value");
+    else
+      DATA_CHECK(
+        vm,
+        base_type_eq(
+          code.op0().type(), to_code_type(code.op1().type()).return_type(), ns),
+        "function returns expression of wrong type");
+  }
+
+  static void validate_full(
+    const codet &code,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    for(const exprt &op : code.operands())
+    {
+      validate_full_expr(op, ns, vm);
+    }
+
+    validate(code, ns, vm);
+  }
 };
 
 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
@@ -1068,6 +1151,11 @@ inline code_function_callt &to_code_function_call(codet &code)
   return static_cast<code_function_callt &>(code);
 }
 
+inline void validate_expr(const code_function_callt &x)
+{
+  validate_operands(x, 3, "function calls must have three operands");
+}
+
 /// \ref codet representation of a "return from a function" statement.
 class code_returnt:public codet
 {
@@ -1099,6 +1187,13 @@ class code_returnt:public codet
       return false; // backwards compatibility
     return return_value().is_not_nil();
   }
+
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
+  }
 };
 
 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
@@ -1121,6 +1216,11 @@ inline code_returnt &to_code_return(codet &code)
   return static_cast<code_returnt &>(code);
 }
 
+inline void validate_expr(const code_returnt &x)
+{
+  validate_operands(x, 1, "return must have one operand");
+}
+
 /// \ref codet representation of a label for branch targets.
 class code_labelt:public codet
 {

src/util/validate_code.cpp

@@ -31,6 +31,18 @@ void call_on_code(const codet &code, Args &&... args)
   {
     CALL_ON_CODE(code_declt);
   }
+  else if(code.get_statement() == ID_dead)
+  {
+    CALL_ON_CODE(code_deadt);
+  }
+  else if(code.get_statement() == ID_function_call)
+  {
+    CALL_ON_CODE(code_function_callt);
+  }
+  else if(code.get_statement() == ID_return)
+  {
+    CALL_ON_CODE(code_returnt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS

unit/Makefile

@@ -15,6 +15,11 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        compound_block_locations.cpp \
+       goto-programs/goto_program_assume.cpp \
+       goto-programs/goto_program_dead.cpp \
+       goto-programs/goto_program_declaration.cpp \
+       goto-programs/goto_program_function_call.cpp \
+       goto-programs/goto_program_goto_target.cpp \
        goto-programs/goto_trace_output.cpp \
        goto-symex/ssa_equation.cpp \
        interpreter/interpreter.cpp \

unit/goto-programs/goto_program_assume.cpp

@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+  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 assert/assume codes",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one assumption")
+  {
+    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::ASSUME);
+
+    symbol.type = type1;
+    symbol_table.insert(symbol);
+    namespacet ns(symbol_table);
+    instructions.back().make_assertion(x_le_10);
+
+    WHEN("Instruction has no targets")
+    {
+      THEN("The consistency check succeeds")
+      {
+        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Instruction has a target")
+    {
+      instructions.back().targets.push_back(instructions.begin());
+      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);
+      }
+    }
+  }
+}