CONTRACTS: new method to detect static locals for contract instrumentation #6679
Conversation
remi-delmas-3000
added
bugfix
aws
remi-delmas-3000
requested review from
tautschnig,
feliperodri and
SaswatPadhi
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6679 +/- ##
===========================================
+ Coverage 76.82% 76.84% +0.02%
===========================================
Files 1582 1582
Lines 182767 182893 +126
===========================================
+ Hits 140403 140538 +135
+ Misses 42364 42355 -9
Continue to review full report at Codecov.
|
| @@ -22,11 +22,14 @@ Date: January 2022 | |||
| #include <util/simplify_expr.h> | |||
|
|
|||
| #include <analyses/call_graph.h> | |||
There was a problem hiding this comment.
Do you still need this?
|
|
||
| size_t line_to_size_t(const irep_idt &line) | ||
| { | ||
| PRECONDITION(!line.empty()); | ||
| std::stringstream stream(id2string(line)); | ||
| size_t res; | ||
| stream >> res; | ||
| return res; | ||
| } |
There was a problem hiding this comment.
You can (should) use one of the utility functions from util/string2int.{h,cpp} to take care of this for you.
| const goto_programt::const_targett &begin, | ||
| const goto_programt::const_targett &end, | ||
| covered_linest &covered_lines) const | ||
| { | ||
| goto_programt::const_targett it(begin); |
There was a problem hiding this comment.
Perhaps just pass the iterators by value?
| { | ||
| goto_programt::const_targett it(begin); | ||
|
|
||
| while(it != end) |
There was a problem hiding this comment.
I think a for loop might be nicer instead of doing it++ in the body of this while loop?
|
|
||
| const auto &found = functions.function_map.find(fun_id); | ||
|
|
||
| if(found != functions.function_map.end()) |
There was a problem hiding this comment.
This should be an INVARIANT: all functions that are called must exist. They might not have a body, but AFAIK they must exist.
| const auto &loc_fun = sym.location.get_function(); | ||
| if(!loc_fun.empty()) |
There was a problem hiding this comment.
As a second layer of defense: have you also consider evaluating the symbol name to extract a function prefix from it?
| if(itv->second.contains(line)) | ||
| { | ||
| dest.insert(sym.symbol_expr()); | ||
| } | ||
| else if(itv->second.contains(line + 1)) | ||
| { |
There was a problem hiding this comment.
This would deserve some comment to explain why line and line + 1 are relevant.
There was a problem hiding this comment.
I'm going to get rid of this test by other means
| // traverses instructions the given list of instructions, updating the given | ||
| // covered lines map, recursing into function calls. |
There was a problem hiding this comment.
Should that say "in the given list?"
| // When the traversal terminates, the covered_lines map will contain one | ||
| // entry per visited function, with the associated range of lines covered | ||
| // by the traversal. Function names and line numbers are collected from source | ||
| // locations attached to the instructions. |
There was a problem hiding this comment.
I'd suggest to make this a Doxygen comment.
| // included in one of the covered_lines map entries or that is -1 adjacent. | ||
| // if an adjacent entry is found, the coverage is expanded and collection is | ||
| // run again until a fixpoint is reached (this is to collect series of local | ||
| // static declarations that happen at the very begining of a function). |
There was a problem hiding this comment.
I'd suggest to make this a Doxygen comment.
remi-delmas-3000
force-pushed
the
contract-detect-local-statics
branch
11 times, most recently
from
199b724 to
01fb4de
Compare
…ation The previous method relied on building a call graph and could not be used on functions that had already been through an inlining pass. This new method uses source_locations and manages scoping by tracking the min and max source_locations for functions that are encountered when traversing instructions. Then, when collecting statics from the symbol table, we only keep the ones that are found in the traversed functions and whose source_location is within the seen intervals. The method makes the sound pessimistic choice to widen the tracked intervals and collect variables whenever the encountered source_locations are undefined or only partially defined. When replace-call-with-contract is used, extra pragmas are used to track static locals and make sure they are propagated to the write set of the function in which the call is replaced.
remi-delmas-3000
force-pushed
the
contract-detect-local-statics
branch
from
01fb4de to
7f5300e
Compare
The previous method relied on building a call graph and could not be used on functions that had already been through an inlining pass.
Scoping is needed in the case of loop contracts, because we need to detect and havoc only the local statics declared in the loop scope but we should not collect static locals declared outside of the loop's scope.
We first traverses the instructions of a function (or the just the instructions forming a loop in the function), recursing into function calls.
The discovered source locations (function, line, column) are compounded into abstract intervals. We check that every instruction has a
functionattribute. When a column is missing we widen the location to the whole line, when a line is missing we widen the interval is widened to the whole function.In a second pass, we collect symbols from the symbol table for which the source location is included in the intervals discovered in the first pass.
When
--replace-call-with-contractis used to replacegby its contract inf, pragmas are used to markstatic locals of
gin the generated instructions and make sure they are collected propagated automatically to the write set offand any function that usesf, either calling it or by replacing the call by the contract off.This method also works after inlining, because the original source location of an instruction is preserved after inlining. So if
fcallsg, andggets inlined inf, we can still identifygas the contributing function and collectg's locally declared static variables from the symbol table.