Get function pointer targets in json format.

Add --get-fp-values option to goto-analyzer for all
callsites in json format to be fed to goto-instrument.

Author: NlightNFotis

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -77,13 +77,13 @@ class abstract_environmentt
 
   abstract_object_statisticst gather_statistics(const namespacet &ns) const;
 
-protected:
-  bool bottom;
-
   // We may need to break out more of these cases into these
   virtual abstract_object_pointert eval_expression(
     const exprt &e, const namespacet &ns) const;
 
+protected:
+  bool bottom;
+
   sharing_mapt<map_keyt, abstract_object_pointert> map;
 
 private:

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -114,7 +114,6 @@ class variable_sensitivity_domaint:public ai_domain_baset
   bool is_bottom() const override;
   bool is_top() const override;
 
-protected:
   virtual abstract_object_pointert eval(
     const exprt &expr, const namespacet &ns) const
   {

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/label_function_pointer_call_sites.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_complex.h>
@@ -64,6 +65,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/version.h>
 
 #include "show_on_source.h"
+#include "show_function_pointer_values.h"
 #include "static_show_domain.h"
 #include "static_simplifier.h"
 #include "static_verifier.h"
@@ -331,6 +333,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
       options.set_option("data-dependencies", cmdline.isset("data-dependencies"));
       options.set_option("interval", cmdline.isset("interval-values"));
       options.set_option("value-set", cmdline.isset("value-set"));
+      if(cmdline.isset("get-fp-values")) {
+        options.set_option("function-pointer-values", cmdline.get_value("get-fp-values"));
+      }
     }
     else if(cmdline.isset("dependence-graph-vs"))
     {
@@ -693,6 +698,12 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       show_on_source(goto_model, *analyzer, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
+    else if(options.is_set("function-pointer-values"))
+    {
+      std::string filename = options.get_option("function-pointer-values");
+      print_function_pointer_values(goto_model, *analyzer, options, ui_message_handler, filename);
+      return CPROVER_EXIT_SUCCESS;
+    }
     else if(options.get_bool_option("verify"))
     {
       result = static_verifier(
@@ -760,6 +771,10 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
     #endif
 
+    if(options.is_set("function-pointer-values")) {
+      label_function_pointer_call_sites(goto_model);
+    }
+
     // remove function pointers
     log.status() << "Removing function pointers and virtual functions"
                  << messaget::eom;
@@ -775,14 +790,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_vector(goto_model);
     remove_complex(goto_model);
 
-#if 0
-    // add generic checks
-    log.status() << "Generic Property Instrumentation" << messaget::eom;
-    goto_check(options, goto_model);
-#else
-    (void)options; // unused parameter
-#endif
-
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -152,7 +152,7 @@ class optionst;
   "(non-null)(show-non-null)" \
   "(variable)" \
   "(variable-sensitivity)" \
-  "(pointers)(arrays)(structs)(value-set)(data-dependencies)" \
+  "(pointers)(arrays)(structs)(value-set)(data-dependencies)(get-fp-values):" \
   "(constants)" \
   "(dependence-graph)" \
   "(dependence-graph-vs)" \

src/goto-analyzer/show_function_pointer_values.cpp

@@ -0,0 +1,86 @@
+// Module: Show function pointer values
+// Author: Fotis Koutoulakis, [email protected]
+// Copyright: Diffblue Ltd, 2020
+
+#include "show_function_pointer_values.h"
+
+#include <util/message.h>
+#include <util/namespace.h>
+
+#include <goto-programs/goto_model.h>
+#include <goto-programs/restrict_function_pointers.h>
+
+#include <analyses/ai.h>
+#include <analyses/variable-sensitivity/abstract_enviroment.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_domain.h>
+#include <analyses/variable-sensitivity/value_set_abstract_object.h>
+
+#include <regex>
+#include <string>
+
+void print_function_pointer_values(
+    const goto_modelt &goto_model,
+    const ai_baset &ai,
+    const optionst &options,
+    message_handlert &message_handler,
+    std::string filename)
+{
+    function_pointer_restrictionst::restrictionst map;
+    namespacet ns(goto_model.symbol_table);
+
+    messaget m(message_handler);
+    m.status() << "Getting function pointer targets at specific callsites" << messaget::eom;
+
+    for(auto const &function_entry :  goto_model.goto_functions.function_map)
+    {
+        for_each_goto_location(function_entry.second, [&](ai_baset::locationt instruction_location)
+        {
+            auto is_assign = instruction_location->is_assign();
+            if (is_assign)
+            {
+                auto assign_stmt = instruction_location->get_assign();
+                auto lhs = assign_stmt.lhs();
+                std::string identifier =
+                    id2string(to_symbol_expr(lhs).get_identifier());
+                // <name of function>.function_pointer_call.<integer>
+                std::regex name(R"(\w+\.function_pointer_call\.\d+)");
+                if (std::regex_match(identifier, name)) {
+                    auto const state_after_unique_ptr = ai.abstract_state_after(instruction_location);
+                    PRECONDITION(state_after_unique_ptr != nullptr);
+                    auto state_after = 
+                        dynamic_cast<variable_sensitivity_domaint *>(
+                        state_after_unique_ptr.get());
+                    CHECK_RETURN(state_after != nullptr);
+                    auto const lhs_identifier = to_symbol_expr(lhs).get_identifier();
+                    
+                    if (state_after->is_top())
+                    {
+                        // for top, we don't add restrictions (i.e. normal function pointer removal should take care of this).
+                    }
+                    else if (state_after->is_bottom())
+                    {
+                        // call site is unreachable, so this is empty set
+                        map[lhs_identifier] = {};
+                    }
+                    else
+                    {
+                        auto evaluated_object =
+                            state_after->eval(lhs, ns).get();
+                        auto value_set_object =
+                            (value_set_abstract_objectt *) evaluated_object;
+                        auto values = value_set_object->get_values();                 
+                        auto get_function_pointer_name = [](const exprt &function_pointer) {
+                            return to_symbol_expr(to_address_of_expr(function_pointer).op()).get_identifier();
+                        };
+                
+                        for (const auto &elem : values)
+                        {
+                            map[lhs_identifier].insert(get_function_pointer_name(elem));
+                        }
+                    }
+                }
+            }
+        });
+    }
+    function_pointer_restrictionst{std::move(map)}.write_to_file(filename);
+}

src/goto-analyzer/show_function_pointer_values.h

@@ -0,0 +1,22 @@
+// Module: Show function pointer values
+// Author: Fotis Koutoulakis, [email protected]
+// Copyright: Diffblue Ltd, 2020
+
+#pragma once
+
+#include <string>
+
+class goto_modelt;
+class ai_baset;
+class optionst;
+class message_handlert;
+
+/// Print the values of function pointer call sites as JSON to a file.
+/// Requires label_function_pointer_call_sites and the ai to have already
+/// run on the goto model to work properly.
+void print_function_pointer_values(
+    const goto_modelt &goto_model,
+    const ai_baset &ai,
+    const optionst &options,
+    message_handlert &message_handler,
+    std::string filename);