C++: Finish up implementation of MaD barriers.

This commit is contained in:
Mathias Vorreiter Pedersen
2026-01-15 18:04:57 +00:00
parent 48254800b1
commit a11b271d6e
3 changed files with 52 additions and 8 deletions

View File

@@ -1040,6 +1040,11 @@ private module Cached {
or
av.isFalse() and result.asBooleanValue() = false
or
// NOTE: The below cases don't contribute anything currently since the
// callers immediate uses `.asBooleanValue()` to convert the `GuardValue`
// to a boolean. Once we're willing to accept the breaking change of
// converting the barrier guard API to use `GuardValue`s instead `Boolean`s
// we can remove this restriction.
av.isNoException() and result.getDualValue().isThrowsException()
or
av.isZero() and result.asIntValue() = 0
@@ -1051,7 +1056,9 @@ private module Cached {
av.isNotNull() and result.isNonNullValue()
}
private predicate barrierGuardChecks(IRGuardCondition g, Expr e, GuardValue gv, TKindModelPair kmp) {
private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate as Private
private predicate barrierGuardChecks(IRGuardCondition g, Expr e, boolean gv, TKindModelPair kmp) {
exists(
SourceSinkInterpretationInput::InterpretNode n, Public::AcceptingValue acceptingvalue,
string kind, string model
@@ -1059,8 +1066,32 @@ private module Cached {
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
gv = convertAcceptingValue(acceptingvalue).asBooleanValue() and
n.asNode().(Private::ArgumentNode).getCall().asCallInstruction() = g
)
}
private newtype TKindModelPairIntPair =
MkKindModelPairIntPair(TKindModelPair pair, int indirectionIndex) {
indirectionIndex > 0 and
Private::nodeHasInstruction(_, _, indirectionIndex) and
exists(pair)
}
private predicate indirectBarrierGuardChecks(
IRGuardCondition g, Expr e, boolean gv, TKindModelPairIntPair kmp
) {
exists(
SourceSinkInterpretationInput::InterpretNode interpretNode,
Public::AcceptingValue acceptingvalue, string kind, string model, int indirectionIndex,
Private::ArgumentNode arg
|
isBarrierGuardNode(interpretNode, acceptingvalue, kind, model) and
arg = interpretNode.asNode() and
arg.asIndirectExpr(indirectionIndex) = e and
kmp = MkKindModelPairIntPair(TMkPair(kind, model), indirectionIndex) and
gv = convertAcceptingValue(acceptingvalue).asBooleanValue() and
arg.getCall().asCallInstruction() = g
)
}
@@ -1076,6 +1107,9 @@ private module Cached {
or
DataFlow::ParameterizedBarrierGuard<TKindModelPair, barrierGuardChecks/4>::getABarrierNode(TMkPair(kind,
model)) = node
or
DataFlow::ParameterizedBarrierGuard<TKindModelPairIntPair, indirectBarrierGuardChecks/4>::getAnIndirectBarrierNode(MkKindModelPairIntPair(TMkPair(kind,
model), _)) = node
}
}

View File

@@ -26,25 +26,25 @@ void sink(int*);
void test_mad(int x, int* p) {
{
if(is_clean_value(&x)) {
sink(x); // $ MISSING: external=int
sink(x); // $ external=int
}
}
{
if(is_clean_value(p)) {
sink(*p); // $ MISSING: external=int
sink(*p); // $ external=int
}
}
{
if(is_clean_pointer(p)) {
sink(p); // $ MISSING: external=int*
sink(p); // $ external=int*
}
}
{
if(is_clean_pointer(&x)) {
sink(x); // $ MISSING: external=glval<int>
sink(x); // $ external=glval<int>
}
}
}

View File

@@ -28,8 +28,15 @@ predicate barrierGuard(DataFlow::Node node, string s) {
else s = node.getType().toString().replaceAll(" ", "")
}
predicate externalBarrierGuard(DataFlow::Node node, string s) {
barrierNode(node, "test-barrier") and
if node.isGLValue()
then s = "glval<" + node.getType().toString().replaceAll(" ", "") + ">"
else s = node.getType().toString().replaceAll(" ", "")
}
module Test implements TestSig {
string getARelevantTag() { result = ["barrier", "indirect_barrier"] }
string getARelevantTag() { result = ["barrier", "indirect_barrier", "external"] }
predicate hasActualResult(Location location, string element, string tag, string value) {
exists(DataFlow::Node node |
@@ -38,6 +45,9 @@ module Test implements TestSig {
or
barrierGuard(node, value) and
tag = "barrier"
or
externalBarrierGuard(node, value) and
tag = "external"
|
element = node.toString() and
location = node.getLocation()