This commit is contained in:
Asger Feldthaus 2022-02-10 13:08:40 +01:00
Родитель b51b6069fc
Коммит f66cad85be
2 изменённых файлов: 211 добавлений и 118 удалений

Просмотреть файл

@ -26,9 +26,13 @@ module Public {
string toString() {
exists(Content c | this = TContentSummaryComponent(c) and result = c.toString())
or
exists(int i | this = TParameterSummaryComponent(i) and result = "parameter " + i)
exists(ArgumentPosition pos |
this = TParameterSummaryComponent(pos) and result = "parameter " + pos
)
or
exists(int i | this = TArgumentSummaryComponent(i) and result = "argument " + i)
exists(ParameterPosition pos |
this = TArgumentSummaryComponent(pos) and result = "argument " + pos
)
or
exists(ReturnKind rk | this = TReturnSummaryComponent(rk) and result = "return (" + rk + ")")
}
@ -39,11 +43,11 @@ module Public {
/** Gets a summary component for content `c`. */
SummaryComponent content(Content c) { result = TContentSummaryComponent(c) }
/** Gets a summary component for parameter `i`. */
SummaryComponent parameter(int i) { result = TParameterSummaryComponent(i) }
/** Gets a summary component for a parameter at position `pos`. */
SummaryComponent parameter(ArgumentPosition pos) { result = TParameterSummaryComponent(pos) }
/** Gets a summary component for argument `i`. */
SummaryComponent argument(int i) { result = TArgumentSummaryComponent(i) }
/** Gets a summary component for an argument at position `pos`. */
SummaryComponent argument(ParameterPosition pos) { result = TArgumentSummaryComponent(pos) }
/** Gets a summary component for a return of kind `rk`. */
SummaryComponent return(ReturnKind rk) { result = TReturnSummaryComponent(rk) }
@ -86,7 +90,9 @@ module Public {
predicate contains(SummaryComponent c) { c = this.drop(_).head() }
/** Gets the bottom element of this stack. */
SummaryComponent bottom() { result = this.drop(this.length() - 1).head() }
SummaryComponent bottom() {
this = TSingletonSummaryComponentStack(result) or result = this.tail().bottom()
}
/** Gets a textual representation of this stack. */
string toString() {
@ -120,8 +126,10 @@ module Public {
result = TConsSummaryComponentStack(head, tail)
}
/** Gets a singleton stack for argument `i`. */
SummaryComponentStack argument(int i) { result = singleton(SummaryComponent::argument(i)) }
/** Gets a singleton stack for an argument at position `pos`. */
SummaryComponentStack argument(ParameterPosition pos) {
result = singleton(SummaryComponent::argument(pos))
}
/** Gets a singleton stack representing a return of kind `rk`. */
SummaryComponentStack return(ReturnKind rk) { result = singleton(SummaryComponent::return(rk)) }
@ -137,9 +145,15 @@ module Public {
or
noComponentSpecificCsv(sc) and
(
exists(int i | sc = TParameterSummaryComponent(i) and result = "Parameter[" + i + "]")
exists(ArgumentPosition pos |
sc = TParameterSummaryComponent(pos) and
result = "Parameter[" + getArgumentPositionCsv(pos) + "]"
)
or
exists(int i | sc = TArgumentSummaryComponent(i) and result = "Argument[" + i + "]")
exists(ParameterPosition pos |
sc = TArgumentSummaryComponent(pos) and
result = "Argument[" + getParameterPositionCsv(pos) + "]"
)
or
sc = TReturnSummaryComponent(getReturnValueKind()) and result = "ReturnValue"
)
@ -163,11 +177,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. */
@ -201,10 +215,10 @@ module Public {
/**
* Holds if values stored inside `content` are cleared on objects passed as
* the `i`th argument to this callable.
* arguments at position `pos` to this callable.
*/
pragma[nomagic]
predicate clearsContent(int i, Content content) { none() }
predicate clearsContent(ParameterPosition pos, Content content) { none() }
}
}
@ -217,20 +231,20 @@ module Private {
newtype TSummaryComponent =
TContentSummaryComponent(Content c) or
TParameterSummaryComponent(int i) { parameterPosition(i) } or
TArgumentSummaryComponent(int i) { parameterPosition(i) } or
TParameterSummaryComponent(ArgumentPosition pos) or
TArgumentSummaryComponent(ParameterPosition pos) or
TReturnSummaryComponent(ReturnKind rk)
private TSummaryComponent thisParam() {
private TParameterSummaryComponent thisParam() {
result = TParameterSummaryComponent(instanceParameterPosition())
}
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, _)
@ -285,9 +299,9 @@ module Private {
/**
* Holds if `c` has a flow summary from `input` to `arg`, where `arg`
* writes to (contents of) the `i`th argument, and `c` has a
* value-preserving flow summary from the `i`th argument to a return value
* (`return`).
* writes to (contents of) arguments at position `pos`, and `c` has a
* value-preserving flow summary from the arguments at position `pos`
* to a return value (`return`).
*
* In such a case, we derive flow from `input` to (contents of) the return
* value.
@ -302,10 +316,10 @@ module Private {
SummarizedCallable c, SummaryComponentStack input, SummaryComponentStack arg,
SummaryComponentStack return, boolean preservesValue
) {
exists(int i |
exists(ParameterPosition pos |
summary(c, input, arg, preservesValue) and
isContentOfArgument(arg, i) and
summary(c, SummaryComponentStack::singleton(TArgumentSummaryComponent(i)), return, true) and
isContentOfArgument(arg, pos) and
summary(c, SummaryComponentStack::argument(pos), return, true) and
return.bottom() = TReturnSummaryComponent(_)
)
}
@ -330,10 +344,10 @@ module Private {
s.head() = TParameterSummaryComponent(_) and exists(s.tail())
}
private predicate isContentOfArgument(SummaryComponentStack s, int i) {
s.head() = TContentSummaryComponent(_) and isContentOfArgument(s.tail(), i)
private predicate isContentOfArgument(SummaryComponentStack s, ParameterPosition pos) {
s.head() = TContentSummaryComponent(_) and isContentOfArgument(s.tail(), pos)
or
s = TSingletonSummaryComponentStack(TArgumentSummaryComponent(i))
s = SummaryComponentStack::argument(pos)
}
private predicate outputState(SummarizedCallable c, SummaryComponentStack s) {
@ -364,8 +378,8 @@ module Private {
private newtype TSummaryNodeState =
TSummaryNodeInputState(SummaryComponentStack s) { inputState(_, s) } or
TSummaryNodeOutputState(SummaryComponentStack s) { outputState(_, s) } or
TSummaryNodeClearsContentState(int i, boolean post) {
any(SummarizedCallable sc).clearsContent(i, _) and post in [false, true]
TSummaryNodeClearsContentState(ParameterPosition pos, boolean post) {
any(SummarizedCallable sc).clearsContent(pos, _) and post in [false, true]
}
/**
@ -414,21 +428,23 @@ module Private {
result = "to write: " + s
)
or
exists(int i, boolean post, string postStr |
this = TSummaryNodeClearsContentState(i, post) and
exists(ParameterPosition pos, boolean post, string postStr |
this = TSummaryNodeClearsContentState(pos, post) and
(if post = true then postStr = " (post)" else postStr = "") and
result = "clear: " + i + postStr
result = "clear: " + pos + postStr
)
}
}
/**
* Holds if `state` represents having read the `i`th argument for `c`. In this case
* we are not synthesizing a data-flow node, but instead assume that a relevant
* parameter node already exists.
* Holds if `state` represents having read from a parameter at position
* `pos` in `c`. In this case we are not synthesizing a data-flow node,
* but instead assume that a relevant parameter node already exists.
*/
private predicate parameterReadState(SummarizedCallable c, SummaryNodeState state, int i) {
state.isInputState(c, SummaryComponentStack::argument(i))
private predicate parameterReadState(
SummarizedCallable c, SummaryNodeState state, ParameterPosition pos
) {
state.isInputState(c, SummaryComponentStack::argument(pos))
}
/**
@ -441,9 +457,9 @@ module Private {
or
state.isOutputState(c, _)
or
exists(int i |
c.clearsContent(i, _) and
state = TSummaryNodeClearsContentState(i, _)
exists(ParameterPosition pos |
c.clearsContent(pos, _) and
state = TSummaryNodeClearsContentState(pos, _)
)
}
@ -452,9 +468,9 @@ module Private {
exists(SummaryNodeState state | state.isInputState(c, s) |
result = summaryNode(c, state)
or
exists(int i |
parameterReadState(c, state, i) and
result.(ParamNode).isParameterOf(c, i)
exists(ParameterPosition pos |
parameterReadState(c, state, pos) and
result.(ParamNode).isParameterOf(c, pos)
)
)
}
@ -468,20 +484,20 @@ module Private {
}
/**
* Holds if a write targets `post`, which is a post-update node for the `i`th
* parameter of `c`.
* Holds if a write targets `post`, which is a post-update node for a
* parameter at position `pos` in `c`.
*/
private predicate isParameterPostUpdate(Node post, SummarizedCallable c, int i) {
post = summaryNodeOutputState(c, SummaryComponentStack::argument(i))
private predicate isParameterPostUpdate(Node post, SummarizedCallable c, ParameterPosition pos) {
post = summaryNodeOutputState(c, SummaryComponentStack::argument(pos))
}
/** Holds if a parameter node is required for the `i`th parameter of `c`. */
predicate summaryParameterNodeRange(SummarizedCallable c, int i) {
parameterReadState(c, _, i)
/** Holds if a parameter node at position `pos` is required for `c`. */
predicate summaryParameterNodeRange(SummarizedCallable c, ParameterPosition pos) {
parameterReadState(c, _, pos)
or
isParameterPostUpdate(_, c, i)
isParameterPostUpdate(_, c, pos)
or
c.clearsContent(i, _)
c.clearsContent(pos, _)
}
private predicate callbackOutput(
@ -493,10 +509,10 @@ module Private {
}
private predicate callbackInput(
SummarizedCallable c, SummaryComponentStack s, Node receiver, int i
SummarizedCallable c, SummaryComponentStack s, Node receiver, ArgumentPosition pos
) {
any(SummaryNodeState state).isOutputState(c, s) and
s.head() = TParameterSummaryComponent(i) and
s.head() = TParameterSummaryComponent(pos) and
receiver = summaryNodeInputState(c, s.drop(1))
}
@ -547,17 +563,17 @@ module Private {
result = getReturnType(c, rk)
)
or
exists(int i | head = TParameterSummaryComponent(i) |
exists(ArgumentPosition pos | head = TParameterSummaryComponent(pos) |
result =
getCallbackParameterType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
s.drop(1))), i)
s.drop(1))), pos)
)
)
)
or
exists(SummarizedCallable c, int i, ParamNode p |
n = summaryNode(c, TSummaryNodeClearsContentState(i, false)) and
p.isParameterOf(c, i) and
exists(SummarizedCallable c, ParameterPosition pos, ParamNode p |
n = summaryNode(c, TSummaryNodeClearsContentState(pos, false)) and
p.isParameterOf(c, pos) and
result = getNodeType(p)
)
}
@ -571,10 +587,10 @@ module Private {
)
}
/** Holds if summary node `arg` is the `i`th argument of call `c`. */
predicate summaryArgumentNode(DataFlowCall c, Node arg, int i) {
/** Holds if summary node `arg` is at position `pos` in the call `c`. */
predicate summaryArgumentNode(DataFlowCall c, Node arg, ArgumentPosition pos) {
exists(SummarizedCallable callable, SummaryComponentStack s, Node receiver |
callbackInput(callable, s, receiver, i) and
callbackInput(callable, s, receiver, pos) and
arg = summaryNodeOutputState(callable, s) and
c = summaryDataFlowCall(receiver)
)
@ -582,12 +598,12 @@ module Private {
/** Holds if summary node `post` is a post-update node with pre-update node `pre`. */
predicate summaryPostUpdateNode(Node post, Node pre) {
exists(SummarizedCallable c, int i |
isParameterPostUpdate(post, c, i) and
pre.(ParamNode).isParameterOf(c, i)
exists(SummarizedCallable c, ParameterPosition pos |
isParameterPostUpdate(post, c, pos) and
pre.(ParamNode).isParameterOf(c, pos)
or
pre = summaryNode(c, TSummaryNodeClearsContentState(i, false)) and
post = summaryNode(c, TSummaryNodeClearsContentState(i, true))
pre = summaryNode(c, TSummaryNodeClearsContentState(pos, false)) and
post = summaryNode(c, TSummaryNodeClearsContentState(pos, true))
)
or
exists(SummarizedCallable callable, SummaryComponentStack s |
@ -610,13 +626,13 @@ module Private {
* node, and back out to `p`.
*/
predicate summaryAllowParameterReturnInSelf(ParamNode p) {
exists(SummarizedCallable c, int i | p.isParameterOf(c, i) |
c.clearsContent(i, _)
exists(SummarizedCallable c, ParameterPosition ppos | p.isParameterOf(c, ppos) |
c.clearsContent(ppos, _)
or
exists(SummaryComponentStack inputContents, SummaryComponentStack outputContents |
summary(c, inputContents, outputContents, _) and
inputContents.bottom() = pragma[only_bind_into](TArgumentSummaryComponent(i)) and
outputContents.bottom() = pragma[only_bind_into](TArgumentSummaryComponent(i))
inputContents.bottom() = pragma[only_bind_into](TArgumentSummaryComponent(ppos)) and
outputContents.bottom() = pragma[only_bind_into](TArgumentSummaryComponent(ppos))
)
)
}
@ -641,9 +657,9 @@ module Private {
preservesValue = false and not summary(c, inputContents, outputContents, true)
)
or
exists(SummarizedCallable c, int i |
pred.(ParamNode).isParameterOf(c, i) and
succ = summaryNode(c, TSummaryNodeClearsContentState(i, _)) and
exists(SummarizedCallable c, ParameterPosition pos |
pred.(ParamNode).isParameterOf(c, pos) and
succ = summaryNode(c, TSummaryNodeClearsContentState(pos, _)) and
preservesValue = true
)
}
@ -692,12 +708,20 @@ module Private {
* node where field `b` is cleared).
*/
predicate summaryClearsContent(Node n, Content c) {
exists(SummarizedCallable sc, int i |
n = summaryNode(sc, TSummaryNodeClearsContentState(i, true)) and
sc.clearsContent(i, c)
exists(SummarizedCallable sc, ParameterPosition pos |
n = summaryNode(sc, TSummaryNodeClearsContentState(pos, true)) and
sc.clearsContent(pos, c)
)
}
pragma[noinline]
private predicate viableParam(
DataFlowCall call, SummarizedCallable sc, ParameterPosition ppos, ParamNode p
) {
p.isParameterOf(sc, ppos) and
sc = viableCallable(call)
}
/**
* Holds if values stored inside content `c` are cleared inside a
* callable to which `arg` is an argument.
@ -706,18 +730,25 @@ module Private {
* `arg` (see comment for `summaryClearsContent`).
*/
predicate summaryClearsContentArg(ArgNode arg, Content c) {
exists(DataFlowCall call, int i |
viableCallable(call).(SummarizedCallable).clearsContent(i, c) and
arg.argumentOf(call, i)
exists(DataFlowCall call, SummarizedCallable sc, ParameterPosition ppos |
argumentPositionMatch(call, arg, ppos) and
viableParam(call, sc, ppos, _) and
sc.clearsContent(ppos, c)
)
}
pragma[nomagic]
private ParamNode summaryArgParam0(DataFlowCall call, ArgNode arg) {
exists(ParameterPosition ppos, SummarizedCallable sc |
argumentPositionMatch(call, arg, ppos) and
viableParam(call, sc, ppos, result)
)
}
pragma[nomagic]
private ParamNode summaryArgParam(ArgNode arg, ReturnKindExt rk, OutNodeExt out) {
exists(DataFlowCall call, int pos, SummarizedCallable callable |
arg.argumentOf(call, pos) and
viableCallable(call) = callable and
result.isParameterOf(callable, pos) and
exists(DataFlowCall call |
result = summaryArgParam0(call, arg) and
out = rk.getAnOutNode(call)
)
}
@ -795,39 +826,33 @@ module Private {
}
/** Holds if specification component `c` parses as parameter `n`. */
predicate parseParam(string c, int n) {
predicate parseParam(string c, ArgumentPosition pos) {
specSplit(_, c, _) and
(
c.regexpCapture("Parameter\\[([-0-9]+)\\]", 1).toInt() = n
or
exists(int n1, int n2 |
c.regexpCapture("Parameter\\[([-0-9]+)\\.\\.([0-9]+)\\]", 1).toInt() = n1 and
c.regexpCapture("Parameter\\[([-0-9]+)\\.\\.([0-9]+)\\]", 2).toInt() = n2 and
n = [n1 .. n2]
)
exists(string body |
body = c.regexpCapture("Parameter\\[([^\\]]*)\\]", 1) and
pos = parseParamBody(body)
)
}
/** Holds if specification component `c` parses as argument `n`. */
predicate parseArg(string c, int n) {
predicate parseArg(string c, ParameterPosition pos) {
specSplit(_, c, _) and
(
c.regexpCapture("Argument\\[([-0-9]+)\\]", 1).toInt() = n
or
exists(int n1, int n2 |
c.regexpCapture("Argument\\[([-0-9]+)\\.\\.([0-9]+)\\]", 1).toInt() = n1 and
c.regexpCapture("Argument\\[([-0-9]+)\\.\\.([0-9]+)\\]", 2).toInt() = n2 and
n = [n1 .. n2]
)
exists(string body |
body = c.regexpCapture("Argument\\[([^\\]]*)\\]", 1) and
pos = parseArgBody(body)
)
}
private SummaryComponent interpretComponent(string c) {
specSplit(_, c, _) and
(
exists(int pos | parseArg(c, pos) and result = SummaryComponent::argument(pos))
exists(ParameterPosition pos |
parseArg(c, pos) and result = SummaryComponent::argument(pos)
)
or
exists(int pos | parseParam(c, pos) and result = SummaryComponent::parameter(pos))
exists(ArgumentPosition pos |
parseParam(c, pos) and result = SummaryComponent::parameter(pos)
)
or
c = "ReturnValue" and result = SummaryComponent::return(getReturnValueKind())
or
@ -867,9 +892,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 {
@ -897,11 +922,13 @@ module Private {
}
private predicate inputNeedsReference(string c) {
c = "Argument" or
parseArg(c, _) or
inputNeedsReferenceSpecific(c)
}
private predicate outputNeedsReference(string c) {
c = "Argument" or
parseArg(c, _) or
c = "ReturnValue" or
outputNeedsReferenceSpecific(c)
@ -934,14 +961,18 @@ module Private {
interpretOutput(output, idx + 1, ref, mid) and
specSplit(output, c, idx)
|
exists(int pos |
node.asNode().(PostUpdateNode).getPreUpdateNode().(ArgNode).argumentOf(mid.asCall(), pos)
exists(ArgumentPosition apos, ParameterPosition ppos |
node.asNode().(PostUpdateNode).getPreUpdateNode().(ArgNode).argumentOf(mid.asCall(), apos) and
parameterMatch(ppos, apos)
|
parseArg(c, pos)
c = "Argument" or parseArg(c, ppos)
)
or
exists(int pos | node.asNode().(ParamNode).isParameterOf(mid.asCallable(), pos) |
c = "Parameter" or parseParam(c, pos)
exists(ArgumentPosition apos, ParameterPosition ppos |
node.asNode().(ParamNode).isParameterOf(mid.asCallable(), ppos) and
parameterMatch(ppos, apos)
|
c = "Parameter" or parseParam(c, apos)
)
or
c = "ReturnValue" and
@ -960,7 +991,12 @@ module Private {
interpretInput(input, idx + 1, ref, mid) and
specSplit(input, c, idx)
|
exists(int pos | node.asNode().(ArgNode).argumentOf(mid.asCall(), pos) | parseArg(c, pos))
exists(ArgumentPosition apos, ParameterPosition ppos |
node.asNode().(ArgNode).argumentOf(mid.asCall(), apos) and
parameterMatch(ppos, apos)
|
c = "Argument" or parseArg(c, ppos)
)
or
exists(ReturnNodeExt ret |
c = "ReturnValue" and
@ -1115,9 +1151,9 @@ module Private {
b.asCall() = summaryDataFlowCall(a.asNode()) and
value = "receiver"
or
exists(int i |
summaryArgumentNode(b.asCall(), a.asNode(), i) and
value = "argument (" + i + ")"
exists(ArgumentPosition pos |
summaryArgumentNode(b.asCall(), a.asNode(), pos) and
value = "argument (" + pos + ")"
)
}

Просмотреть файл

@ -22,6 +22,42 @@ predicate parameterPosition(int i) {
/** Gets the parameter position of the instance parameter. */
int instanceParameterPosition() { result = -1 }
/** A parameter position represented by an integer. */
class ParameterPosition extends int {
ParameterPosition() {
parameterPosition(this)
}
}
/** An argument position represented by an integer. */
class ArgumentPosition extends int {
ArgumentPosition() {
parameterPosition(this)
}
}
/** Holds if arguments at position `apos` match parameters at position `ppos`. */
pragma[inline]
predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos) { ppos = apos }
/**
* Holds if `arg` is an argument of `call` with an argument position that matches
* parameter position `ppos`.
*/
pragma[noinline]
predicate argumentPositionMatch(DataFlowCall call, ArgNode arg, ParameterPosition ppos) {
exists(ArgumentPosition apos |
arg.argumentOf(call, apos) and
parameterMatch(ppos, apos)
)
}
/** Gets the textual representation of a parameter position in the format used for flow summaries. */
string getParameterPositionCsv(ParameterPosition pos) { result = pos.toString() }
/** Gets the textual representation of an argument position in the format used for flow summaries. */
string getArgumentPositionCsv(ArgumentPosition pos) { result = pos.toString() }
Node summaryNode(SummarizedCallable c, SummaryNodeState state) { result = getSummaryNode(c, state) }
/** Gets the synthesized data-flow call for `receiver`. */
@ -254,3 +290,24 @@ predicate parseReturn(string c, int n) {
)
)
}
bindingset[arg]
private int parseConstantOrRange(string arg) {
result = arg.toInt()
or
exists(int n1, int n2 |
arg.regexpCapture("ReturnValue\\[([-0-9]+)\\.\\.([0-9]+)\\]", 1).toInt() = n1 and
arg.regexpCapture("ReturnValue\\[([-0-9]+)\\.\\.([0-9]+)\\]", 2).toInt() = n2 and
result = [n1 .. n2]
)
}
bindingset[arg]
ArgumentPosition parseParamBody(string arg) {
result = parseConstantOrRange(arg)
}
bindingset[arg]
ParameterPosition parseArgBody(string arg) {
result = parseConstantOrRange(arg)
}