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"