Well-formedness check for function calls and returns

Check that returned types are matching.

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -748,6 +748,18 @@ void goto_programt::instructiont::validate(
       "asserting non-boolean condition\n" + guard.pretty(),
       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 RETURN:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      code.get_statement() == ID_return,
+      "return instruction should contain a return statement",
+      source_location);
+    break;
   case DEAD:
     DATA_CHECK_WITH_DIAGNOSTICS(
       code.get_statement() == ID_dead,

src/util/std_code.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr.h"
 #include "expr_cast.h"
 #include "invariant.h"
+#include "std_types.h"
 #include "validate.h"
 #include "validate_code.h"
 
@@ -1101,6 +1102,40 @@ class code_function_callt:public codet
   {
     return op2().operands();
   }
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(
+      operands().size() == 3, "function calls must have three operands");
+  }
+
+  void validate(
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    check(vm);
+    if(lhs().id() == ID_nil)
+      DATA_CHECK(
+        to_code_type(function().type()).return_type().id() == ID_empty,
+        "void function should not return value");
+    else
+      DATA_CHECK(
+        base_type_eq(
+          lhs().type(), to_code_type(function().type()).return_type(), ns),
+        "function returns expression of wrong type");
+  }
+
+  void validate_full(
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    for(const exprt &op : operands())
+    {
+      validate_expr_full_pick(op, ns, vm);
+    }
+
+    validate(ns, vm);
+  }
 };
 
 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
@@ -1123,6 +1158,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
 {
@@ -1154,6 +1194,30 @@ class code_returnt:public codet
       return false; // backwards compatibility
     return return_value().is_not_nil();
   }
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(operands().size() == 1, "return must have one operand");
+  }
+
+  void validate(
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    check(vm);
+  }
+
+  void validate_full(
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    for(const exprt &op : operands())
+    {
+      validate_expr_full_pick(op, ns, vm);
+    }
+
+    validate(ns, vm);
+  }
 };
 
 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
@@ -1176,6 +1240,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

@@ -30,6 +30,14 @@ void call_on_code(const codet &code, Args &&... args)
   {
     CALL_ON_CODE(code_declt);
   }
+  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 if(code.get_statement() == ID_decl)
   {
     CALL_ON_CODE(code_declt);

unit/Makefile

@@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
        goto-programs/goto_program_assume.cpp \
+       goto-programs/goto_program_function_call.cpp \
        goto-programs/goto_program_declaration.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.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);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_function.body.validate(symbol_table, 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(
+            symbol_table, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}