mirror of
https://github.com/github/codeql.git
synced 2025-12-16 08:43:11 +01:00
Merge branch 'main' of https://github.com/github/codeql into oscarsj/mergeback-rc-3-20-into-main
This commit is contained in:
@@ -1280,39 +1280,38 @@ module Make<
|
||||
}
|
||||
}
|
||||
|
||||
signature predicate guardChecksSig(Guard g, Expr e, boolean branch);
|
||||
signature predicate guardChecksSig(Guard g, Expr e, GuardValue gv);
|
||||
|
||||
bindingset[this]
|
||||
signature class StateSig;
|
||||
signature class ParamSig;
|
||||
|
||||
private module WithState<StateSig State> {
|
||||
signature predicate guardChecksSig(Guard g, Expr e, boolean branch, State state);
|
||||
private module WithParam<ParamSig P> {
|
||||
signature predicate guardChecksSig(Guard g, Expr e, GuardValue gv, P par);
|
||||
}
|
||||
|
||||
/**
|
||||
* Extends a `BarrierGuard` input predicate with wrapped invocations.
|
||||
*/
|
||||
module ValidationWrapper<guardChecksSig/3 guardChecks0> {
|
||||
private predicate guardChecksWithState(Guard g, Expr e, boolean branch, Unit state) {
|
||||
guardChecks0(g, e, branch) and exists(state)
|
||||
private predicate guardChecksWithParam(Guard g, Expr e, GuardValue gv, Unit par) {
|
||||
guardChecks0(g, e, gv) and exists(par)
|
||||
}
|
||||
|
||||
private module StatefulWrapper = ValidationWrapperWithState<Unit, guardChecksWithState/4>;
|
||||
private module ParameterizedWrapper =
|
||||
ParameterizedValidationWrapper<Unit, guardChecksWithParam/4>;
|
||||
|
||||
/**
|
||||
* Holds if the guard `g` validates the SSA definition `def` upon evaluating to `val`.
|
||||
*/
|
||||
predicate guardChecksDef(Guard g, SsaDefinition def, GuardValue val) {
|
||||
StatefulWrapper::guardChecksDef(g, def, val, _)
|
||||
ParameterizedWrapper::guardChecksDef(g, def, val, _)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Extends a `BarrierGuard` input predicate with wrapped invocations.
|
||||
*/
|
||||
module ValidationWrapperWithState<
|
||||
StateSig State, WithState<State>::guardChecksSig/4 guardChecks0>
|
||||
{
|
||||
module ParameterizedValidationWrapper<ParamSig P, WithParam<P>::guardChecksSig/4 guardChecks0> {
|
||||
private import WrapperGuard
|
||||
|
||||
/**
|
||||
@@ -1321,12 +1320,12 @@ module Make<
|
||||
* parameter has been validated by the given guard.
|
||||
*/
|
||||
private predicate validReturnInValidationWrapper(
|
||||
ReturnExpr ret, ParameterPosition ppos, GuardValue retval, State state
|
||||
ReturnExpr ret, ParameterPosition ppos, GuardValue retval, P par
|
||||
) {
|
||||
exists(NonOverridableMethod m, SsaParameterInit param, Guard guard, GuardValue val |
|
||||
m.getAReturnExpr() = ret and
|
||||
param.getParameter() = m.getParameter(ppos) and
|
||||
guardChecksDef(guard, param, val, state)
|
||||
guardChecksDef(guard, param, val, par)
|
||||
|
|
||||
guard.valueControls(ret.getBasicBlock(), val) and
|
||||
relevantReturnExprValue(m, ret, retval)
|
||||
@@ -1341,7 +1340,7 @@ module Make<
|
||||
* that the argument has been validated by the given guard.
|
||||
*/
|
||||
private NonOverridableMethod validationWrapper(
|
||||
ParameterPosition ppos, GuardValue retval, State state
|
||||
ParameterPosition ppos, GuardValue retval, P par
|
||||
) {
|
||||
forex(ReturnExpr ret |
|
||||
result.getAReturnExpr() = ret and
|
||||
@@ -1350,12 +1349,12 @@ module Make<
|
||||
disjointValues(notRetval, retval)
|
||||
)
|
||||
|
|
||||
validReturnInValidationWrapper(ret, ppos, retval, state)
|
||||
validReturnInValidationWrapper(ret, ppos, retval, par)
|
||||
)
|
||||
or
|
||||
exists(SsaParameterInit param, BasicBlock bb, Guard guard, GuardValue val |
|
||||
param.getParameter() = result.getParameter(ppos) and
|
||||
guardChecksDef(guard, param, val, state) and
|
||||
guardChecksDef(guard, param, val, par) and
|
||||
guard.valueControls(bb, val) and
|
||||
normalExitBlock(bb) and
|
||||
retval = TException(false)
|
||||
@@ -1365,12 +1364,12 @@ module Make<
|
||||
/**
|
||||
* Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
|
||||
*/
|
||||
private predicate guardChecks(Guard g, Expr e, GuardValue val, State state) {
|
||||
guardChecks0(g, e, val.asBooleanValue(), state)
|
||||
private predicate guardChecks(Guard g, Expr e, GuardValue val, P par) {
|
||||
guardChecks0(g, e, val, par)
|
||||
or
|
||||
exists(NonOverridableMethodCall call, ParameterPosition ppos, ArgumentPosition apos |
|
||||
g = call and
|
||||
call.getMethod() = validationWrapper(ppos, val, state) and
|
||||
call.getMethod() = validationWrapper(ppos, val, par) and
|
||||
call.getArgument(apos) = e and
|
||||
parameterMatch(pragma[only_bind_out](ppos), pragma[only_bind_out](apos))
|
||||
)
|
||||
@@ -1379,9 +1378,9 @@ module Make<
|
||||
/**
|
||||
* Holds if the guard `g` validates the SSA definition `def` upon evaluating to `val`.
|
||||
*/
|
||||
predicate guardChecksDef(Guard g, SsaDefinition def, GuardValue val, State state) {
|
||||
predicate guardChecksDef(Guard g, SsaDefinition def, GuardValue val, P par) {
|
||||
exists(Expr e |
|
||||
guardChecks(g, e, val, state) and
|
||||
guardChecks(g, e, val, par) and
|
||||
guardReadsSsaVar(e, def)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -75,6 +75,9 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
|
||||
/** Gets a limit on the number of reads out of sources and number of stores into sinks. */
|
||||
default int accessPathLimit() { result = Lang::accessPathLimit() }
|
||||
|
||||
/** Gets the access path limit used in the internal invocation of the standard data flow library. */
|
||||
default int accessPathLimitInternal() { result = Lang::accessPathLimit() }
|
||||
|
||||
/** Holds if `c` is relevant for reads out of sources or stores into sinks. */
|
||||
default predicate isRelevantContent(ContentSet c) { any() }
|
||||
}
|
||||
@@ -110,7 +113,7 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
|
||||
|
||||
FlowFeature getAFeature() { result = ContentConfig::getAFeature() }
|
||||
|
||||
predicate accessPathLimit = ContentConfig::accessPathLimit/0;
|
||||
predicate accessPathLimit = ContentConfig::accessPathLimitInternal/0;
|
||||
|
||||
// needed to record reads/stores inside summarized callables
|
||||
predicate includeHiddenNodes() { any() }
|
||||
@@ -274,6 +277,16 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the length of this access path.
|
||||
*/
|
||||
int length() {
|
||||
this = TAccessPathNil() and
|
||||
result = 0
|
||||
or
|
||||
result = this.getTail().length() + 1
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the content set at index `i` in this access path, if any.
|
||||
*/
|
||||
|
||||
@@ -207,6 +207,28 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
|
||||
flowLocal(source, sink) and Config::observeOverlayInformedIncrementalMode()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `source` to some sink.
|
||||
* This is a local predicate that only has results local to the overlay/base database.
|
||||
*/
|
||||
predicate flowFromLocal(Node source) = forceLocal(Flow::flowFrom/1)(source)
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `source` to some sink.
|
||||
*/
|
||||
predicate flowFrom(Node source) {
|
||||
Flow::flowFrom(source)
|
||||
or
|
||||
// If we are overlay informed (i.e. we are not diff-informed), we
|
||||
// merge in the local results which includes the base database results.
|
||||
flowFromLocal(source) and Config::observeOverlayInformedIncrementalMode()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `source` to some sink.
|
||||
*/
|
||||
predicate flowFromExpr(Lang::DataFlowExpr source) { flowFrom(exprNode(source)) }
|
||||
|
||||
/**
|
||||
* Holds if data can flow from some source to `sink`.
|
||||
* This is a local predicate that only has results local to the overlay/base database.
|
||||
@@ -3501,6 +3523,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `source` to some sink.
|
||||
*/
|
||||
predicate flowFrom(Node source) { exists(PathNode n | n.isSource() and n.getNode() = source) }
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `source` to some sink.
|
||||
*/
|
||||
predicate flowFromExpr(Expr source) { flowFrom(exprNode(source)) }
|
||||
|
||||
/**
|
||||
* Holds if data can flow from some source to `sink`.
|
||||
*/
|
||||
|
||||
@@ -74,6 +74,9 @@ signature module InputSig<LocationSig Location, DF::InputSig<Location> DataFlowL
|
||||
) {
|
||||
none()
|
||||
}
|
||||
|
||||
/** Holds if `(n1, n2)` should be excluded from the consistency test `localFlowIsLocal`. */
|
||||
default predicate localFlowIsLocalExclude(DataFlowLang::Node n1, DataFlowLang::Node n2) { none() }
|
||||
}
|
||||
|
||||
module MakeConsistency<
|
||||
@@ -169,6 +172,7 @@ module MakeConsistency<
|
||||
query predicate localFlowIsLocal(Node n1, Node n2, string msg) {
|
||||
simpleLocalFlowStep(n1, n2, _) and
|
||||
nodeGetEnclosingCallable(n1) != nodeGetEnclosingCallable(n2) and
|
||||
not Input::localFlowIsLocalExclude(n1, n2) and
|
||||
msg = "Local flow step does not preserve enclosing callable."
|
||||
}
|
||||
|
||||
@@ -240,6 +244,13 @@ module MakeConsistency<
|
||||
|
||||
private predicate hasPost(Node n) { exists(PostUpdateNode post | post.getPreUpdateNode() = n) }
|
||||
|
||||
/**
|
||||
* Consider code like `a.b.f = source()`. There is flow from `source()` to
|
||||
* `[post] a.b` (with an appropriate access path), but we also want there to
|
||||
* be flow to `[post] a` (with an appropriate access path). The data flow
|
||||
* library is able to infer this step because there is a read step from `a`
|
||||
* to `a.b`, as long as the post-update node for `a` exists.
|
||||
*/
|
||||
query predicate reverseRead(Node n, string msg) {
|
||||
exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
|
||||
not Input::reverseReadExclude(n) and
|
||||
|
||||
@@ -215,6 +215,35 @@ module Make<
|
||||
]
|
||||
}
|
||||
|
||||
class AcceptingValue extends string {
|
||||
AcceptingValue() {
|
||||
this =
|
||||
[
|
||||
"true",
|
||||
"false",
|
||||
"no-exception",
|
||||
"zero",
|
||||
"not-zero",
|
||||
"null",
|
||||
"not-null",
|
||||
]
|
||||
}
|
||||
|
||||
predicate isTrue() { this = "true" }
|
||||
|
||||
predicate isFalse() { this = "false" }
|
||||
|
||||
predicate isNoException() { this = "no-exception" }
|
||||
|
||||
predicate isZero() { this = "zero" }
|
||||
|
||||
predicate isNotZero() { this = "not-zero" }
|
||||
|
||||
predicate isNull() { this = "null" }
|
||||
|
||||
predicate isNotNull() { this = "not-null" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A class used to represent provenance values for MaD models.
|
||||
*
|
||||
@@ -2015,6 +2044,12 @@ module Make<
|
||||
not exists(interpretComponent(c))
|
||||
}
|
||||
|
||||
/** Holds if `acceptingvalue` is not a valid barrier guard accepting-value. */
|
||||
bindingset[acceptingvalue]
|
||||
predicate invalidAcceptingValue(string acceptingvalue) {
|
||||
not acceptingvalue instanceof AcceptingValue
|
||||
}
|
||||
|
||||
/** Holds if `provenance` is not a valid provenance value. */
|
||||
bindingset[provenance]
|
||||
predicate invalidProvenance(string provenance) { not provenance instanceof Provenance }
|
||||
@@ -2052,6 +2087,23 @@ module Make<
|
||||
Element n, string input, string kind, Provenance provenance, string model
|
||||
);
|
||||
|
||||
/**
|
||||
* Holds if an external barrier specification exists for `n` with output specification
|
||||
* `output` and kind `kind`.
|
||||
*/
|
||||
predicate barrierElement(
|
||||
Element n, string output, string kind, Provenance provenance, string model
|
||||
);
|
||||
|
||||
/**
|
||||
* Holds if an external barrier guard specification exists for `n` with input
|
||||
* specification `input`, accepting value `acceptingvalue`, and kind `kind`.
|
||||
*/
|
||||
predicate barrierGuardElement(
|
||||
Element n, string input, AcceptingValue acceptingvalue, string kind,
|
||||
Provenance provenance, string model
|
||||
);
|
||||
|
||||
class SourceOrSinkElement extends Element;
|
||||
|
||||
/** An entity used to interpret a source/sink specification. */
|
||||
@@ -2105,7 +2157,9 @@ module Make<
|
||||
|
||||
private predicate sourceSinkSpec(string spec) {
|
||||
sourceElement(_, spec, _, _, _) or
|
||||
sinkElement(_, spec, _, _, _)
|
||||
sinkElement(_, spec, _, _, _) or
|
||||
barrierElement(_, spec, _, _, _) or
|
||||
barrierGuardElement(_, spec, _, _, _, _)
|
||||
}
|
||||
|
||||
private module AccessPath = AccessPathSyntax::AccessPath<sourceSinkSpec/1>;
|
||||
@@ -2160,11 +2214,34 @@ module Make<
|
||||
)
|
||||
}
|
||||
|
||||
private predicate barrierElementRef(
|
||||
InterpretNode ref, SourceSinkAccessPath output, string kind, string model
|
||||
) {
|
||||
exists(SourceOrSinkElement e |
|
||||
barrierElement(e, output, kind, _, model) and
|
||||
if outputNeedsReferenceExt(output.getToken(0))
|
||||
then e = ref.getCallTarget()
|
||||
else e = ref.asElement()
|
||||
)
|
||||
}
|
||||
|
||||
private predicate barrierGuardElementRef(
|
||||
InterpretNode ref, SourceSinkAccessPath input, AcceptingValue acceptingvalue, string kind,
|
||||
string model
|
||||
) {
|
||||
exists(SourceOrSinkElement e |
|
||||
barrierGuardElement(e, input, acceptingvalue, kind, _, model) and
|
||||
if inputNeedsReferenceExt(input.getToken(0))
|
||||
then e = ref.getCallTarget()
|
||||
else e = ref.asElement()
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if the first `n` tokens of `output` resolve to the given interpretation. */
|
||||
private predicate interpretOutput(
|
||||
SourceSinkAccessPath output, int n, InterpretNode ref, InterpretNode node
|
||||
) {
|
||||
sourceElementRef(ref, output, _, _) and
|
||||
(sourceElementRef(ref, output, _, _) or barrierElementRef(ref, output, _, _)) and
|
||||
n = 0 and
|
||||
(
|
||||
if output = ""
|
||||
@@ -2220,7 +2297,7 @@ module Make<
|
||||
private predicate interpretInput(
|
||||
SourceSinkAccessPath input, int n, InterpretNode ref, InterpretNode node
|
||||
) {
|
||||
sinkElementRef(ref, input, _, _) and
|
||||
(sinkElementRef(ref, input, _, _) or barrierGuardElementRef(ref, input, _, _, _)) and
|
||||
n = 0 and
|
||||
(
|
||||
if input = ""
|
||||
@@ -2280,6 +2357,30 @@ module Make<
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` is specified as a barrier with the given kind in a MaD flow
|
||||
* model.
|
||||
*/
|
||||
predicate isBarrierNode(InterpretNode node, string kind, string model) {
|
||||
exists(InterpretNode ref, SourceSinkAccessPath output |
|
||||
barrierElementRef(ref, output, kind, model) and
|
||||
interpretOutput(output, output.getNumToken(), ref, node)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` is specified as a barrier guard argument with the
|
||||
* given kind in a MaD flow model.
|
||||
*/
|
||||
predicate isBarrierGuardNode(
|
||||
InterpretNode node, AcceptingValue acceptingvalue, string kind, string model
|
||||
) {
|
||||
exists(InterpretNode ref, SourceSinkAccessPath input |
|
||||
barrierGuardElementRef(ref, input, acceptingvalue, kind, model) and
|
||||
interpretInput(input, input.getNumToken(), ref, node)
|
||||
)
|
||||
}
|
||||
|
||||
final private class SourceOrSinkElementFinal = SourceOrSinkElement;
|
||||
|
||||
signature predicate sourceOrSinkElementSig(
|
||||
|
||||
@@ -173,7 +173,7 @@ module KindValidation<KindValidationConfigSig Config> {
|
||||
or
|
||||
exists(string kind, string msg | Config::sinkKind(kind) |
|
||||
not kind instanceof ValidSinkKind and
|
||||
msg = "Invalid kind \"" + kind + "\" in sink model." and
|
||||
msg = "Invalid kind \"" + kind + "\" in sink or barrier model." and
|
||||
// The part of this message that refers to outdated sink kinds can be deleted after June 1st, 2024.
|
||||
if kind instanceof OutdatedSinkKind
|
||||
then result = msg + " " + kind.(OutdatedSinkKind).outdatedMessage()
|
||||
|
||||
@@ -277,6 +277,16 @@ module MakeModelGeneratorFactory<
|
||||
*/
|
||||
predicate isAdditionalContentFlowStep(Lang::Node nodeFrom, Lang::Node nodeTo);
|
||||
|
||||
/**
|
||||
* Gets the access path limit for content flow analysis.
|
||||
*/
|
||||
default int contentAccessPathLimit() { result = 2 }
|
||||
|
||||
/**
|
||||
* Gets the internal access path limit for content flow analysis.
|
||||
*/
|
||||
default int contentAccessPathLimitInternal() { result = Lang::accessPathLimit() }
|
||||
|
||||
/**
|
||||
* Holds if the content set `c` is field like.
|
||||
*/
|
||||
@@ -650,7 +660,10 @@ module MakeModelGeneratorFactory<
|
||||
exists(Type t | t = n.(NodeExtended).getType() and not isRelevantType(t))
|
||||
}
|
||||
|
||||
int accessPathLimit() { result = 2 }
|
||||
predicate accessPathLimit = SummaryModelGeneratorInput::contentAccessPathLimit/0;
|
||||
|
||||
predicate accessPathLimitInternal =
|
||||
SummaryModelGeneratorInput::contentAccessPathLimitInternal/0;
|
||||
|
||||
predicate isRelevantContent(DataFlow::ContentSet s) { isRelevantContent0(s) }
|
||||
|
||||
@@ -703,14 +716,17 @@ module MakeModelGeneratorFactory<
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the access path `ap` is not a parameter or returnvalue of a callback
|
||||
* stored in a field.
|
||||
* Holds if `ap` is valid for generating summary models.
|
||||
*
|
||||
* That is, we currently don't include summaries that rely on parameters or return values
|
||||
* of callbacks stored in fields.
|
||||
* We currently don't include summaries that rely on parameters or return values
|
||||
* of callbacks stored in fields, as those are not supported by the data flow
|
||||
* library.
|
||||
*
|
||||
* We also exclude access paths with contents not supported by `printContent`.
|
||||
*/
|
||||
private predicate validateAccessPath(PropagateContentFlow::AccessPath ap) {
|
||||
not (mentionsField(ap) and mentionsCallback(ap))
|
||||
not (mentionsField(ap) and mentionsCallback(ap)) and
|
||||
forall(int i | i in [0 .. ap.length() - 1] | exists(getContent(ap, i)))
|
||||
}
|
||||
|
||||
private predicate apiFlow(
|
||||
@@ -720,7 +736,9 @@ module MakeModelGeneratorFactory<
|
||||
) {
|
||||
PropagateContentFlow::flow(p, reads, returnNodeExt, stores, preservesValue) and
|
||||
getEnclosingCallable(returnNodeExt) = api and
|
||||
getEnclosingCallable(p) = api
|
||||
getEnclosingCallable(p) = api and
|
||||
validateAccessPath(reads) and
|
||||
validateAccessPath(stores)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -763,9 +781,7 @@ module MakeModelGeneratorFactory<
|
||||
PropagateContentFlow::AccessPath reads, ReturnNodeExt returnNodeExt,
|
||||
PropagateContentFlow::AccessPath stores, boolean preservesValue
|
||||
) {
|
||||
PropagateContentFlow::flow(p, reads, returnNodeExt, stores, preservesValue) and
|
||||
getEnclosingCallable(returnNodeExt) = api and
|
||||
getEnclosingCallable(p) = api and
|
||||
apiFlow(api, p, reads, returnNodeExt, stores, preservesValue) and
|
||||
p = api.getARelevantParameterNode()
|
||||
}
|
||||
|
||||
@@ -956,8 +972,6 @@ module MakeModelGeneratorFactory<
|
||||
input = parameterNodeAsExactInput(p) + printReadAccessPath(reads) and
|
||||
output = getExactOutput(returnNodeExt) + printStoreAccessPath(stores) and
|
||||
input != output and
|
||||
validateAccessPath(reads) and
|
||||
validateAccessPath(stores) and
|
||||
(
|
||||
if mentionsField(reads) or mentionsField(stores)
|
||||
then lift = false and api.isRelevant()
|
||||
|
||||
@@ -705,7 +705,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `app` is _not_ a possible instantiation of `constraint`.
|
||||
* Holds if `app` is _not_ a possible instantiation of `constraint`, because `app`
|
||||
* and `constraint` differ on concrete types at `path`.
|
||||
*
|
||||
* This is an approximation of `not isInstantiationOf(app, abs, constraint)`, but
|
||||
* defined without a negative occurrence of `isInstantiationOf`.
|
||||
@@ -719,9 +720,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
* `isInstantiationOf` nor `isNotInstantiationOf` will hold.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate isNotInstantiationOf(App app, TypeAbstraction abs, Constraint constraint) {
|
||||
predicate isNotInstantiationOf(
|
||||
App app, TypeAbstraction abs, Constraint constraint, TypePath path
|
||||
) {
|
||||
// `app` and `constraint` differ on a concrete type
|
||||
exists(Type t, Type t2, TypePath path |
|
||||
exists(Type t, Type t2 |
|
||||
t = resolveTypeAt(app, abs, constraint, path) and
|
||||
not t = abs.getATypeParameter() and
|
||||
app.getTypeAt(path) = t2 and
|
||||
@@ -983,6 +986,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
}
|
||||
}
|
||||
|
||||
private module SatisfiesConstraintIsInstantiationOf =
|
||||
IsInstantiationOf<HasTypeTree, TypeMentionTypeTree, IsInstantiationOfInput>;
|
||||
|
||||
/**
|
||||
* Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
|
||||
*/
|
||||
@@ -1004,13 +1010,21 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
// constraint we need to find the right implementation, which is the
|
||||
// one where the type instantiates the precondition.
|
||||
if multipleConstraintImplementations(type, constraint)
|
||||
then
|
||||
IsInstantiationOf<HasTypeTree, TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt,
|
||||
abs, condition)
|
||||
then SatisfiesConstraintIsInstantiationOf::isInstantiationOf(tt, abs, condition)
|
||||
else any()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate isNotInstantiationOf(
|
||||
HasTypeTree tt, TypeAbstraction abs, TypeMention condition, Type root
|
||||
) {
|
||||
exists(TypePath path |
|
||||
SatisfiesConstraintIsInstantiationOf::isNotInstantiationOf(tt, abs, condition, path) and
|
||||
path.isCons(root.getATypeParameter(), _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `tt` does not satisfy `constraint`.
|
||||
*
|
||||
@@ -1040,8 +1054,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
forex(TypeAbstraction abs, TypeMention condition |
|
||||
rootTypesSatisfaction(type, constraint, abs, condition, _)
|
||||
|
|
||||
IsInstantiationOf<HasTypeTree, TypeMentionTypeTree, IsInstantiationOfInput>::isNotInstantiationOf(tt,
|
||||
abs, condition)
|
||||
isNotInstantiationOf(tt, abs, condition, type)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
Reference in New Issue
Block a user