C++: compute overlap on irvars with vvar indexes

This commit is contained in:
Robert Marsh
2020-01-06 09:14:03 -08:00
parent 4830e43b3e
commit ba9741f552

View File

@@ -402,49 +402,37 @@ private predicate isRelatableMemoryLocation(VariableMemoryLocation vml) {
} }
private predicate isCoveredOffset( private predicate isCoveredOffset(
VirtualVariable vv, IRVariable var, int offsetRank, VariableMemoryLocation vml IRVariable var, int offsetRank, VariableMemoryLocation vml
) { ) {
exists(int startRank, int endRank | exists(int startRank, int endRank, VirtualVariable vvar |
vml.getStartBitOffset() = rank[startRank](IntValue offset_ | isRelevantOffset(vv, offset_)) and vml.getStartBitOffset() = rank[startRank](IntValue offset_ | isRelevantOffset(vvar, offset_)) and
vml.getEndBitOffset() = rank[endRank](IntValue offset_ | isRelevantOffset(vv, offset_)) and vml.getEndBitOffset() = rank[endRank](IntValue offset_ | isRelevantOffset(vvar, offset_)) and
hasVariableAndVirtualVariable(vv, var, vml) and var = vml.getVariable() and
vvar = vml.getVirtualVariable() and
isRelatableMemoryLocation(vml) and isRelatableMemoryLocation(vml) and
offsetRank in [startRank .. endRank] offsetRank in [startRank .. endRank]
) )
} }
private predicate hasUnknownOffset(VirtualVariable vv, IRVariable var, VariableMemoryLocation vml) { private predicate hasUnknownOffset(IRVariable var, VariableMemoryLocation vml) {
hasVariableAndVirtualVariable(vv, var, vml) and vml.getVariable() = var and
( (
vml.getStartBitOffset() = Ints::unknown() or vml.getStartBitOffset() = Ints::unknown() or
vml.getEndBitOffset() = Ints::unknown() vml.getEndBitOffset() = Ints::unknown()
) )
} }
private predicate hasVariableAndVirtualVariable(
VirtualVariable vv, IRVariable var, VariableMemoryLocation vml
) {
var = vml.getVariable() and
vv = vml.getVirtualVariable()
}
private predicate overlappingIRVariableMemoryLocations( private predicate overlappingIRVariableMemoryLocations(
VariableMemoryLocation def, VariableMemoryLocation use VariableMemoryLocation def, VariableMemoryLocation use
) { ) {
exists(VirtualVariable vv, IRVariable var, int offsetRank | exists(IRVariable var, int offsetRank |
isCoveredOffset(vv, var, offsetRank, def) and isCoveredOffset(var, offsetRank, def) and
isCoveredOffset(vv, var, offsetRank, use) isCoveredOffset(var, offsetRank, use)
) )
or or
exists(VirtualVariable vv, IRVariable var | hasUnknownOffset(use.getVariable(), def)
hasUnknownOffset(vv, var, def) and
hasVariableAndVirtualVariable(vv, var, use)
)
or or
exists(VirtualVariable vv, IRVariable var | hasUnknownOffset(def.getVariable(), use)
hasUnknownOffset(vv, var, use) and
hasVariableAndVirtualVariable(vv, var, def)
)
} }
private Overlap getVariableMemoryLocationOverlap( private Overlap getVariableMemoryLocationOverlap(