Port the last user of static_analysist #6482
Conversation
martin-cs
requested review from
chrisr-diffblue and
peterschrammel
as code owners
|
At this stage I haven't removed cbmc/src/analyses/static_analysis.h Line 16 in 8a720e0 |
no objections |
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
2 times, most recently
from
b8180db to
06e0910
Compare
|
I am seeing unit test failures in https://github.com/diffblue/cbmc/blame/develop/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp which I think are because |
| exprt get_return_lhs(locationt to) const | ||
| { | ||
| // get predecessor of "to" | ||
| to--; |
There was a problem hiding this comment.
I am wondering whether get_return_lhs should have a different interface: decrementing to is an unchecked operation, and would be undefined when to already is the beginning of a container.
There was a problem hiding this comment.
Yes; it is a risky bit of code and far from an ideal design. It is moved over because I was trying to preserve functionality and structure where I could. I should refactor this though.
There was a problem hiding this comment.
I have had a look at this and when doing a "return" edge from END_FUNCTION, decrementing to really is the best way of getting the function call instruction. That is probably a wider API failure. However the only case in which this is actually needed is to handle the return value. So if we are happy return removal has always been done first then it is fine to just remove all of this code.
There was a problem hiding this comment.
I am mildly concerned that some of the more obscure users might not ensure this so I think I will just simplify but preserve the functionality.
| if(to->is_end_function()) | ||
| return static_cast<const exprt &>(get_nil_irep()); |
There was a problem hiding this comment.
Is that really a possible scenario, i.e., can decrementing to result in reaching an END_FUNCTION instruction? If so, is passing a one-past-the-end iterator to get_return_lhs a realistic scenario?
There was a problem hiding this comment.
I really don't think it should be. I think this bit of code is only used in END_FUNCTION where to is the instruction after the call.
|
Memories of this far too foggy to be authoritative, but I think this was added so the security project (RIP) could do value-set-analysis-with-tweaks. |
|
@martin-cs, please adapt the test for use with |
|
@chrisr-diffblue thanks, that does ring a bell... I will assume that changes to this are not going to be high-risk for Diffblue. @peterschrammel Will do, I think the changes should be very minimal. |
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
06e0910 to
d07e6a5
Compare
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
d07e6a5 to
867dd02
Compare
|
A couple of jobs failed because the reference to file has not been removed from the `makefiles. |
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
3 times, most recently
from
f4d7037 to
07d63a5
Compare
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
07d63a5 to
b5666ba
Compare
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
b5666ba to
b517a56
Compare
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
b517a56 to
b6ed850
Compare
The corresponding text function has been public for a long time and there is not reason why the JSON and XML ones can't be as they are const and are called from other public methods.
This is used by the majority of domains and if you don't want to / can't implement make_top() then you probably want a custom make_entry() anyway. This is a net saving of code!
Previously there were no direct checks for this functionality, only for users such as the memory model functionality.
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
b6ed850 to
a1ee415
Compare
|
@peterschrammel @tautschnig : you both reviewed and approved this back in the distant past. I am trying to get it moving again. The PR is essentially identical but with the fix for the issue with the custom value set analysis and removal of static_analysist. These were the outstanding issues from the reviews. If you want another look then do shout, otherwise I will merge it when I can get CI to pass! |
This removes the last in-tree use of static_analysis.{h,cpp}.
It also gives the option of using value_set_domain with the history
options to perform per-path value-set analysis.
shared_ptr's are returned rather than references as it allows the abstract interpreter to synthesise domains at query time, either for unexplored locations or merging multiple traces.
This has been deprecated for many many years and only had one user which was a more obscure feature of goto-instrument. ait is better in almost every direction.
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
a1ee415 to
e0e9bde
Compare
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #6482 +/- ##
===========================================
+ Coverage 78.27% 78.99% +0.72%
===========================================
Files 1699 1696 -3
Lines 195410 195105 -305
===========================================
+ Hits 152953 154123 +1170
+ Misses 42457 40982 -1475
☔ View full report in Codecov by Sentry. |
martin-cs
force-pushed
the
refactor/remove-static-analysis
branch
from
bffd94f to
168901f
Compare
|
I'm going to ignore the patch coverage metric because of the increase of project coverage. |
This ports
value_set_analysis, which was the last user of deprecatedstatic_analysistto useait. Note that this is not the value set analysis code used bycbmc; this one is only used bygoto-instrument(see #6469 ). There are a few supporting changes to theaitinfrastructure which are necessary but technically independent. It is best to review commit by commit. Note that the test case is added before the porting and works both before and after so most of the output is preserved (the afterwards,aitoutput has slightly more as it also outputs the instructions).