Merge pull request #7688 from hvitved/dataflow/required-component-stack

Data flow: Restructure `RequiredSummaryComponentStack`
This commit is contained in:
Tom Hvitved
2022-01-24 15:10:08 +01:00
committed by GitHub
5 changed files with 32 additions and 42 deletions

View File

@@ -175,11 +175,11 @@ module Public {
* A class that exists for QL technical reasons only (the IPA type used
* to represent component stacks needs to be bounded).
*/
abstract class RequiredSummaryComponentStack extends SummaryComponentStack {
class RequiredSummaryComponentStack extends Unit {
/**
* Holds if the stack obtained by pushing `head` onto `tail` is required.
*/
abstract predicate required(SummaryComponent c);
abstract predicate required(SummaryComponent head, SummaryComponentStack tail);
}
/** A callable with a flow summary. */
@@ -240,9 +240,9 @@ module Private {
newtype TSummaryComponentStack =
TSingletonSummaryComponentStack(SummaryComponent c) or
TConsSummaryComponentStack(SummaryComponent head, SummaryComponentStack tail) {
tail.(RequiredSummaryComponentStack).required(head)
any(RequiredSummaryComponentStack x).required(head, tail)
or
tail.(RequiredSummaryComponentStack).required(TParameterSummaryComponent(_)) and
any(RequiredSummaryComponentStack x).required(TParameterSummaryComponent(_), tail) and
head = thisParam()
or
derivedFluentFlowPush(_, _, _, head, tail, _)
@@ -890,9 +890,9 @@ module Private {
}
private class MkStack extends RequiredSummaryComponentStack {
MkStack() { interpretSpec(_, _, _, this) }
override predicate required(SummaryComponent c) { interpretSpec(_, _, c, this) }
override predicate required(SummaryComponent head, SummaryComponentStack tail) {
interpretSpec(_, _, head, tail)
}
}
private class SummarizedCallableExternal extends SummarizedCallable {