Allow instrumentation of loops with "holes" #6808
Conversation
SaswatPadhi
added
enhancement
aws
Codecov Report
@@ Coverage Diff @@
## develop #6808 +/- ##
===========================================
+ Coverage 76.99% 77.00% +0.01%
===========================================
Files 1594 1594
Lines 184263 184345 +82
===========================================
+ Hits 141872 141957 +85
+ Misses 42391 42388 -3
Continue to review full report at Codecov.
|
| if(has_disable_assigns_check_pragma(instruction_it)) | ||
| if( | ||
| has_disable_assigns_check_pragma(instruction_it) || | ||
| (filter && !filter(instruction_it))) |
There was a problem hiding this comment.
See below: I'm not convinced we should permit an empty std::function here.
There was a problem hiding this comment.
Or at least we should make it the default to check all instructions.
There was a problem hiding this comment.
That is the default.
| @@ -541,7 +544,7 @@ exprt instrument_spec_assignst::target_validity_expr( | |||
| // the target's `start_address` pointer satisfies w_ok with the expected size | |||
| // (or is NULL if we allow it explicitly). | |||
| // This assertion will be falsified whenever `start_address` is invalid or | |||
| // not of the right size (or is NULL if we dot not allow it expliclitly). | |||
| // not of the right size (or is NULL if we dot not allow it explicitly). | |||
There was a problem hiding this comment.
Since you're fixing typos - can you also change "dot" to "do" in here?
There was a problem hiding this comment.
Yes sure, will do.
| @@ -449,7 +449,8 @@ class instrument_spec_assignst | |||
| goto_programt::targett instruction_it, | |||
| const goto_programt::targett &instruction_end, | |||
| skip_function_paramst skip_function_params, | |||
| optionalt<cfg_infot> &cfg_info_opt); | |||
| optionalt<cfg_infot> &cfg_info_opt, | |||
| const std::function<bool(const goto_programt::targett &)> &filter = {}); | |||
There was a problem hiding this comment.
I'm not convinced that default-arguments are a good thing here, and also I'm wondering about the semantics: if the function returns true, is the instruction filtered out, or is it only to be included when the filter returns true?
There was a problem hiding this comment.
I'm not convinced that default-arguments are a good thing here
Hmm, what exactly is the issue that you see here? I think default arguments actually very nicely capture the right semantics for a "filter" here:
"if there is a filter and it rejects an instruction, then don't instrument it"
So in the default case when there is no filter, nothing is filtered.
I'm wondering about the semantics: if the function returns
true, is the instruction filtered out, or is it only to be included when the filter returnstrue?
In like 325, I check filter && !filter(instruction_it). So instructions are filtered out only if a filter is provided, and it rejects the instruction. std::function has an operator bool overload that makes this check, IMO, readable and succinct.
There was a problem hiding this comment.
I shall accept the use of a default argument, but I'm afraid you're evading my question when it comes to the semantics: what is the desired result when a filter "rejects the instruction?" You can probably address this concern by changing the name of the parameter to something that a human expects a true/false (or yes/no) response to (such as "skip_instruction" or "should_be_instrumented").
There was a problem hiding this comment.
I don't think I evaded your question. I think explained the desired result. Quoting from my answer again:
"if there is a filter and it rejects an instruction, then don't instrument it"
Are you asking something else?
As to the name of the parameter, sure, I could change it but a "filter" has pretty standard semantics across all languages, okay at least those I know of, e.g. List.filter in OCaml / Haskell, Stream.filter in Java, and even the new views::filter in C++20. They all return the set of things that satisfy the given predicate (and that set of thigs is instrumented in our case).
There was a problem hiding this comment.
If you want to use the filter analogy, isn't what you are expecting the user to provide here the "predicate," and not the "filter" itself?
We are talking about a method that does not have any documentation, so the parameter names are all that a user can go by. RTFS is not an acceptable answer. The parameter you added requires answers to two questions, which the user has to be able to figure out just from the signature of this parameter and its name in the context of the name of the method:
- What are the semantics of this function to be provided?
- [Because of the default argument:] When does a function need to be provided?
It may well be that the right answer is to write documentation instead of trying to come up with a parameter name that is self explanatory, but the current status is not good enough.
There was a problem hiding this comment.
If you want to use the filter analogy, isn't what you are expecting the user to provide here the "predicate," and not the "filter" itself?
The analogy holds because each predicate can only result in a single filter, i.e. one cannot derive two distinct filters from the same predicate.
So, the user gives gives a predicate, which defines the unique filter under discussion.
In any case, I will add some doxygen doc.
What would you like this parameter to be named?
There was a problem hiding this comment.
If you add comments then I won't care all that much about the name, because I expect to be able to construct a suitable function just by reading those comments. Else I'd have gone with needs_instrumentation.
There was a problem hiding this comment.
in other languages you'll find filter(collection, predicate) and filter_not(collection, predicate)
I'd name this pred, and precise that the semantics is that checks are applied when it returns true, and no arguments means "all instruction checked".
There was a problem hiding this comment.
precise that the semantics is that checks are applied when it returns true, and no arguments means "all instruction checked".
Yes, I will specify this in the doc comment.
Thanks for taking a look.
Our assigns clause instrumentation works over a sequence of instructions ignoring control flow edges. In diffblue#6701 a safety check was added to bail out on attempting to instrument loops that contain "holes" -- instructions that appear within the [head, end] sequence for the loop, but are not part of the computed "natural loop" because of control flow. In this PR, we remove this restriction and allow instrumenting such loops by masking out instructions outside of the computed natural loop.
SaswatPadhi
force-pushed
the
loop-holes-fix
branch
from
b85e7dc to
7aa1044
Compare
Our assigns clause instrumentation currently works over a sequence of instructions, ignoring control flow edges.
In #6701 a safety check was added to bail out on attempting to instrument loops that contain "holes" -- instructions that appear within the [head, end] sequence for the loop, but are not part of the computed "natural loop" because of control flow.
In this PR, we remove this restriction and allow instrumenting such loops by masking out instructions outside of the computed natural loop.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).