Merge pull request #1010 from danpoe/no-body-inlining

Do not remove calls to functions without a body during inlining

Author: danpoe

regression/goto-instrument/inline_09/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---inline
+--inline --remove-calls-no-body
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
@@ -9,4 +9,5 @@ main.c
 ^\s*a;$
 no body.*[`]f
 --
+f\(\)
 ^warning: ignoring

regression/goto-instrument/inline_16/main.c

@@ -0,0 +1,9 @@
+void func1();
+
+int main()
+{
+  int ret;
+
+  func1();
+  ret = func2();
+}

regression/goto-instrument/inline_16/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+func1\(\)
+ret.*=.*func2\(\)
+no body for function.*func1
+no body for function.*func2
+--
+^warning: ignoring

regression/goto-instrument/inline_17/main.c

@@ -0,0 +1,9 @@
+void func1()
+{
+  func2();
+}
+
+int main()
+{
+  func1();
+}

regression/goto-instrument/inline_17/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function-inline func1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+func1\(\)
+func2\(\)
+--
+^warning: ignoring

regression/goto-instrument/remove-calls-no-body1/main.c

@@ -0,0 +1,19 @@
+void func1();
+
+void func3()
+{
+}
+
+void func4()
+{
+  func1();
+  func2();
+}
+
+void main()
+{
+  func1();
+  func2();
+  func3();
+  func4();
+}

regression/goto-instrument/remove-calls-no-body1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--remove-calls-no-body
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+func3\(\)
+func4\(\)
+--
+func1\(\)
+func2\(\)
+^warning: ignoring

regression/goto-instrument/remove-calls-no-body2/main.c

@@ -0,0 +1,21 @@
+int func1(int arg1, int arg2);
+
+void func3()
+{
+}
+
+void func4()
+{
+  func1(567, 285);
+  func2();
+}
+
+void main()
+{
+  int ret1;
+
+  ret1 = func1(567, 285);
+  func2();
+  func3();
+  func4();
+}

regression/goto-instrument/remove-calls-no-body2/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--remove-calls-no-body
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+func3\(\)
+func4\(\)
+567;
+285;
+ret1.*=.*NONDET
+--
+func1\(.*\)
+func2\(.*\)
+^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_exceptions.h>
@@ -729,6 +730,10 @@ int goto_instrument_parse_optionst::doit()
       status() << "Performing full inlining" << eom;
       goto_inline(goto_model, get_message_handler());
 
+      status() << "Removing calls to functions without a body" << eom;
+      remove_calls_no_bodyt remove_calls_no_body;
+      remove_calls_no_body(goto_model.goto_functions);
+
       status() << "Accelerating" << eom;
       accelerate_functions(
         goto_model, get_message_handler(), cmdline.isset("z3"));
@@ -992,7 +997,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   // now do full inlining, if requested
   if(cmdline.isset("inline"))
   {
-    do_indirect_call_and_rtti_removal();
+    do_indirect_call_and_rtti_removal(true);
 
     if(cmdline.isset("show-custom-bitvector-analysis") ||
        cmdline.isset("custom-bitvector-analysis"))
@@ -1003,7 +1008,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     }
 
     status() << "Performing full inlining" << eom;
-    goto_inline(goto_model, get_message_handler());
+    goto_inline(goto_model, get_message_handler(), true);
   }
 
   if(cmdline.isset("show-custom-bitvector-analysis") ||
@@ -1111,27 +1116,23 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("partial-inline"))
   {
     do_indirect_call_and_rtti_removal();
-    do_partial_inlining();
+
+    status() << "Partial inlining" << eom;
+    goto_partial_inline(goto_model, ui_message_handler, 0, true);
 
     goto_model.goto_functions.update();
     goto_model.goto_functions.compute_loop_numbers();
   }
 
-  // now do full inlining, if requested
-  if(cmdline.isset("inline"))
+  if(cmdline.isset("remove-calls-no-body"))
   {
-    do_indirect_call_and_rtti_removal(/*force=*/true);
+    status() << "Removing calls to functions without a body" << eom;
 
-    if(cmdline.isset("show-custom-bitvector-analysis") ||
-       cmdline.isset("custom-bitvector-analysis"))
-    {
-      do_remove_returns();
-      thread_exit_instrumentation(goto_model);
-      mutex_init_instrumentation(goto_model);
-    }
+    remove_calls_no_bodyt remove_calls_no_body;
+    remove_calls_no_body(goto_model.goto_functions);
 
-    status() << "Performing full inlining" << eom;
-    goto_inline(goto_model, get_message_handler(), true);
+    goto_model.goto_functions.update();
+    goto_model.goto_functions.compute_loop_numbers();
   }
 
   if(cmdline.isset("constant-propagator"))
@@ -1560,6 +1561,7 @@ void goto_instrument_parse_optionst::help()
     " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
     " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
     " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
+    HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS
     " --add-library                add models of C library functions\n"
     " --model-argc-argv <n>        model up to <n> command line arguments\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
+#include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_const_function_pointers.h>
 
 #include <analyses/goto_check.h>
@@ -84,7 +85,8 @@ Author: Daniel Kroening, [email protected]
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
-  "(splice-call):"
+  "(splice-call):" \
+  OPT_REMOVE_CALLS_NO_BODY
 // clang-format on
 
 class goto_instrument_parse_optionst:

src/goto-programs/Makefile

@@ -40,6 +40,7 @@ SRC = basic_blocks.cpp \
       read_goto_binary.cpp \
       rebuild_goto_start_function.cpp \
       remove_asm.cpp \
+      remove_calls_no_body.cpp \
       remove_complex.cpp \
       remove_const_function_pointers.cpp \
       remove_exceptions.cpp \

src/goto-programs/goto_inline_class.cpp

@@ -380,59 +380,6 @@ void goto_inlinet::insert_function_body(
   dest.destructive_insert(target, tmp);
 }
 
-void goto_inlinet::insert_function_nobody(
-  goto_programt &dest,
-  const exprt &lhs,
-  goto_programt::targett target,
-  const symbol_exprt &function,
-  const exprt::operandst &arguments)
-{
-  PRECONDITION(target->is_function_call());
-  PRECONDITION(!dest.empty());
-
-  const irep_idt identifier=function.get_identifier();
-
-  if(no_body_set.insert(identifier).second) // newly inserted
-  {
-    warning().source_location=function.find_source_location();
-    warning() << "no body for function `" << identifier << "'" << eom;
-  }
-
-  goto_programt tmp;
-
-  // evaluate function arguments -- they might have
-  // pointer dereferencing or the like
-  forall_expr(it, arguments)
-  {
-    goto_programt::targett t=tmp.add_instruction();
-    t->make_other(code_expressiont(*it));
-    t->source_location=target->source_location;
-    t->function=target->function;
-  }
-
-  // return value
-  if(lhs.is_not_nil())
-  {
-    side_effect_expr_nondett rhs(lhs.type());
-    rhs.add_source_location()=target->source_location;
-
-    code_assignt code(lhs, rhs);
-    code.add_source_location()=target->source_location;
-
-    goto_programt::targett t=tmp.add_instruction(ASSIGN);
-    t->source_location=target->source_location;
-    t->function=target->function;
-    t->code.swap(code);
-  }
-
-  // kill call
-  target->type=LOCATION;
-  target->code.clear();
-  target++;
-
-  dest.destructive_insert(target, tmp);
-}
-
 void goto_inlinet::expand_function_call(
   goto_programt &dest,
   const inline_mapt &inline_map,
@@ -551,7 +498,13 @@ void goto_inlinet::expand_function_call(
   }
   else // no body available
   {
-    insert_function_nobody(dest, lhs, target, function, arguments);
+    const irep_idt identifier = function.get_identifier();
+
+    if(no_body_set.insert(identifier).second) // newly inserted
+    {
+      warning().source_location = function.find_source_location();
+      warning() << "no body for function `" << identifier << "'" << eom;
+    }
   }
 }
 

src/goto-programs/goto_inline_class.h

@@ -172,13 +172,6 @@ class goto_inlinet:public messaget
     const symbol_exprt &function,
     const exprt::operandst &arguments);
 
-  void insert_function_nobody(
-    goto_programt &dest,
-    const exprt &lhs,
-    goto_programt::targett target,
-    const symbol_exprt &function,
-    const exprt::operandst &arguments);
-
   void replace_return(
     goto_programt &body,
     const exprt &lhs);