Add support for barrier guards in functions that indicate success by returning nil

Typically these are returning a nil error when sanitization succeeds.
This commit is contained in:
Chris Smowton
2020-11-12 18:55:16 +00:00
parent 7bbf9ed860
commit 387a13f22a

View File

@@ -1162,6 +1162,9 @@ abstract class BarrierGuard extends Node {
or
onlyPossibleReturnOfNonNil(fd, outp, ret) and
p.isNonNil()
or
onlyPossibleReturnOfNil(fd, outp, ret) and
p.isNil()
)
}
}
@@ -1207,3 +1210,42 @@ private predicate onlyPossibleReturnOfNonNil(FuncDecl fd, FunctionOutput res, No
otherRet.asExpr() = Builtin::nil().getAReference()
)
}
/**
* Holds if function `f`'s result `output`, which must be a return value, is always non-nil.
*/
private predicate certainlyReturnsNonNil(Function f, FunctionOutput output) {
output.isResult(_) and
(
f.hasQualifiedName("errors", "New")
or
f in [Builtin::new(), Builtin::make()]
or
exists(FuncDecl fd | fd = f.getFuncDecl() |
forex(DataFlow::Node ret | ret = output.getEntryNode(fd) | isCertainlyNotNil(ret))
)
)
}
/**
* Holds if `node` is always non-nil.
*/
private predicate isCertainlyNotNil(DataFlow::Node node) {
node instanceof DataFlow::AddressOperationNode
or
exists(DataFlow::CallNode c, FunctionOutput output | output.getExitNode(c) = node |
certainlyReturnsNonNil(c.getTarget(), output)
)
}
/**
* Holds if `ret` is the only data-flow node whose value contributes to the output `res` of `fd`
* that returns `nil`, since all the other output nodes are known to be non-nil.
*/
private predicate onlyPossibleReturnOfNil(FuncDecl fd, FunctionOutput res, DataFlow::Node ret) {
ret = res.getEntryNode(fd) and
ret.asExpr() = Builtin::nil().getAReference() and
forall(DataFlow::Node otherRet | otherRet = res.getEntryNode(fd) and otherRet != ret |
isCertainlyNotNil(otherRet)
)
}