Dataflow: Handle non-trivial type systems with stores into a top type.

This commit is contained in:
Anders Schack-Mulligen
2024-06-21 11:24:27 +02:00
parent a26132e818
commit fdf6e30888
2 changed files with 21 additions and 1 deletions

View File

@@ -1448,11 +1448,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate compatibleContainer0(ApHeadContent apc, DataFlowType containerType) {
exists(DataFlowType containerType0, Content c |
PrevStage::storeStepCand(_, _, c, _, _, containerType0) and
not isTopType(containerType0) and
compatibleTypesCached(containerType0, containerType) and
apc = projectToHeadContent(c)
)
}
pragma[nomagic]
private predicate topTypeContent(ApHeadContent apc) {
exists(DataFlowType containerType0, Content c |
PrevStage::storeStepCand(_, _, c, _, _, containerType0) and
isTopType(containerType0) and
apc = projectToHeadContent(c)
)
}
bindingset[apc, containerType]
pragma[inline_late]
private predicate compatibleContainer(ApHeadContent apc, DataFlowType containerType) {
@@ -1484,7 +1494,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
(
if castingNodeEx(node)
then
ap instanceof ApNil or compatibleContainer(getHeadContent(ap), node.getDataFlowType())
ap instanceof ApNil or
compatibleContainer(getHeadContent(ap), node.getDataFlowType()) or
topTypeContent(getHeadContent(ap))
else any()
)
}

View File

@@ -889,6 +889,14 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
cached
predicate compatibleTypesCached(DataFlowType t1, DataFlowType t2) { compatibleTypes(t1, t2) }
private predicate relevantType(DataFlowType t) { t = getNodeType(_) }
cached
predicate isTopType(DataFlowType t) {
strictcount(DataFlowType t0 | relevantType(t0)) =
strictcount(DataFlowType t0 | relevantType(t0) and compatibleTypesCached(t, t0))
}
cached
predicate typeStrongerThanCached(DataFlowType t1, DataFlowType t2) { typeStrongerThan(t1, t2) }