C++: Add support for MaD barriers and barrier guards.
This commit is contained in:
Anders Schack-Mulligen
2025-12-12 09:57:26 +01:00
committed by Mathias Vorreiter Pedersen
parent 07ac8a5d81
commit 48254800b1
2 changed files with 69 additions and 4 deletions

View File

@@ -95,6 +95,7 @@
import cpp
private import new.DataFlow
private import semmle.code.cpp.controlflow.IRGuards
private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate as Private
private import semmle.code.cpp.ir.dataflow.internal.DataFlowUtil
private import internal.FlowSummaryImpl
@@ -367,6 +368,8 @@ private predicate elementSpec(
) {
sourceModel(namespace, type, subtypes, name, signature, ext, _, _, _, _) or
sinkModel(namespace, type, subtypes, name, signature, ext, _, _, _, _) or
barrierModel(namespace, type, subtypes, name, signature, ext, _, _, _, _) or
barrierGuardModel(namespace, type, subtypes, name, signature, ext, _, _, _, _, _) or
summaryModel(namespace, type, subtypes, name, signature, ext, _, _, _, _, _)
}
@@ -1028,6 +1031,52 @@ private module Cached {
isSinkNode(n, kind, model) and n.asNode() = node
)
}
private newtype TKindModelPair =
TMkPair(string kind, string model) { isBarrierGuardNode(_, _, kind, model) }
private GuardValue convertAcceptingValue(Public::AcceptingValue av) {
av.isTrue() and result.asBooleanValue() = true
or
av.isFalse() and result.asBooleanValue() = false
or
av.isNoException() and result.getDualValue().isThrowsException()
or
av.isZero() and result.asIntValue() = 0
or
av.isNotZero() and result.getDualValue().asIntValue() = 0
or
av.isNull() and result.isNullValue()
or
av.isNotNull() and result.isNonNullValue()
}
private predicate barrierGuardChecks(IRGuardCondition g, Expr e, GuardValue gv, TKindModelPair kmp) {
exists(
SourceSinkInterpretationInput::InterpretNode n, Public::AcceptingValue acceptingvalue,
string kind, string model
|
isBarrierGuardNode(n, acceptingvalue, kind, model) and
n.asNode().asExpr() = e and
kmp = TMkPair(kind, model) and
gv = convertAcceptingValue(acceptingvalue) and
n.asNode().(ArgumentNode).getCallInstruction() = g
)
}
/**
* Holds if `node` is specified as a barrier with the given kind in a MaD flow
* model.
*/
cached
predicate barrierNode(DataFlow::Node node, string kind, string model) {
exists(SourceSinkInterpretationInput::InterpretNode n |
isBarrierNode(n, kind, model) and n.asNode() = node
)
or
DataFlow::ParameterizedBarrierGuard<TKindModelPair, barrierGuardChecks/4>::getABarrierNode(TMkPair(kind,
model)) = node
}
}
import Cached
@@ -1044,6 +1093,12 @@ predicate sourceNode(DataFlow::Node node, string kind) { sourceNode(node, kind,
*/
predicate sinkNode(DataFlow::Node node, string kind) { sinkNode(node, kind, _) }
/**
* Holds if `node` is specified as a barrier with the given kind in a MaD flow
* model.
*/
predicate barrierNode(DataFlow::Node node, string kind) { barrierNode(node, kind, _) }
private predicate interpretSummary(
Function f, string input, string output, string kind, string provenance, string model
) {

View File

@@ -149,16 +149,26 @@ module SourceSinkInterpretationInput implements
}
predicate barrierElement(
Element n, string output, string kind, Public::Provenance provenance, string model
Element e, string output, string kind, Public::Provenance provenance, string model
) {
none()
exists(
string namespace, string type, boolean subtypes, string name, string signature, string ext
|
barrierModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance, model) and
e = interpretElement(namespace, type, subtypes, name, signature, ext)
)
}
predicate barrierGuardElement(
Element n, string input, Public::AcceptingValue acceptingvalue, string kind,
Element e, string input, Public::AcceptingValue acceptingvalue, string kind,
Public::Provenance provenance, string model
) {
none()
exists(
string package, string type, boolean subtypes, string name, string signature, string ext
|
barrierGuardModel(package, type, subtypes, name, signature, ext, input, acceptingvalue, kind, provenance, model) and
e = interpretElement(package, type, subtypes, name, signature, ext)
)
}
private newtype TInterpretNode =