Block function command line option #1566

polgreen · 2017-11-07T15:32:58Z

Blocks a function by replacing the function body with assume_false.
This is similar to --undefined-function-is-assume-false, but gives the flexibility to havoc undefined functions and block specific functions in one go without needing multiple calls to goto-instrument.

I still need to create a unit test and add it to this pull request, but any early feedback welcome

peterschrammel · 2017-11-07T22:16:24Z

src/goto-instrument/remove_function.cpp

+
+    if(entry->second.body_available())
+    {
+      message.status() << "Removing body of " << identifier


Should be "Blocking"

peterschrammel · 2017-11-07T22:16:43Z

src/goto-instrument/remove_function.cpp

+    else if(entry->second.is_inlined())
+    {
+      message.warning() << "Function " << identifier << " is inlined, "
+                        << "instantiations will not be removed"


"removed" -> "blocked"

peterschrammel · 2017-11-07T22:17:03Z

src/goto-instrument/remove_function.cpp

+    goto_model.goto_functions.function_map.find(identifier);
+
+  if(entry==goto_model.goto_functions.function_map.end())
+    {


run clang-format

peterschrammel · 2017-11-07T22:18:06Z

src/goto-instrument/remove_function.cpp

+    entry->second.body.add_instruction()->make_assumption(false_exprt());
+}
+
+void block_functions(


doxygen here

thk123

Seems good (pending the clang-format and doxygen changes).

thk123 · 2017-11-10T09:51:20Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1521,6 +1529,7 @@ void goto_instrument_parse_optionst::help()
    " --model-argc-argv <n>        model up to <n> command line arguments\n"
    // NOLINTNEXTLINE(whitespace/line_length)
    " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
+    " --block-function <f>         replace body of function <f> with assume(false), effectively block all paths through function\n" // NOLINT(*)


Consider adding (may be repeated) as above to indicate it can be used more than once.

martin-cs · 2017-11-17T14:49:51Z

Seems reasonable enough on first glance. Ping me when the other comments have been applied and the "do not merge" has been removed.

chrisr-diffblue · 2017-11-20T17:29:47Z

src/goto-instrument/remove_function.cpp

@@ -70,3 +70,48 @@ void remove_functions(
  for(const auto &f : names)
    remove_function(goto_model, f, message_handler);
 }
+
+void block_function(


It would be nice to have some Doxygen comments for this function, as @peterschrammel mentioned.

I've now moved the doxygen from the .h file to the .cpp file now, although I understood that in general the rule was to put it in the header file?

smowton

Looks reasonable, some nitpicks on style. @peterschrammel @martin-cs do either of you know of standard terminology for this? "Block" made me think of "basic block" first and foremost. --mark-function-unreachable perhaps?

smowton · 2017-11-22T10:25:58Z

src/goto-instrument/remove_function.cpp

+/// \brief Replace calls to the function with assume(false).
+/// This effectively blocks any paths through the function
+/// or depending on return values from the function.
+/// \param goto_model  input program to be modifier


typo modified

smowton · 2017-11-22T10:26:20Z

src/goto-instrument/remove_function.cpp

+
+/// \brief Replace calls to the function with assume(false).
+/// This effectively blocks any paths through the function
+/// or depending on return values from the function.


return values or side-effects

smowton · 2017-11-22T10:26:46Z

src/goto-instrument/remove_function.cpp

+/// \param identifier  name of function to block
+/// \param message_handler  Error/status output
+void block_function(
+    goto_modelt &goto_model,


indent 2 I think

smowton · 2017-11-22T10:28:03Z

src/goto-instrument/remove_function.cpp

+  {
+    message.status() << "Blocking all calls to " << identifier << messaget::eom;
+
+    Forall_goto_functions(it, goto_model.goto_functions)


Braces around multi-line forall

smowton · 2017-11-22T10:28:21Z

src/goto-instrument/remove_function.cpp

+{
+  messaget message(message_handler);
+
+  goto_functionst::function_mapt::iterator entry=


Spaces around = / ==

smowton · 2017-11-22T10:29:30Z

src/goto-instrument/remove_function.cpp

+        {
+          ins.make_assumption(false_exprt());
+          ins.source_location.set_comment(
+              "`"+id2string(identifier)+"' is undefined");


That's an odd comment. How about "...was explicitly marked unusable by command-line option --block-function"?

smowton · 2017-11-22T10:30:23Z

src/goto-instrument/remove_function.cpp

+          ins.make_assumption(false_exprt());
+          ins.source_location.set_comment(
+              "`"+id2string(identifier)+"' is undefined");
+        }


How about simply replacing the function body, rather than every callsite?

So, originally I did that (have a look at 8708282), but I got into difficulties when it started violating the asset at line 320 of local_bitvector_analysis.cpp:
assert(succ<loc_infos.size())

I attempted to find a solution to this, and ended up deciding to mirror the code in undefined_function_abort_path (which is, in principle, doing a very similar thing)

Do you know how to solve the assertion violation? I assume that loc_infos needs updating somehow, but I wasn't able to work out how

loc_infos is created when local-bitvector-analysis is run, after you've messed with the GOTO programs, so it won't need updating, but this does suggest the alteration somehow left the GOTO program in an inconsistent state. Couldn't say how without some deeper debugging though. I'd be happy to keep this as-is in the meantime, but it'd be a good cleanup to do if time permits.

smowton · 2017-11-22T10:49:25Z

Oh one more thing, should make the name of the cpp / h file consistent with the eventually chosen name for the pass

polgreen · 2017-11-24T10:18:54Z

is "block-calls-to-function" more descriptive? I don't like "mark-function-unreachable" as to me that sounds too similar to "mark-unreachable-functions", I think "make-function-unreachable" might be better, but it's not clear how it is being made unreachable.

The equivalent command for doing this for an undefined function is just "undefined-function-is-assume-false", so we could make this "make-function-assume-false"

smowton · 2017-11-24T10:25:54Z

make-function-assume-false is fine with me

smowton · 2017-11-24T11:14:22Z

Rather than merge develop into this, please rebase this branch on current develop

polgreen · 2017-11-24T11:48:30Z

Yeah, I'm on it. The last rebase was awful, some of the changes to the regression tests for java strings created conflicts in basically every single test.desc. In the end I gave up and checked out develop and cherry-picked my changes on it.

polgreen · 2017-11-30T12:59:39Z

I rebased this on the current branch when I made the last comment, what else is left for me to do?

tautschnig · 2017-11-30T13:19:12Z

I was just confused by the "I'm on it" I guess. Re-assigning to @peterschrammel to evaluate the "Do not merge" and possibly actually approve and merge.

polgreen · 2017-11-30T13:22:29Z

Sorry, I think I posted the comment slightly before I pushed the rebase and then just forgot to post an update

smowton · 2017-11-30T14:43:38Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1521,6 +1530,9 @@ void goto_instrument_parse_optionst::help()
    " --model-argc-argv <n>        model up to <n> command line arguments\n"
    // NOLINTNEXTLINE(whitespace/line_length)
    " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
+    " --make-function-assume-false <f>\n"
+    "                              replace calls to function <f> with assume(false) (may be repeated)\n" // NOLINT(*)
+    "                              through function (may be repeated).\n"


smowton

Think the help text has got mangled, otherwise lgtm

Blocks all paths through a function by replacing the function calls with assume_false. This is similar to --undefined-function-is-assume-false, but gives the flexibility to havoc undefined functions and block specific functions without needing multiple calls to goto-instrument. Needed for aggressive slicer work

polgreen · 2017-12-04T11:53:10Z

help text is fixed

martin-cs · 2017-12-15T23:52:29Z

I don't want to be That Guy but ... would this be best addressed as part of a comprehensive solution to : #1585 ?

polgreen · 2017-12-16T18:24:07Z

I think the suggested solution to #1585 was to create stub bodies for the functions and insert the changes into the stub bodies.

Originally that is what I did for this PR and there is a discussion with @smowton about this in the comments above. I created stub bodies for the functions and inserted "assume(false)" into the stub bodies. This change was fine when I applied it to the version of CBMC I was using at the time. When I applied it to develop it caused violation of the assert at line 320 of local_bitvector_analysis.cpp:
assert(succ<loc_infos.size())

I couldn't fix this and decided it made sense to mirror the code in undefined_function_abort_path instead (which is doing a very similar thing).

So, the options are:

this pull request could be left consistent with undefined_function_abort_path
this pull request could be changed to create a stub body and add instructions to it, but I would need some help debugging the assertion violation described above. It will then be inconsistent with undefined_function_abort_path.
all the possible ways of handling undefined functions could be changed to be consistent. I don't have time to do this before the end of January, so if this is the solution it's best it is assigned to someone else

martin-cs · 2017-12-18T15:31:37Z

Assorted thoughts...

The assertion failure looks like a corrupted goto-program. The most obvious source is not calling update() after modifying it. Without code it is harder to be clear.
Consistency, especially between similar tasks, if good but shouldn't keep us going down the wrong road (if we are).
Given the variety of behaviours that are potentially desirable for functions without bodies and the need for consistency between back-ends I think the "transform the program" approach is the right way forward.

I'm certainly happy to review, probably to help program even but it will have to be late January at the earliest.

polgreen requested review from martin-cs, peterschrammel and thk123 as code owners November 7, 2017 15:32

peterschrammel reviewed Nov 7, 2017

View reviewed changes

thk123 approved these changes Nov 10, 2017

View reviewed changes

peterschrammel added the do not merge label Nov 10, 2017

polgreen mentioned this pull request Nov 14, 2017

Aggressive slicer #1587

Closed

polgreen requested review from cesaro, chrisr-diffblue, forejtv, kroening, mgudemann, smowton and tautschnig as code owners November 20, 2017 16:45

polgreen force-pushed the block_function branch from 49ae8f9 to 7ba26cf Compare November 20, 2017 16:46

chrisr-diffblue reviewed Nov 20, 2017

View reviewed changes

smowton reviewed Nov 22, 2017

View reviewed changes

polgreen force-pushed the block_function branch from c0cb108 to dd63f78 Compare November 24, 2017 11:08

polgreen force-pushed the block_function branch from c105a90 to 7343adb Compare November 24, 2017 11:41

tautschnig assigned polgreen Nov 30, 2017

tautschnig assigned peterschrammel and unassigned polgreen Nov 30, 2017

smowton reviewed Nov 30, 2017

View reviewed changes

smowton approved these changes Nov 30, 2017

View reviewed changes

tautschnig assigned polgreen Nov 30, 2017

polgreen and others added 2 commits December 3, 2017 12:37

Regression tests for make-function-assume-false

7d80a52

polgreen force-pushed the block_function branch from 7343adb to 7d80a52 Compare December 3, 2017 12:39

tautschnig unassigned polgreen Dec 4, 2017

tautschnig mentioned this pull request Feb 27, 2018

Add option to generate function body to goto-instrument #1889

Merged

tautschnig mentioned this pull request Apr 27, 2018

Lazy methods: allow driver program to provide stubs #2124

Merged

polgreen closed this Jun 20, 2018

polgreen deleted the block_function branch June 27, 2018 08:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Block function command line option #1566

Block function command line option #1566

polgreen commented Nov 7, 2017

peterschrammel Nov 7, 2017

peterschrammel Nov 7, 2017

peterschrammel Nov 7, 2017

peterschrammel Nov 7, 2017

thk123 left a comment

thk123 Nov 10, 2017

martin-cs commented Nov 17, 2017

chrisr-diffblue Nov 20, 2017

polgreen Nov 21, 2017

smowton left a comment

smowton Nov 22, 2017

smowton Nov 22, 2017

smowton Nov 22, 2017

smowton Nov 22, 2017

smowton Nov 22, 2017

smowton Nov 22, 2017

smowton Nov 22, 2017

polgreen Nov 22, 2017

smowton Nov 22, 2017

smowton commented Nov 22, 2017

polgreen commented Nov 24, 2017

smowton commented Nov 24, 2017

smowton commented Nov 24, 2017

polgreen commented Nov 24, 2017

polgreen commented Nov 30, 2017

tautschnig commented Nov 30, 2017

polgreen commented Nov 30, 2017

smowton Nov 30, 2017

smowton left a comment

polgreen commented Dec 4, 2017

martin-cs commented Dec 15, 2017

polgreen commented Dec 16, 2017

martin-cs commented Dec 18, 2017

Block function command line option #1566

Block function command line option #1566

Conversation

polgreen commented Nov 7, 2017

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

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented Nov 17, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton 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

smowton commented Nov 22, 2017

polgreen commented Nov 24, 2017

smowton commented Nov 24, 2017

smowton commented Nov 24, 2017

polgreen commented Nov 24, 2017

polgreen commented Nov 30, 2017

tautschnig commented Nov 30, 2017

polgreen commented Nov 30, 2017

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

polgreen commented Dec 4, 2017

martin-cs commented Dec 15, 2017

polgreen commented Dec 16, 2017

martin-cs commented Dec 18, 2017