Skip to content

Ruby: Fix spurious flow through reverse stores #10574

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

Merged
merged 4 commits into from
Sep 28, 2022

Conversation

hvitved
Copy link
Contributor

@hvitved hvitved commented Sep 26, 2022

Commit-by-commit review is encouraged.

In Ruby, reads with known indices, such as

a[0]

give rise to two read steps; one that reads TSingletonContent(TKnownElementContent(0)) and one that reads TSingletonContent(TUnknownElementContent()) (if data is stored at an unknown index, it might be 0).

Since [] is just a method call, it means we have two flow summaries for []:

Argument[self].Argument[0] -> ReturnValue
Argument[self].Argument[?] -> ReturnValue

This works well for reads, however for reverse stores

a[0][1] = x

it means that we will get store steps into a with both TSingletonContent(TKnownElementContent(0)) and TSingletonContent(TUnknownElementContent()), which allows for spurious flow:

a[0][1] = x
sink(a[2][1]) # spurious flow

The solution in this PR is to add a new ContentSet branch

TKnownOrUnknownElementContent(Content::KnownElementContent c)

which can read from both TKnownElementContent(c) and TUnknownElementContent(), but which can only store into TKnownElementContent(c). We can then reduce a[0] to just a single read step, which reads from TKnownOrUnknownElementContent(TKnownElementContent(0)).

In order to distinguish TKnownOrUnknownElementContent(c) from TSingletonContent(TKnownElementContent(c)) in models-as-data specifications, we use the following syntax

MaD syntax ContentSet
Element[0] TKnownOrUnknownElementContent(0)
Element[0!] TSingletonContent(TKnownElementContent(0))

and similarly for With(out)Element and ranges Element[0..]. This means that the flow summary for [] is just a single row:

Argument[self].Argument[0] -> ReturnValue

Note also that using Element[0] vs Element[0!] in output specifications makes no differences, since the former also stores only into TSingletonContent(TKnownElementContent(0)).

@github-actions github-actions bot added the Ruby label Sep 26, 2022
@hvitved hvitved force-pushed the ruby/reverse-known-stores branch from 34fb0d3 to 31806b8 Compare September 27, 2022 18:16
@hvitved hvitved marked this pull request as ready for review September 28, 2022 07:35
@hvitved hvitved requested a review from a team as a code owner September 28, 2022 07:35
@hvitved hvitved added the no-change-note-required This PR does not need a change note label Sep 28, 2022
Copy link
Contributor

@asgerf asgerf left a comment

Choose a reason for hiding this comment

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

LGTM. This conflicts with #10375 but it's probably easier for me to update my PR than the other way around, so feel free to merge first.

@hvitved
Copy link
Contributor Author

hvitved commented Sep 28, 2022

This conflicts with #10375 but it's probably easier for me to update my PR than the other way around, so feel free to merge first.

Thanks. Sorry for introducing yet another merge conflict on your PR.

@hvitved hvitved merged commit 22946b1 into github:main Sep 28, 2022
asgerf added a commit to asgerf/codeql that referenced this pull request Sep 28, 2022
This only fixes superficial conflicts with
  github#10574
semantic conflicts will be addressed in later commits
@hvitved hvitved deleted the ruby/reverse-known-stores branch September 29, 2022 08:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation no-change-note-required This PR does not need a change note Ruby
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants