Replace function calls with calls to other functions #2705

danpoe · 2018-08-09T17:55:29Z

This adds an option --replace-calls f:g (can be repeated) to cbmc and goto-instrument which replaces calls to function f by calls to function g. A use case is to replace certain functions by simpler stubs for analysis.

tautschnig · 2018-08-09T18:04:30Z

src/goto-programs/Makefile

@@ -67,6 +67,7 @@ SRC = adjust_float_expressions.cpp \
      wp.cpp \
      write_goto_binary.cpp \
      xml_goto_trace.cpp \
+      replace_calls.cpp \


Please maintain lexicographic sorting.

tautschnig · 2018-08-09T18:05:41Z

src/cbmc/cbmc_parse_options.cpp

@@ -193,6 +193,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
  if(cmdline.isset("nondet-static"))
    options.set_option("nondet-static", true);

+  if(cmdline.isset("replace-calls"))


I'm not too convinced that adding this to CBMC is a good idea - it has too many command-line options already.

It does feel a bit more like a linker / goto-instrument kind of feature. It seems like it would be happy living with --remove-function-body and --generate-function-body.

tautschnig · 2018-08-09T18:06:29Z

regression/cbmc/replace-calls-01/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>


Random place: the description provided in the PR is way more useful than the commit message - could the latter please be updated?

tautschnig · 2018-08-09T18:07:28Z

src/goto-programs/replace_calls.cpp

+  {
+    goto_functionst::goto_functiont &goto_function = p.second;
+
+    if(!goto_function.body_available())


I think this is unnecessary, the invoked function is perfectly safe for an empty body.

peterschrammel · 2018-08-09T22:21:56Z

regression/goto-instrument/replace-calls-05/main.c

@@ -0,0 +1,5 @@
+


remove blank line (same in other files)

Ok, done (but github doesn't seem to notice).

peterschrammel · 2018-08-09T22:23:09Z

regression/goto-instrument/replace-calls-05/test.desc

+CORE
+main.c
+--replace-calls f:g --replace-calls h:f
+Function f cannot both be replaced and be a replacement


What happens if I replace the entry point (potentially specified by --function)?

Can you add a test involving function pointers?

Ok, I've added a test that involves function pointers.

Regarding the entry point replacement with --function, were you meaning that the error message should be more specific to indicate that it's coming from the replace calls analysis?

If it is saying the usual 'No entry point found' then this is fine. An invariant violation would not be ok.

The replace calls pass works both when an entry point is present and when not (goto-instrument does not check whether an entry point is present). Also it cannot be used to replace the entry point, as it replaces calls not functions and the entry point is not called by anything.

peterschrammel · 2018-08-09T22:24:22Z

src/goto-instrument/goto_instrument_parse_options.h

@@ -97,7 +98,8 @@ Author: Daniel Kroening, [email protected]
  OPT_REMOVE_CALLS_NO_BODY \
  OPT_REPLACE_FUNCTION_BODY \
  OPT_GOTO_PROGRAM_STATS \
-  "(show-local-safe-pointers)(show-safe-dereferences)"
+  "(show-local-safe-pointers)(show-safe-dereferences)" \
+  OPT_REPLACE_CALLS


put \ at the end, and // empty last line in the next line to make diffs more readable in future

peterschrammel · 2018-08-09T22:25:55Z

src/goto-programs/replace_calls.cpp

+    auto f_it2 = goto_functions.function_map.find(new_id);
+
+    if(f_it2 == goto_functions.function_map.end())
+      throw "Replacement function " + id2string(new_id) +


Use proper user input exceptions?

Yes. PR #2703 introduces an invalid_user_input_exceptiont. Once it's merged we'll change most throws in here to throw that one (as part of the error handling cleanup).

I think this should be checked when things are set up / parsed rather than during the operation; but that may just be me.

peterschrammel · 2018-08-09T22:26:29Z

src/goto-programs/replace_calls.cpp

+      {
+        const symbol_exprt &se = to_symbol_expr(rhs);
+        if(has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX))
+          throw "Returns must not be removed before replacing calls";


DATA_INVARIANT?

Rather a precondition?

We could potentially get a goto binary in which returns have been removed by some previous analysis. Thus I think this should be an invalid user input exception.

peterschrammel · 2018-08-09T22:28:21Z

src/goto-programs/replace_calls.cpp

+    exprt &function = cfc.function();
+
+    if(function.id() != ID_symbol)
+      throw "Function pointer calls must be removed before replacing calls";


DATA_INVARIANT?

Or probably better a PRECONDITION.

martin-cs

Mostly discussion. Over all seems good. I do think it should be goto-instrument rather than CBMC.

martin-cs · 2018-08-10T13:09:31Z

src/goto-programs/replace_calls.cpp

+    code_function_callt &cfc = to_code_function_call(ins.code);
+    exprt &function = cfc.function();
+
+    PRECONDITION(function.id() == ID_symbol);


This implies function pointer removal, right?

martin-cs · 2018-08-10T13:13:32Z

src/goto-programs/replace_calls.cpp

+
+    INVARIANT(
+      f_it1 != goto_functions.function_map.end(),
+      "Called functions need to be present");


This is a post condition of linking, right?

martin-cs · 2018-08-10T13:14:21Z

src/goto-programs/replace_calls.cpp

+    auto f_it2 = goto_functions.function_map.find(new_id);
+
+    if(f_it2 == goto_functions.function_map.end())
+      throw "Replacement function " + id2string(new_id) +


I think this should be checked when things are set up / parsed rather than during the operation; but that may just be me.

martin-cs · 2018-08-10T13:15:04Z

src/goto-programs/replace_calls.cpp

+
+    if(!base_type_eq(cur_goto_function.type, new_goto_function.type, ns))
+      throw "Functions " + id2string(id) + " and " + id2string(new_id) +
+        " are not type-compatible";


Likewise; this seems like option checking.

martin-cs · 2018-08-10T13:16:04Z

src/goto-programs/replace_calls.cpp

+      throw "Functions " + id2string(id) + " and " + id2string(new_id) +
+        " are not type-compatible";
+
+    // check that returns have not been removed


OK; so function pointer removal but not return removal? This fits with goto-instrument but not CBMC. It seems like the kind of thing that should be documented.

Yes, if it would be used directly in cbmc it would need to be inserted after the function pointer removal and before the return removal.

martin-cs · 2018-08-10T13:17:06Z

src/goto-programs/replace_calls.cpp

+}
+
+replace_callst::replacement_mapt replace_callst::parse_replacement_list(
+  const replacement_listt &replacement_list) const


See, I think the checking whether they are defined, checking types, etc. should be done here.

…ions.h

danpoe · 2018-08-13T09:57:20Z

Ok, I think I've addressed all the comments.

tautschnig · 2018-08-13T11:43:51Z

src/cbmc/cbmc_parse_options.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/goto_check.h>

 #include <goto-programs/goto_trace.h>
+#include <goto-programs/replace_calls.h>


This shouldn't be necessary anymore.

tautschnig · 2018-08-13T11:45:17Z

src/goto-programs/replace_calls.cpp

+
+#include <util/base_type.h>
+#include <util/invariant.h>
+#include <util/irep.h>


I don't think this is necessary, it will have been included several times already.

Hm, I think there's some merit to the idea of explicitely including everything that is used and not relying on transitive includes. If for example A includes B and B includes C, and A uses symbols from C, then B could not be refactored to not include C anymore without also having to change A (also see https://github.com/include-what-you-use/include-what-you-use/blob/master/docs/WhyIWYU.md, section "Allow Refactoring").

I do subscribe to this principle, but then you'll have to be consistent about it and include std_code.h, namespace.h and likely a few more.

Ok, cool. Yeah true, I actually need to include several more.

I don't see where irept is used explicitly here.

It uses irep_idt which is defined in irep.h.

Adds an option --replace-calls f:g (can be repeated) to goto-instrument which replaces calls to function f by calls to function g. A use case is to replace certain functions by simpler stubs for analysis.

4f5e148 Merge pull request diffblue#2713 from thk123/dump/expr2c-configuration 01b7418 Merge pull request diffblue#2710 from thomasspriggs/tas/struct_component b763877 Merge pull request diffblue#2737 from diffblue/remove-appveyor 9c3fd45 Add AWS CodeBuild badges 4261fd8 Remove appveyor badge fe23db7 Remove appveyor.yml 21857a7 Add support for getting components by name to `struct_exprt` 05993f4 Merge pull request diffblue#2727 from tautschnig/fptr-debug 0ecd008 Merge pull request diffblue#2701 from antlechner/antonia/enum-constants 159bf15 Merge pull request diffblue#2205 from diffblue/rename_symbol_type 5ca6cd2 Restrict new clinit_wrapper calls to enum types 6e04213 Reformatting the structs to aid readability 0cfacb8 Add type2c conversion for specifying a type name c3fef70 Add a clean configuration for expr2c 3a40db1 Make expr2ct configurable in a number of ways 097cf71 Merge pull request diffblue#2731 from diffblue/increase-version 170c1ea Merge pull request diffblue#2730 from diffblue/parent-child-invariant c9e46ae Temporarily remove new UNREACHABLE statements 03e3877 Add tests for nondet initialization of enums 3e32140 CI lazy methods: load clinit for all param types 5542c54 Move nondet enum initialization to new function 6ecf4f9 Nondet-init enums by assigning them to a constant 6c84caa Refactor logic for generating a nondet int 07d1e44 Always run clinit_wrapper before nondet object init 3be826f Add some documentation to java_object_factory 5e80310 add invariant on parent-child class relationship 2cf1931 Merge pull request diffblue#2661 from jeannielynnmoulton/jeannie/JavaMethodType c6acc9c increased version number in preparation for release 5.10 0ee4178 Merge pull request diffblue#2729 from tautschnig/add-sub-conflict f5aff56 Merge pull request diffblue#2705 from danpoe/feature/replace-function-calls 89048e6 Function-pointer remvoval: print human-friendly debug messages 1fc3118 Use pointer difference type when adding to pointer 072b592 Merge pull request diffblue#2726 from tautschnig/java-loc 4dca215 Goto program should not use java_method_typet 273fff4 Add can_cast_type and precondition. 6cb7e5d Reinstate require_code and add require_java_method 78f7cb7 Refactor constructors for java_method_typet 6cefc61 Unit tests conversion from code_typet to java_method_typet c3b8b5a Update tag in to_java_method_type 972315a Update docs on java_method_typet constructor 211931c Add tag for java_method_type 551df9c Update unit tests to use java_method_typet da18c9f Change variables named code_type to method_type f1bd41e Change code_typet to java_method_typet in jbmc be3c4c6 Merge pull request diffblue#2430 from tautschnig/vs-function-id 03fa885 Replace function calls c4d79ab Java string preprocessing: use provided source location fb0c552 Java string preprocessing: use and document parameter function_id c31edca Merge pull request diffblue#2725 from tautschnig/replace-symbolt-code-type 2c1fc06 Merge pull request diffblue#2721 from tautschnig/replace_symbol-cleanup2 8211a78 Merge pull request diffblue#2722 from tautschnig/cleanup-valuest 30bc071 Add "// empty last line" to options list in goto_instrument_parse_options.h 8c8801c List source files in goto-programs/Makefile in lexicographic order 40d28ae replace_symbolt: report replacements in code_typet::return_type 4b9df3b Revert "Ignore return value" e39ea2e Merge pull request diffblue#2683 from karkhaz/kk-continue-unsafe 424ab4f --stop-on-fail now stops on failed path 545bff8 Add clear() to path exploration worklist 95d8d0f Generalise option setting from strategy unit tests e85fb77 Cleanup constant_propagator_domaint::valuest 18d08bf Merge pull request diffblue#2719 from tautschnig/quiet-unit-tests 30d557a Constant propagation: Check type consistency before adding to replacement map a5ce621 Make unit tests quiet 61b3086 Merge pull request diffblue#2468 from tautschnig/vs-names 7bfd36b Merge pull request diffblue#2714 from diffblue/msvc-asm 3785941 Remove names of unused parameters af79cb9 add support for Visual Studio style inline assembler 254b4d4 Merge pull request diffblue#2642 from diffblue/remove_asm_fix 26009a3 remove_asm now guarantees that functions called exist 9c10f38 Merge pull request diffblue#2716 from tautschnig/fix-buildspec c3b2beb Merge pull request diffblue#2635 from qaphla/move_is_lvalue e247a29 CodeBuild: Remove empty artifact stanza 756018d Merge pull request diffblue#2709 from owen-jones-diffblue/doc/how-to-run-tests bba5dea Merge pull request diffblue#2699 from diffblue/goto-cc-clang 355fbd2 avoid assert() 6178908 bump goto binary version f93deec type symbols now use ID_symbol_type 22b755a Merge pull request diffblue#2711 from diffblue/mode-gcc-asm-functions cf75535 Merge pull request diffblue#2702 from owen-jones-diffblue/doc/minor-fixes-to-cprover-developer-documentation 5c06786 set mode for functions added by remove_asm ef53b65 Update description of regression test framework 312ca1d Add section to documentation about running tests d7ddf59 Merge pull request diffblue#2700 from romainbrenguier/clean-up/side-effect-location 119e88b Pass location around for nondet initialization 50660db Specify source location for nondet expressions d1f2ad9 Replace -> with → e448db6 Merge pull request diffblue#2708 from owen-jones-diffblue/coding-standard-class-comments 519370d State that identifiers should be good 30d29b9 Replace unicode arrows → with ascii ones -> 611374f Document classes and member variables unless obvious adb7ef0 Minor fixes to documentation outline fd4f563 Add side_effect_exprt constructor with location 98657d8 Merge pull request diffblue#2668 from diffblue/expose_remove_preconditions 6a36fa4 Merge pull request diffblue#2615 from owen-jones-diffblue/doc/cbmc-developer-guide 61a8c30 Merge pull request diffblue#2666 from NlightNFotis/invariant_changes c0bcce7 use clang as native compiler for goto-clang 1f19e23 goto-cc: use result of our native compiler detection d9d9e2a Merge pull request diffblue#2692 from diffblue/follow-tags f94d5e2 follow union, struct and enum tags 99e33bd fix typo in comments for struct_tag_typet 1f53246 expose remove_preconditions f212505 Avoids using expr.op0 when type is known 7b36ca2 Moves is_lvalue to expr_util.c 4782b48 Fix invariant regression tests efb1c40 Refactor invariant_failedt definition. 515f050 Pass the condition to the invariant_failedt constructor. bf6dd9e Added extra use-case hints to the already present invariant definitions. 612b4f8 Address review comments 7233f92 Rearrange everything into separate pages 1cb3cdd Move other tools into a separate file 82eefb7 Fix links between files d9e690b Move folder walkthrough to a separate file 2939db4 Address review comments 8d5cbcb Create CBMC developer guide documentation git-subtree-dir: cbmc git-subtree-split: 4f5e148

danpoe requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners August 9, 2018 17:55

danpoe force-pushed the feature/replace-function-calls branch from cfcb6b1 to 9dfa375 Compare August 9, 2018 18:00

tautschnig reviewed Aug 9, 2018

View reviewed changes

peterschrammel reviewed Aug 9, 2018

View reviewed changes

danpoe force-pushed the feature/replace-function-calls branch 2 times, most recently from e13014e to d6147f5 Compare August 10, 2018 12:35

martin-cs reviewed Aug 10, 2018

View reviewed changes

danpoe force-pushed the feature/replace-function-calls branch 3 times, most recently from d583cae to ff80a1d Compare August 10, 2018 14:56

danpoe added 2 commits August 13, 2018 10:47

List source files in goto-programs/Makefile in lexicographic order

8c8801c

Add "// empty last line" to options list in goto_instrument_parse_opt…

30bc071

…ions.h

danpoe force-pushed the feature/replace-function-calls branch from ff80a1d to 6c2ce6f Compare August 13, 2018 09:54

tautschnig approved these changes Aug 13, 2018

View reviewed changes

Replace function calls

03fa885

Adds an option --replace-calls f:g (can be repeated) to goto-instrument which replaces calls to function f by calls to function g. A use case is to replace certain functions by simpler stubs for analysis.

danpoe force-pushed the feature/replace-function-calls branch from 6c2ce6f to 03fa885 Compare August 13, 2018 13:06

peterschrammel approved these changes Aug 13, 2018

View reviewed changes

peterschrammel assigned danpoe Aug 13, 2018

peterschrammel added the new feature label Aug 13, 2018

kroening merged commit f5aff56 into diffblue:develop Aug 13, 2018

danpoe deleted the feature/replace-function-calls branch June 2, 2020 17:18

Replace function calls with calls to other functions #2705

Replace function calls with calls to other functions #2705

Conversation

danpoe commented Aug 9, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe commented Aug 13, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe commented Aug 9, 2018 •

edited

Loading