Merge pull request #7023 from tautschnig/bugfixes/7022-validation

Cleanup GOTO model validation of function calls

Author: kroening

src/goto-programs/validate_goto_model.cpp

@@ -34,9 +34,6 @@ class validate_goto_modelt
   /// until they are linked.
   void entry_point_exists();
 
-  /// Check that no function calls via function pointer are present
-  void function_pointer_calls_removed();
-
   /// Check that for all:
   /// -# functions that are called or
   /// -# functions of which the address is taken
@@ -61,13 +58,7 @@ validate_goto_modelt::validate_goto_modelt(
   if(validation_options.entry_point_exists)
     entry_point_exists();
 
-  if(validation_options.function_pointer_calls_removed)
-  {
-    function_pointer_calls_removed();
-  }
-
-  if(validation_options.check_called_functions)
-    check_called_functions();
+  check_called_functions();
 }
 
 void validate_goto_modelt::entry_point_exists()
@@ -78,23 +69,6 @@ void validate_goto_modelt::entry_point_exists()
     "an entry point must exist");
 }
 
-void validate_goto_modelt::function_pointer_calls_removed()
-{
-  for(const auto &fun : function_map)
-  {
-    for(const auto &instr : fun.second.body.instructions)
-    {
-      if(instr.is_function_call())
-      {
-        DATA_CHECK(
-          vm,
-          instr.call_function().id() == ID_symbol,
-          "no calls via function pointer should be present");
-      }
-    }
-  }
-}
-
 void validate_goto_modelt::check_called_functions()
 {
   auto test_for_function_address =
@@ -123,6 +97,18 @@ void validate_goto_modelt::check_called_functions()
       // check functions that are called
       if(instr.is_function_call())
       {
+        // calls through function pointers are represented by dereference
+        // expressions
+        if(instr.call_function().id() == ID_dereference)
+          continue;
+
+        // the only other permitted expression is a symbol
+        DATA_CHECK(
+          vm,
+          instr.call_function().id() == ID_symbol &&
+            instr.call_function().type().id() == ID_code,
+          "function call expected to be code-typed symbol expression");
+
         const irep_idt &identifier =
           to_symbol_expr(instr.call_function()).get_identifier();
 

src/goto-programs/validate_goto_model.h

@@ -18,18 +18,13 @@ class goto_model_validation_optionst final
   // this check is disabled by default (not all goto programs
   // have an entry point)
   bool entry_point_exists = false;
-
-  bool function_pointer_calls_removed = true;
   bool check_returns_removed = true;
-  bool check_called_functions = true;
 
 private:
   void set_all_flags(bool options_value)
   {
     entry_point_exists = options_value;
-    function_pointer_calls_removed = options_value;
     check_returns_removed = options_value;
-    check_called_functions = options_value;
   }
 
 public:

unit/goto-programs/goto_program_validate.cpp

@@ -132,59 +132,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
     }
   }
 
-  /// check function_pointer_calls_removed()
-  WHEN("not all function calls via fn pointer have been removed")
-  {
-    THEN("fail!")
-    {
-      // introduce function k that has a function pointer call;
-      symbolt k;
-      k.name = "k";
-      k.mode = ID_C;
-      k.type = code_typet({}, empty_typet{}); // void return, take no params
-
-      code_function_callt function_call{
-        dereference_exprt{fn_ptr.symbol_expr(),
-                          pointer_typet(code_typet{{}, empty_typet{}}, 64)}};
-
-      code_blockt k_body{{function_call}};
-      k.value = k_body;
-
-      goto_model.symbol_table.add(k);
-      goto_convert(goto_model, null_message_handler);
-
-      goto_model_validation_optionst validation_options{
-        goto_model_validation_optionst ::set_optionst::all_false};
-
-      validation_options.function_pointer_calls_removed = true;
-
-      REQUIRE_THROWS_AS(
-        validate_goto_model(
-          goto_model.goto_functions,
-          validation_modet::EXCEPTION,
-          validation_options),
-        incorrect_goto_program_exceptiont);
-    }
-  }
-
-  WHEN("all function calls via fn pointer have been removed")
-  {
-    THEN("pass!")
-    {
-      goto_convert(goto_model, null_message_handler);
-
-      goto_model_validation_optionst validation_options{
-        goto_model_validation_optionst ::set_optionst::all_false};
-
-      validation_options.function_pointer_calls_removed = true;
-
-      REQUIRE_NOTHROW(validate_goto_model(
-        goto_model.goto_functions,
-        validation_modet::EXCEPTION,
-        validation_options));
-    }
-  }
-
   WHEN("all returns have been removed")
   {
     THEN("true!")
@@ -218,8 +165,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
       goto_model_validation_optionst validation_options{
         goto_model_validation_optionst ::set_optionst::all_false};
 
-      validation_options.check_called_functions = true;
-
       REQUIRE_THROWS_AS(
         validate_goto_model(
           goto_model.goto_functions,
@@ -242,8 +187,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
       goto_model_validation_optionst validation_options{
         goto_model_validation_optionst ::set_optionst::all_false};
 
-      validation_options.check_called_functions = true;
-
       REQUIRE_THROWS_AS(
         validate_goto_model(
           goto_model.goto_functions,
@@ -264,8 +207,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
       goto_model_validation_optionst validation_options{
         goto_model_validation_optionst ::set_optionst::all_false};
 
-      validation_options.check_called_functions = true;
-
       REQUIRE_NOTHROW(validate_goto_model(
         goto_model.goto_functions,
         validation_modet::EXCEPTION,