Merge pull request #6985 from tautschnig/bugfixes/value-set-fi-fp-removal

De-duplicate and fix code of value-set backed function pointer removal

Author: tautschnig

regression/goto-instrument/value-set-fi-fp-removal7/main.c

@@ -0,0 +1,51 @@
+#include <assert.h>
+
+struct PtrWrapperInner
+{
+  int *value;
+};
+
+struct PtrWrapper
+{
+  int *value;
+  struct PtrWrapperInner inner;
+};
+
+struct AltPtrWrapperInner
+{
+  int *value;
+};
+
+struct AltPtrWrapper
+{
+  unsigned int *value;
+  // A) Doesn't work
+  struct AltPtrWrapperInner inner;
+  // B) Works
+  // struct PtrWrapperInner inner;
+};
+
+void fn(struct PtrWrapper wrapper)
+{
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+}
+
+int main()
+{
+  int ret = 10;
+  int *ptr = &ret;
+
+  struct AltPtrWrapper alt;
+  alt.inner.value = ptr;
+  alt.value = ptr;
+
+  // Casting the structure itself works.
+  struct PtrWrapper wrapper = *(struct PtrWrapper *)&alt;
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+
+  // This only works if there is one level of casting.
+  int (*alias)(struct AltPtrWrapper) = (int (*)(struct AltPtrWrapper))fn;
+  alias(alt);
+}

regression/goto-instrument/value-set-fi-fp-removal7/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--value-set-fi-fp-removal
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that the value-set-fi-based function pointer removal performs
+suitable type conversion when argument and parameter types do not match. Source
+file is a copy of cbmc/Function_Pointer19/main.c.

src/goto-instrument/value_set_fi_fp_removal.cpp

@@ -8,176 +8,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_set_fi_fp_removal.h"
 
-#include <goto-programs/goto_model.h>
-
-#include <pointer-analysis/value_set_analysis_fi.h>
-
-#include <util/c_types.h>
-#include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
-#include <util/std_code.h>
-
-#ifdef USE_STD_STRING
-#  include <util/dstring.h>
-#endif
-
-void fix_argument_types(
-  code_function_callt &function_call,
-  const namespacet &ns)
-{
-  const code_typet &code_type =
-    to_code_type(ns.follow(function_call.function().type()));
-
-  const code_typet::parameterst &function_parameters = code_type.parameters();
-
-  code_function_callt::argumentst &call_arguments = function_call.arguments();
-
-  for(std::size_t i = 0; i < function_parameters.size(); i++)
-  {
-    // casting pointers might result in more arguments than function parameters
-    if(i < call_arguments.size())
-    {
-      call_arguments[i] = typecast_exprt::conditional_cast(
-        call_arguments[i], function_parameters[i].type());
-    }
-  }
-}
-
-void fix_return_type(
-  code_function_callt &function_call,
-  goto_programt &dest,
-  goto_modelt &goto_model)
-{
-  // are we returning anything at all?
-  if(function_call.lhs().is_nil())
-    return;
-
-  const namespacet ns(goto_model.symbol_table);
-
-  const code_typet &code_type =
-    to_code_type(ns.follow(function_call.function().type()));
-
-  // type already ok?
-  if(function_call.lhs().type() == code_type.return_type())
-    return;
-
-  const symbolt &function_symbol =
-    ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
-
-  symbolt &tmp_symbol = get_fresh_aux_symbol(
-    code_type.return_type(),
-    id2string(function_call.source_location().get_function()),
-    "tmp_return_val_" + id2string(function_symbol.base_name),
-    function_call.source_location(),
-    function_symbol.mode,
-    goto_model.symbol_table);
-
-  const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
-
-  exprt old_lhs = function_call.lhs();
-  function_call.lhs() = tmp_symbol_expr;
-
-  dest.add(goto_programt::make_assignment(
-    code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
-}
-
-void remove_function_pointer(
-  goto_programt &goto_program,
-  goto_programt::targett target,
-  const std::set<symbol_exprt> &functions,
-  goto_modelt &goto_model)
-{
-  const exprt &function = as_const(*target).call_function();
-  PRECONDITION(function.id() == ID_dereference);
-
-  // this better have the right type
-  code_typet call_type = to_code_type(function.type());
-
-  // refine the type in case the forward declaration was incomplete
-  if(call_type.has_ellipsis() && call_type.parameters().empty())
-  {
-    call_type.remove_ellipsis();
-    for(const auto &argument : as_const(*target).call_arguments())
-      call_type.parameters().push_back(code_typet::parametert(argument.type()));
-  }
-
-  const exprt &pointer = to_dereference_expr(function).pointer();
-
-  // the final target is a skip
-  goto_programt final_skip;
-  goto_programt::targett t_final = final_skip.add(goto_programt::make_skip());
-
-  // build the calls and gotos
-
-  goto_programt new_code_calls;
-  goto_programt new_code_gotos;
-
-  for(const auto &fun : functions)
-  {
-    // call function
-    goto_programt::targett t1 =
-      new_code_calls.add(goto_programt::make_function_call(
-        as_const(*target).call_lhs(),
-        fun,
-        as_const(*target).call_arguments(),
-        target->source_location()));
-
-    // the signature of the function might not match precisely
-    const namespacet ns(goto_model.symbol_table);
-    fix_argument_types(to_code_function_call(t1->code_nonconst()), ns);
-    fix_return_type(
-      to_code_function_call(t1->code_nonconst()), new_code_calls, goto_model);
-
-    // goto final
-    new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
-
-    // goto to call
-    address_of_exprt address_of(fun, pointer_type(fun.type()));
-
-    new_code_gotos.add(goto_programt::make_goto(
-      t1,
-      equal_exprt(
-        pointer,
-        typecast_exprt::conditional_cast(address_of, pointer.type()))));
-  }
-
-  goto_programt::targett t =
-    new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
-  t->source_location_nonconst().set_property_class("pointer dereference");
-  t->source_location_nonconst().set_comment("invalid function pointer");
-
-  goto_programt new_code;
-
-  // patch them all together
-  new_code.destructive_append(new_code_gotos);
-  new_code.destructive_append(new_code_calls);
-  new_code.destructive_append(final_skip);
-
-  // set locations
-  for(auto &instruction : new_code.instructions)
-  {
-    irep_idt property_class =
-      instruction.source_location().get_property_class();
-    irep_idt comment = instruction.source_location().get_comment();
-    instruction.source_location_nonconst() = target->source_location();
-    if(!property_class.empty())
-      instruction.source_location_nonconst().set_property_class(property_class);
-    if(!comment.empty())
-      instruction.source_location_nonconst().set_comment(comment);
-  }
 
-  goto_programt::targett next_target = target;
-  next_target++;
-
-  goto_program.destructive_insert(next_target, new_code);
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_function_pointers.h>
 
-  // We preserve the original dereferencing to possibly catch
-  // further pointer-related errors.
-  *target = goto_programt::make_other(
-    code_expressiont(function), function.source_location());
-}
+#include <pointer-analysis/value_set_analysis_fi.h>
 
 void value_set_fi_fp_removal(
   goto_modelt &goto_model,
@@ -210,7 +48,7 @@ void value_set_fi_fp_removal(
           const auto &pointer = to_dereference_expr(function).pointer();
           auto addresses = value_sets.get_values(f.first, target, pointer);
 
-          std::set<symbol_exprt> functions;
+          std::unordered_set<symbol_exprt, irep_hash> functions;
 
           for(const auto &address : addresses)
           {
@@ -230,8 +68,16 @@ void value_set_fi_fp_removal(
               << "  function: " << f.get_identifier() << messaget::eom;
 
           if(functions.size() > 0)
+          {
             remove_function_pointer(
-              f.second.body, target, functions, goto_model);
+              message_handler,
+              goto_model.symbol_table,
+              f.second.body,
+              f.first,
+              target,
+              functions,
+              true);
+          }
         }
       }
     }