C#: Update dataflow consistency queries to cater for non unique post and pre unique update notes for conditional branches.

This commit is contained in:
Michael Nebel
2022-09-28 09:18:26 +02:00
parent e8fd2bfc78
commit 2d0a377b7a
2 changed files with 18 additions and 8 deletions

View File

@@ -35,13 +35,7 @@ private class MyConsistencyConfiguration extends ConsistencyConfiguration {
override predicate argHasPostUpdateExclude(ArgumentNode n) {
n instanceof SummaryNode
or
n.asExpr().(Expr).stripCasts().getType() =
any(Type t |
not t instanceof RefType and
not t = any(TypeParameter tp | not tp.isValueType())
or
t instanceof NullType
)
not exists(getAPostUpdateNodeForArg(n.asExpr()))
or
n instanceof ImplicitCapturedArgumentNode
or
@@ -50,5 +44,21 @@ private class MyConsistencyConfiguration extends ConsistencyConfiguration {
n.asExpr() instanceof CIL::Expr
}
override predicate postHasUniquePreExclude(PostUpdateNode n) {
exists(ControlFlow::Nodes::ExprNode e, ControlFlow::Nodes::ExprNode arg |
e = getAPostUpdateNodeForArg(arg.getExpr()) and
e != arg and
n = TExprPostUpdateNode(e)
)
}
override predicate uniquePostUpdateExclude(Node n) {
exists(ControlFlow::Nodes::ExprNode e, ControlFlow::Nodes::ExprNode arg |
e = getAPostUpdateNodeForArg(arg.getExpr()) and
e != arg and
n.asExpr() = arg.getExpr()
)
}
override predicate reverseReadExclude(Node n) { n.asExpr() = any(AwaitExpr ae).getExpr() }
}

View File

@@ -197,7 +197,7 @@ private predicate relevantArgumentType(ControlFlow::Nodes::ExprNode cfn) {
}
/** Gets a node for which to construct a post-update node for argument `arg`. */
private ControlFlow::Nodes::ExprNode getAPostUpdateNodeForArg(Argument arg) {
ControlFlow::Nodes::ExprNode getAPostUpdateNodeForArg(Argument arg) {
result = getALastEvalNode*(arg.getAControlFlowNode()) and
relevantArgumentType(result) and
not exists(getALastEvalNode(result))