-
Notifications
You must be signed in to change notification settings - Fork 285
Add option to generate function body to goto-instrument #1889
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add option to generate function body to goto-instrument #1889
Conversation
|
May I start with a few questions:
|
|
43613c1 to
9d874aa
Compare
hannes-steffenhagen-diffblue
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add a test for function name regex
Add a test for replace-function-body-options skip
Add an option for assert-false-then-assume-false
| " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*) | ||
| // NOLINTNEXTLINE(whitespace/line_length) | ||
| " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) | ||
| " convert each call to an undefined function to assume(false)\n" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Removed text that should still be there
| { | ||
| function.body.clear(); | ||
| generate_parameter_names(function, symbol_table, function_name); | ||
| replace_function_body_impl(function, symbol_table, function_name); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should be "generate_function_body", because the body has already been removed here
| goto_functiont &function, | ||
| symbol_tablet &symbol_table, | ||
| irep_idt function_name) override | ||
| { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Put a skip instruction here or rename this to empty
| public: | ||
| havoc_replace_function_bodiest( | ||
| std::vector<irep_idt> globals_to_havoc, | ||
| bool havoc_parameters) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Use regex for parameter instead of all-in boolean parameter
| bool havoc_parameters; | ||
| }; | ||
|
|
||
| std::unique_ptr<replace_function_bodiest> parse_replace_function_body_options( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Rename this to "factory..."
| const std::regex &functions_regex, | ||
| const std::string &replace_options) | ||
| { | ||
| messaget messages; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
pass this as parameter instead
| Module: Replace bodies of goto functions | ||
| Author: DiffBlue Limited. All rights reserved. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't use "All rights reserved"
|
For the record, the comments above are a composite of mine and @chrisr-diffblue 's reviews of this done sat with @hannes-steffenhagen-diffblue . Beyond these we are happy to merge this. |
|
There are questions of condensing other options and other functionality. This patch is the first step of a not-as-covert-as-it-was-before-I-started-writing-this attempt to remove the special case code for functions without bodies from the various analyses. In line with this I think we should also:
@tautschnig @peterschrammel opinions? Also @polgreen does the functionality in this PR cover the use cases you had for #1566 and #1585 ? |
|
@hannes-steffenhagen-diffblue : one thing I forgot when we were writing up the review, can we have an option --generate-function-bodies which is --replace-function-body for all functions which don't have a body at the moment. |
9d874aa to
1c9b407
Compare
54ca23e to
b80eea6
Compare
9efca43 to
ea1f752
Compare
|
@martin-cs I think that's all the comments addressed, except for the option merging thing (maybe separate PR?). Mind taking another look? |
thk123
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not reviewed tests
| ^SIGNAL=0$ | ||
| ^VERIFICATION FAILED$ | ||
| ^\[main.assertion.1\] assertion does_not_get_reached: SUCCESS$ | ||
| ^\[should_be_generated.assertion.1\] assertion FALSE: FAILURE$ No newline at end of file |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Missing new line
| std::regex function_regex = std::regex( | ||
| only_generate ? cmdline.get_value("generate-function-body") | ||
| : cmdline.get_value("replace-function-body")); | ||
| status() << "Replacing function bodies" << eom; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this method say "Generating function bodies" if cmdline.get_value("generate-function-body")
| "(splice-call):" \ | ||
| OPT_REMOVE_CALLS_NO_BODY | ||
| OPT_REMOVE_CALLS_NO_BODY \ | ||
| "(replace-function-body):" \ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
But these options and their documentation in to replace_function_bodies.h to make it easier for it to be reused in different front ends.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As a define like some of the other options?
| cmdline.isset("replace-function-body") || | ||
| cmdline.isset("generate-function-body")) | ||
| { | ||
| if( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have a mild preference to remove this code from here and put into the constructor of replace_function_bodiest so that the logic of how these parameters are handled is separated from the specific binary being used.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was actually the opposite; I had considered doing the parsing of the arguments outside of replace_function_bodiest entirely to avoid passing more "meaningful" strings around than we really have to
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My reason was that if someone wishes to re-use this they must copy/paste the interface to provide a consistent experience for the user. Rather than passing raw strings, what if you pass the whole cmdlinet into it? So it is clear they aren't meaningful strings but really the user input.
The down side to my suggestion is becomes a class that is both responsible for generating functions and parsing command line args. Perhaps it would be better to have a third place that takes a cmdline and returns a replace_goto_functionst, but OK with leaving that to the first person who wishes to re-use this code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd like to support @thk123's position: In order to achieve what #1949 says, we will need this in all front-ends. So we really don't want to reimplement the command-line parsing multiple times. In my opinion, the last suggestion to have "a third place that takes a cmdline and returns..." is the best approach.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Pushing the only_generate and function_regex logic into a reusable helper in replace_function_bodies would be preferable.
| throw replace_function_body_parse_error("Can't parse \"", options, "\""); | ||
| } | ||
|
|
||
| void replace_function_bodies( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As the interface to this whole functionality, could you add documentation here.
| } | ||
| }; | ||
|
|
||
| class assume_false_replace_function_bodiest : public replace_function_bodiest |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Consider documenting each of these classes with:
a) the arugments needed to use them
b) a C style code block of what will be produced
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You might also consider writing some really simple unit tests for each of these classes to verify the program produced.
| { | ||
| if( | ||
| parameter.type().id() == ID_pointer && | ||
| !parameter.type().subtype().get_bool(ID_C_constant) && |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure, but perhaps this is the same condition as is_constant_or_has_constant_components (e.g. is pointer to a pointer to a constant?)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure; Actually it's also possible that this is the better version; i.e. you can absolutely assign a pointer-to-pointer-to-constant. Then again, structs with constant members usually aren't assignable so I'm not 100% clear on what the correct way to do this here is
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Consider writing unit tests to figure out - I think it should be clear what is "correct" when you do this
| }; | ||
|
|
||
| static std::vector<std::string> | ||
| tokenize(const std::string &base, char separator) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Document? Also surely this code exists somewhere already? Is it not split_string in string_utils.cpp?
| } | ||
|
|
||
| static void write_to_stream(std::ostream &out) | ||
| { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
huh?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is just to have a convenient method to assemble a string... Didn't end up actually needed it here so I'm removing it, but I figure something along those lines might be useful for string-utils?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe? I'll reserve judgement until I see a PR with it being used 😛
| const std::vector<std::string> key_value_pair = tokenize(tokens[i], ':'); | ||
| if(key_value_pair.size() != 2) | ||
| { | ||
| throw replace_function_body_parse_error( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Avoid introducing throw std::string type statements, consider having a replace_function_body_exceptiont for this
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should it be a child of std::runtime_error? If yes, should the message include __FILE__ and __LINE__?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They both sound like sensible suggestions to me.
ea1f752 to
ca0553a
Compare
|
@thk123 I think I've addressed most of your comments, mind having another look? |
| #include <util/message.h> | ||
|
|
||
| /// Replace function bodies with some default behavior | ||
| /// Can generate the following types of function bodies: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Explain the lhs of this list is the command line argument
| /// return nondet_int(); | ||
| /// } | ||
| /// | ||
| /// nondet-return return nondet for non-void functions |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: nondet-return: return nondet for non-void functions (missing colon separating command line from result)
| /// @param functions_regex Replace bodies of functions whose names matches regex | ||
| /// @param only_generate When true, skip functions that already have a body | ||
| /// @param replace_options Options string indicating what body to generate | ||
| /// @param messages Destination for status/warning messages |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
\param also this documentation should go in the cpp next to the implementation rather than the header (as per coding guidelines)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I also think it would be more useful to split each up to go with the corresponding class but that might just be personal preference
| new_param_sym.type = parameter.type(); | ||
| new_param_sym.base_name = param_base_name; | ||
| new_param_sym.mode = ID_C; | ||
| auto &function_symbol = symbol_table.lookup_ref(function_name); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it is clearer if you make the const here explicit.
| { | ||
| if( | ||
| parameter.type().id() == ID_pointer && | ||
| !parameter.type().subtype().get_bool(ID_C_constant) && |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Consider writing unit tests to figure out - I think it should be clear what is "correct" when you do this
0ae6a9f to
44fb0b1
Compare
|
@peterschrammel @thk123 @tautschnig @martin-cs Can you please check whether or not you feel that your comments have been addressed? |
tautschnig
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks a lot for the updates; still a few smaller issues, but mainly I'm wondering about the set options/the discussion around that, if it has taken place.
| Module: Replace bodies of goto functions | ||
| Author: DiffBlue Limited. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See #1919.
| }; | ||
| auto assert_instruction = add_instruction(); | ||
| assert_instruction->make_assertion(false_exprt()); | ||
| // assert_instruction->code = code_assertt(false_exprt()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No need for this commented-out code, please remove.
| { | ||
| throw replace_function_bodies_errort( | ||
| "can only use one of --replace-function-body " | ||
| "or --generate-function-body"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@hannes-steffenhagen-diffblue @peterschrammel - did you discuss this? What was the conclusion, or maybe why was my proposal not acceptable?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@tautschnig Nobody else said anything about this. It's possible that they missed it. I wouldn't mind implementing it that way, but it wasn't obviously better than the current behaviour from my perspective, I'd prefer at least one other person saying they think it's the better way to do it before going ahead with changing the options at this point.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Poking @martin-cs @chrisr-diffblue with the hope that more people might chime in. Everyone: see the discussion in #1889 (comment) for context.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've left a comment in that discussion thread - but bottom line is that I agree with @tautschnig's proposal.
| /// A list of currently accepted command line arguments | ||
| /// + the type of bodies generated by them | ||
| /// | ||
| /// assert-false: { __CPROVER_assert(false); } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
__CPROVER_assert takes a second argument.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah. I should probably just use assert here, the __CPROVER doesn't really add to the legibility of the example
| Module: Replace bodies of goto functions | ||
| Author: DiffBlue Ltd. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
| #include <util/std_types.h> | ||
| #include <util/message.h> | ||
| #include <goto-programs/goto_model.h> | ||
| #include <util/cmdline.h> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please try to sort internal includes lexicographically.
thk123
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
New changes seem fine but I think a bit more context on the slightly wrong test would be in order.
| havoc_struct(¶mStruct); | ||
| assert(globalStruct.non_const == 10); | ||
| assert(globalStruct.is_const == 20); | ||
| assert(paramStruct.non_const == 11); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this not been havoced? (A good technique for trying to verify these tests is to try and write bodies that violate this asserts, for example for this can you not do:
(*WithConstMember).non_const = 20;| const irep_idt &function_name); | ||
|
|
||
| private: | ||
| /// Generate parameter names for unnamed parameters. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Comments should go with the implementation
| @@ -0,0 +1,410 @@ | |||
| /*******************************************************************\ | |||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm assuming this is a move of the original?
| { | ||
| struct WithConstMember paramStruct = {11, 21}; | ||
| havoc_struct(¶mStruct); | ||
| assert(globalStruct.non_const == 10); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In fact - since you are also havocing globals, shouldn't this assert fail too?
| } | ||
| else if(!parameter.type().subtype().get_bool(ID_C_constant)) | ||
| { | ||
| warning() << "warning: not havoccing non-const pointer parameter '" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah I see - this is why the tests are "wrong". I assume there is an issue? Probably worth ensuring this warning appears in the test and there is an appropriate comment on the issue to update the test.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is all intended behaviour for now, I had asked around what people thought the right behaviour should be and it was "just skip structs with const members for now". The other behaviour is also possible, would that be your preference then?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
On the face of it it seems more "correct" as I can easily write a method body for that method that violates that assert without wandering into undefined behaviour or even something particularly odd. That said, I'm not using this tool on a regular basis, it might be in the real world this is simply a more useful behaviour.
|
@thk123 I've now changed the behaviour so that structs, unions and arrays are traversed during havoccing instead of giving up when they contain constant elements. |
177a60a to
38ee140
Compare
|
There is some documentation about the feature in |
e835e6b to
8958d37
Compare
|
I have rebased the changes onto the newest develop. Apologies for any inconveniences. |
thk123
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for changes and docs. I would suggest if the (?!__) thing is so important, you may want to add a warning in the code if the supplied regex matches __CPROVER since most people won't read the manual...
| ^\[main.assertion.6\] assertion globalUnion.is_const == 10: FAILURE$ | ||
| ^\[main.assertion.7\] assertion paramUnion.non_const == 20: FAILURE$ | ||
| ^\[main.assertion.8\] assertion paramUnion.is_const == 20: FAILURE$ | ||
| ^VERIFICATION FAILED$ No newline at end of file |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Missing new line
|
This is approaching the point where GH refuses to load this page due to too many comments. It might be wise to close this and open a new PR if there are still outstanding comments. |
|
@thk123 I might just end up doing that. Technical issues aside, it's starting to get to the point of being difficult to follow along with a lot of the discussion no longer being relevant due to code changes |
|
From my point of view this is very close to be ready to be merged (but others might disagree). I'd actually just suggest to squash the commit series into a few meaningful commits, re-review, approve, and be happy :-) |
616cfd1 to
29d9882
Compare
|
@tautschnig I believe this is in a good state now. Would you mind taking another look at this once CI passes? |
tautschnig
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think there is further room for cleaning up the closely related options, but certainly this is a good piece of work to go in and further work can follow.
One wishlist request: please put a comment in the CHANGELOG file, this is a user-visible feature.
| ^\[main.assertion.6\] assertion globalUnion.is_const == 10: FAILURE$ | ||
| ^\[main.assertion.7\] assertion paramUnion.non_const == 20: FAILURE$ | ||
| ^\[main.assertion.8\] assertion paramUnion.is_const == 20: FAILURE$ | ||
| ^VERIFICATION FAILED$ No newline at end of file |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Github says there's no newline here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed
| " --check-invariant function instruments invariant checking function\n" | ||
| " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) | ||
| " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*) | ||
| " --undefined-function-is-assume-false\n" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could we mark this as deprecated (possibly be removing it from help output, but leaving it in the .h file)? Also: is it now implemented via the new options? (Just being lazy, I should be able to figure out once I've completely read the code.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The effect can be replicated with --generate-function-body '.*' --generate-function-body-options assume-false
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes indeed - but then we could get rid of the code implementing undefined_function_abort_path, couldn't we?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@hannes-steffenhagen-diffblue I'd leave it to you whether to include such changes in this PR or instead just create an issue and make someone else (such as myself...) fix it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've created #2070 to cover the additional cleanup and will merge this PR now.
| "(splice-call):" \ | ||
| OPT_REMOVE_CALLS_NO_BODY | ||
| OPT_REMOVE_CALLS_NO_BODY \ | ||
| OPT_REPLACE_FUNCTION_BODY |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this might not be worth renaming to OPT_GENERATE...?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done
29d9882 to
ebfaf5a
Compare
|
@tautschnig I added a short reference to the new option in CHANGELOG under a new "5.9" section |
ebfaf5a to
7952f2c
Compare
chrisr-diffblue
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good - thanks for all the extra work and polishing on this PR.
|
I know this PR has already been merged, but I have a question about the documentation: " /// Replace the function body with one based on the implementation Does "implementation" have a specific meaning, I thought it just meant the actual function body? I'm not sure how you would replace the function body with one based on the function body if there is no function body, or, if there is a body, how the body that it replaces the body with is based on the original body? |
This adds the commandline parameters
--replace-function-bodyand--replace-function-body-options. The first gets a regex that defines a set of functions whose body should be replaced; Whereas the latter specifies what kind of body should be generated. The options here are:nondet-returnsame ashavocwithout further optionsassert-falsegenerate a singleassert(false);in the body.assume-falsegenerate a singleassume(false);in the body (this has a similar effect to--undefined-function-is-assume-false)havoc[,params][,globals:<regex>]which generates areturn nondetfor non-voidfunctions and assignsnondetto the targets of pointers to non-constifparamsis set and assignments of nondet to non-constglobals matching the regex if it is set.Other than that, I'm looking for comments on the command line parameters (I've put the function "goals" and the options for the body replacement in separate options for now, but it feels a bit wordy).