Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Remove duplicate ctx-derived arguments in base analysis #1308

Merged
merged 50 commits into from
Jan 24, 2024
Merged

Remove duplicate ctx-derived arguments in base analysis #1308

merged 50 commits into from
Jan 24, 2024

Conversation

karoliineh
Copy link
Member

@karoliineh karoliineh commented Dec 27, 2023 •
edited by sim642
Loading

Solves #1266

TODO

  • reachable_from_value
  • reachable_from_address
  • reachable_vars
  • Before and after sv-benchmarks run. @sim642

@karoliineh
Remove gs from set signature in base
a568620
@karoliineh
Remove gs from set_many signature in base
fcb52df
@karoliineh
Remove gs from invalidate signature in base
ae56428
@karoliineh
Remove gs from special_unknown_invalidate signature in base
9d13dd1
@karoliineh
Remove ask from set signature in base
55bc2d6
@karoliineh
Remove ask from set_many signature in base
c740996
@karoliineh
Remove ask from invalidate signature
05abd0d
@karoliineh
Remove ask from special_unknown_invalidate signature
5c27f2b
@karoliineh
Remove unneccessary parentheses and rename a -> ask
1575f7e
@karoliineh
Remove st from special_unknown_invalidate signature
16c9a8b
@karoliineh
Add ctx to almost everywhere in base
8187ac9
@karoliineh
Remove ask and gs from eval_rv signature
d4ef5c0
@karoliineh
Remove st from eval_rv signature
77c6f20
@karoliineh
Remove ask, gs and st from eval_rv_address signature
c0c8de3
@karoliineh
Remove ask, gs and st from eval_rv_back_up signature
7ae6bdd
@karoliineh
Remove ask, gs and st from eval_lv signature
7b6005e
@karoliineh
Remove ask, gs and st from convert_offset signature
b11d327
@karoliineh
Remove unused parameter st from evalbinop_base signature
5f18ee7
@karoliineh
Remove ask, gs and st from evalbinop signature
292bd8d
@karoliineh
Remove ask, gs and st from eval_fv, eval_tv and eval_int signatures
4bd1493
@karoliineh
Remove unused parameters ask and gs from set_savetop signature
ac2839a
@karoliineh
Repetitive usages of (Analyses.ask_of_ctx ctx) to one variable
f68cfa7
@karoliineh
Remove ask, gs and st from collect_funargs and collect_invalidate sig…
dd1b753 
…natures
@karoliineh karoliineh added the cleanup Refactoring, clean-up label Dec 27, 2023
@sim642 sim642 linked an issue Dec 27, 2023 that may be closed by this pull request
Remove duplicate ctx-derived arguments in base analysis #1266
Open
@sim642 sim642 added this to the v2.4.0 milestone Dec 27, 2023
@karoliineh
Copy link
Member Author

Although the regression tests did pass with the st argument removed, it is not clear how it affects the refinement. Thus, as it is not a priority right now, I have just put the st argument back everywhere. However, the cleanup from replacing the ask and gs arguments with ctx is still significant enough.

I have still removed the st argument from functions that did not even use it (e.g. evalbinop_base and reachable_from_value), and the functions that just passed the argument st to the functions that did not use it.

@karoliineh karoliineh requested a review from sim642 January 5, 2024 12:15
michael-schwarz
michael-schwarz reviewed Jan 5, 2024
View reviewed changes
src/analyses/base.ml Outdated
Comment on lines 1879 to 1880
let immediately_reachable = reachable_from_value ~ctx (eval_rv ~ctx st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in
reachable_vars ~ctx [immediately_reachable]
Copy link
Member

@michael-schwarz michael-schwarz Jan 5, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I quite get why this is guaranteed to be the same? To me, it looks like we are evaluating some things on st (eval_rv) and others on ctx.local (reachable_vars)?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR currently leaves st as separate from ctx.local because of this, but there's a broader conceptual problem with it even before this PR.
Namely, even if a different st is passed and used for some local lookups, ask isn't (and cannot be) modified, so EvalInt query would still run on the original local state. So having a separate local state is overall questionable and should maybe be addressed separately in the future somehow.

sim642
sim642 reviewed Jan 9, 2024
View reviewed changes
src/analyses/base.ml Outdated Show resolved Hide resolved
@sim642 sim642 self-assigned this Jan 9, 2024
sim642
sim642 approved these changes Jan 11, 2024
View reviewed changes
Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verdicts and performance on sv-benchmarks are essentially unchanged, which is good.

@sim642 sim642 removed their assignment Jan 22, 2024
@sim642 sim642 merged commit 71e21b2 into master Jan 24, 2024
16 of 17 checks passed
@sim642 sim642 deleted the issue-1266 branch January 24, 2024 11:04
@sim642 sim642 mentioned this pull request Jan 24, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@michael-schwarz michael-schwarz michael-schwarz approved these changes

@sim642 sim642 sim642 approved these changes

Assignees
No one assigned
Labels
cleanup Refactoring, clean-up
Projects
None yet
Milestone
v2.4.0
Development

Successfully merging this pull request may close these issues.

Remove duplicate ctx-derived arguments in base analysis
3 participants
@karoliineh @sim642 @michael-schwarz