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.

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

C#/Java: Content based model generation improvements. #17363

Merged
merged 10 commits into from
Sep 19, 2024

Conversation

michaelnebel
Copy link
Contributor

@michaelnebel michaelnebel commented Sep 3, 2024

If we apply the content based model generator to

  • The Java SDK we get around 80k models.
  • The .NET 8 Runtime we get around 500k models.

Many of these models are undesirable, primarily because of one of the following reasons

  1. Due to the lack of type constraints, we get lots of models as "data" could have originated from lots of different implementations (and conversely for stores).
  2. A model reads from a synthetic field that no other model writes to (and conversely).

With the changes proposed in this PR, applying the content based model generator to

  • The Java SDK we get around 4k models.
  • The .NET 8 Runtime we get around 5k models.

The issues are addressed in the following way:

  1. We make a rough filtering on the APIs: Content based model generation is only considered for an API if the formula below holds for that particular API (the reasoning behind this is also listed as a code comment and the magic numbers 2 and 3 in the formula below are definitely up for debate. If another approach should be taken - e.g. maybe something like filtering APIs based on input and return types then we can discuss this as well). Applying this constraint to the target APIs from the Java SDK removes approximately 2% og the possible target APIs for summary generation, which indicates that this is not an especially invasive constraint.
    • # summaries <= 2 * #number of parameters + 3
  2. We only include a summary for an API that reads or stores into a synthetic field, if there exists a "chain" of APIs with summaries such that data originates from non-synthetic content and targets non-synthetic content. The canonical example for this are get and set methods that uses a private backing field X. In this case we would like to generate the summaries set : Argument[0] -> Argument[this].SyntheticField[X] and get : Argument[this].SyntheticField[X] -> ReturnValue, but we only want to do this in case both methods exists. If only the get method exists, then it retrieves information from a "dead" synthetic field. The synthetic chaining is currently based on access path equality but that restriction could potentially be loosened a bit, but I suspect that this only has limited impact on the generated summaries.

Note that the changes in this PR doesn't change the production version of the model generation and only impacts model generated by the recently introduced --with-contentbased-summaries.
Further changes are still required for this to be production ready, but the changes in this PR are self contained.

@michaelnebel michaelnebel force-pushed the modelgen/fieldbasedimprovements branch from 76b9cdd to 8473b8c Compare September 5, 2024 11:14
@michaelnebel michaelnebel force-pushed the modelgen/fieldbasedimprovements branch from 8473b8c to 412551f Compare September 6, 2024 09:44
@michaelnebel michaelnebel force-pushed the modelgen/fieldbasedimprovements branch 3 times, most recently from b5456a3 to b7d00a4 Compare September 9, 2024 11:11
@michaelnebel michaelnebel force-pushed the modelgen/fieldbasedimprovements branch 4 times, most recently from 4521dfd to 30f3923 Compare September 10, 2024 09:38
@michaelnebel michaelnebel force-pushed the modelgen/fieldbasedimprovements branch from 30f3923 to 0abc08c Compare September 10, 2024 13:26
@michaelnebel michaelnebel added the no-change-note-required This PR does not need a change note label Sep 10, 2024
@michaelnebel michaelnebel marked this pull request as ready for review September 10, 2024 14:16
@michaelnebel michaelnebel requested review from a team as code owners September 10, 2024 14:16
@michaelnebel
Copy link
Contributor Author

DCA looks good!

Copy link
Contributor

@hvitved hvitved left a comment

Choose a reason for hiding this comment

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

Some initial comments.

* detection instead, as reads and stores would use a significant
* part of an objects internal state.
*/
private class ContentDataFlowSummaryTargetApi extends DataFlowSummaryTargetApi {
Copy link
Contributor

Choose a reason for hiding this comment

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

Alternatively, we could make the restriction per parameter. I.e., if a method has only one summary for Argument[0] then include it, but if it has more than, say 3, summaries for Argument[1] then exclude those.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, that could also be interesting.
Would it be acceptable if I do that experiment as a follow up?
As it is now we "only" exclude approximately 2% of all the possible target APIs with this limitation.

Copy link
Contributor

Choose a reason for hiding this comment

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

Yes!

hasSyntheticContent(read) and
hasSyntheticContent(store) and
(
step(t1, read, t2, store)
Copy link
Contributor

Choose a reason for hiding this comment

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

Shouldn't we restrict to syntPathEntry here? Otherwise it looks like we will compute O(n^2) paths.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Uh - this was intended as a helper predicate, but it looks like we need to fold it into the declarations where it is used to avoid the O(n^2).

* if both of these methods exist.
*/
pragma[nomagic]
predicate acceptReadStore(
Copy link
Contributor

Choose a reason for hiding this comment

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

I wonder if it is simply enough to say that we will include a synthetic field if it is part of some input specification and part of some output specification. That should also handle cases such as

setAll // input: Argument[0], output: ReturnValue.SyntheticField[Foo].Element
get // input: Argument[0].SyntheticField[Foo], output: ReturnValue

list = setAll("taint");
x = list[0];
sink(get(x));

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I also thought about that as a possible "improvement" (instead of using "path" equality we could "hash" paths with synthetics (basically just print the synthetics in the order they are shown in the path and then compare that)). This would allow path continuations as the one you mention there.
Is it acceptable that we attempt this as a follow up?

Copy link
Contributor

Choose a reason for hiding this comment

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

I was actually thinking of something even simpler where the order is not taken into account, but yes follow-up is fine.

Copy link
Contributor Author

@michaelnebel michaelnebel Sep 19, 2024

Choose a reason for hiding this comment

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

We could also try without order; However, I am quite sure that we need the "chaining" logic. It turned out that it is not uncommen that we produce summaries like SyntheticField[A] -> SyntheticField[A] (without other mentions on the synthetic field A) or SyntheticField[A] -> SyntheticField[B] and SyntheticField[B] -> SyntheticField[A], if we don't restrict the use of synthetics.

* be translated into a synthetic field.
*
* This is needed because we don't want to include summaries that reads from or
* stores into a "dead" synthetic field.
Copy link
Contributor

Choose a reason for hiding this comment

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

"internal" instead of "dead"?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Sure! I will add a commit to the re-factor PR that changes this.

@michaelnebel michaelnebel merged commit 4a9e3ee into github:main Sep 19, 2024
52 checks passed
@michaelnebel michaelnebel deleted the modelgen/fieldbasedimprovements branch September 19, 2024 08:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants