Well-formedness check for function calls and returns

Check that returned types are matching.

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -713,6 +713,10 @@ void goto_programt::instructiont::validate(
   case ATOMIC_END:
     break;
   case RETURN:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      code.get_statement() == ID_return,
+      "return instruction should contain a return statement",
+      source_location);
     break;
   case ASSIGN:
     DATA_CHECK(
@@ -743,6 +747,10 @@ void goto_programt::instructiont::validate(
       source_location);
     break;
   case FUNCTION_CALL:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      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

@@ -1080,6 +1080,47 @@ class code_function_callt:public codet
   {
     return op2().operands();
   }
+
+  static void check(const codet& code,
+                    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      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(
+        to_code_type(code.op1().type()).return_type().id() == ID_empty,
+        "void function should not return value");
+    else
+      DATA_CHECK(
+        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)
@@ -1102,6 +1143,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
 {
@@ -1133,6 +1179,12 @@ 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(code.operands().size() == 1, "return must have one operand");
+  }
 };
 
 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
@@ -1155,6 +1207,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

@@ -35,6 +35,14 @@ void call_on_code(const codet &code, Args &&... args)
   {
     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

@@ -18,6 +18,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/goto_trace_output.cpp \
        goto-programs/goto_program_declaration.cpp \
        goto-programs/goto_program_assume.cpp \
+       goto-programs/goto_program_function_call.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/goto-programs/goto_program_function_call.cpp

@@ -0,0 +1,84 @@
+/*******************************************************************\
+
+  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 function call codes",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one function call")
+  {
+    symbol_tablet symbol_table;
+    const signedbv_typet type1(32);
+    const signedbv_typet type2(64);
+    const code_typet code_type({}, type1);
+
+    symbolt var_symbol;
+    irep_idt var_symbol_name = "a";
+    var_symbol.name = var_symbol_name;
+    symbol_exprt var_a(var_symbol_name, type1);
+
+    symbolt var_symbol2;
+    irep_idt var_symbol_name2 = "b";
+    var_symbol2.name = var_symbol_name2;
+    symbol_exprt var_b(var_symbol_name2, type2);
+
+    symbolt fun_symbol;
+    irep_idt fun_symbol_name = "foo";
+    fun_symbol.name = fun_symbol_name;
+    symbol_exprt fun_foo(fun_symbol_name, code_type);
+
+    goto_functiont goto_function;
+    auto &instructions = goto_function.body.instructions;
+    instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL);
+
+    var_symbol.type = type1;
+    var_symbol2.type = type2;
+    fun_symbol.type = type1;
+    symbol_table.insert(var_symbol);
+    symbol_table.insert(var_symbol2);
+    symbol_table.insert(fun_symbol);
+    namespacet ns(symbol_table);
+
+    WHEN("Return type matches")
+    {
+      code_function_callt function_call(var_a, fun_foo, {});
+      instructions.back().make_function_call(function_call);
+      REQUIRE(instructions.back().code.get_statement() == ID_function_call);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Return type differs from function type")
+    {
+      code_function_callt function_call(var_b, fun_foo, {});
+      instructions.back().make_function_call(function_call);
+
+      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);
+      }
+    }
+  }
+}