-
Notifications
You must be signed in to change notification settings - Fork 1.7k
JS: Generate flow summaries from summaryModels; only generate steps as a fallback #19445
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
Changes from all commits
ca5f8b0
0fc1ae2
a44bdf3
16fc8c3
8fab235
891b2b8
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -530,6 +530,93 @@ module Make< | |
} | ||
} | ||
|
||
private predicate isNonLocalSummaryComponent(SummaryComponent c) { | ||
c instanceof TArgumentSummaryComponent or | ||
c instanceof TParameterSummaryComponent or | ||
c instanceof TReturnSummaryComponent | ||
} | ||
|
||
private predicate isLocalSummaryComponent(SummaryComponent c) { | ||
not isNonLocalSummaryComponent(c) | ||
} | ||
|
||
/** | ||
* Holds if `s` is a valid input stack, in the sense that we generate a data flow graph | ||
* that faithfully represents this flow, and lambda-tracking can be expected to track | ||
* lambdas to the relevant callbacks in practice. | ||
*/ | ||
private predicate isSupportedInputStack(SummaryComponentStack s) { | ||
// Argument[n].* | ||
s.length() = 1 and | ||
s.head() instanceof TArgumentSummaryComponent | ||
or | ||
// Argument[n].ReturnValue.* | ||
s.length() = 2 and | ||
s.head() instanceof TReturnSummaryComponent and | ||
s.tail().head() instanceof TArgumentSummaryComponent | ||
or | ||
// Argument[n].Parameter[n].Content.* | ||
s.length() = 3 and | ||
s.head() instanceof TContentSummaryComponent and | ||
s.tail().head() instanceof TParameterSummaryComponent and | ||
s.drop(2).head() instanceof TArgumentSummaryComponent | ||
or | ||
isSupportedInputStack(s.tail()) and | ||
isLocalSummaryComponent(s.head()) | ||
} | ||
|
||
private predicate isSupportedOutputStack1(SummaryComponentStack s) { | ||
// ReturnValue.* | ||
s.length() = 1 and | ||
s.head() instanceof TReturnSummaryComponent | ||
or | ||
// Argument[n].Content.* | ||
s.length() = 2 and | ||
s.head() instanceof TContentSummaryComponent and | ||
s.tail().head() instanceof TArgumentSummaryComponent | ||
Comment on lines
+573
to
+576
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We actually support just There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Good call. I pushed a commit that recognises this, please take a look. |
||
or | ||
// Argument[n].Parameter[n].* | ||
s.length() = 2 and | ||
s.head() instanceof TParameterSummaryComponent and | ||
s.tail().head() instanceof TArgumentSummaryComponent | ||
or | ||
isSupportedOutputStack1(s.tail()) and | ||
isLocalSummaryComponent(s.head()) | ||
} | ||
|
||
/** Like `isSupportedInputStack` but for output stacks. */ | ||
private predicate isSupportedOutputStack(SummaryComponentStack s) { | ||
isSupportedOutputStack1(s) | ||
or | ||
// `Argument[n]` not followed by anything. Needs to be outside the recursion. | ||
s.length() = 1 and | ||
s.head() instanceof TArgumentSummaryComponent | ||
} | ||
|
||
/** | ||
* Holds if `callable` has an unsupported flow `input -> output`. | ||
* | ||
* `whichOne` indicates if the `input` or `output` contains the unsupported sequence. | ||
*/ | ||
predicate unsupportedCallable( | ||
SummarizedCallableImpl callable, SummaryComponentStack input, SummaryComponentStack output, | ||
string whichOne | ||
) { | ||
callable.propagatesFlow(input, output, _, _) and | ||
( | ||
not isSupportedInputStack(input) and whichOne = "input" | ||
or | ||
not isSupportedOutputStack(output) and whichOne = "output" | ||
) | ||
} | ||
|
||
/** | ||
* Holds if `callable` has an unsupported flow. | ||
*/ | ||
predicate unsupportedCallable(SummarizedCallableImpl callable) { | ||
unsupportedCallable(callable, _, _, _) | ||
} | ||
|
||
private predicate summarySpec(string spec) { | ||
exists(SummarizedCallable c | | ||
c.propagatesFlow(spec, _, _, _) | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I hadn't considered the fact that we also support this case, a lambda passed in which has a side-effect on one of it's arguments.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a good thing we do. We rely on this to model the
Promise
constructor in JavaScript.