Merge pull request #12182 from MathiasVP/content-approx

C++: Use `Content` approximation
This commit is contained in:
Mathias Vorreiter Pedersen
2023-02-14 13:00:47 +00:00
committed by GitHub
2 changed files with 59 additions and 15 deletions

View File

@@ -795,12 +795,63 @@ predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preserves
*/
predicate allowParameterReturnInSelf(ParameterNode p) { none() }
private predicate fieldHasApproxName(Field f, string s) {
s = f.getName().charAt(0) and
// Reads and writes of union fields are tracked using `UnionContent`.
not f.getDeclaringType() instanceof Cpp::Union
}
private predicate unionHasApproxName(Cpp::Union u, string s) { s = u.getName().charAt(0) }
cached
private newtype TContentApprox =
TFieldApproxContent(string s) { fieldHasApproxName(_, s) } or
TUnionApproxContent(string s) { unionHasApproxName(_, s) }
/** An approximated `Content`. */
class ContentApprox = Unit;
class ContentApprox extends TContentApprox {
string toString() { none() } // overriden in subclasses
}
private class FieldApproxContent extends ContentApprox, TFieldApproxContent {
string s;
FieldApproxContent() { this = TFieldApproxContent(s) }
Field getAField() { fieldHasApproxName(result, s) }
string getPrefix() { result = s }
final override string toString() { result = s }
}
private class UnionApproxContent extends ContentApprox, TUnionApproxContent {
string s;
UnionApproxContent() { this = TUnionApproxContent(s) }
Cpp::Union getAUnion() { unionHasApproxName(result, s) }
string getPrefix() { result = s }
final override string toString() { result = s }
}
/** Gets an approximated value for content `c`. */
pragma[inline]
ContentApprox getContentApprox(Content c) { any() }
ContentApprox getContentApprox(Content c) {
exists(string prefix, Field f |
prefix = result.(FieldApproxContent).getPrefix() and
f = c.(FieldContent).getField() and
fieldHasApproxName(f, prefix)
)
or
exists(string prefix, Cpp::Union u |
prefix = result.(UnionApproxContent).getPrefix() and
u = c.(UnionContent).getUnion() and
unionHasApproxName(u, prefix)
)
}
private class MyConsistencyConfiguration extends Consistency::ConsistencyConfiguration {
override predicate argHasPostUpdateExclude(ArgumentNode n) {

View File

@@ -1628,9 +1628,7 @@ private newtype TContent =
// field can be read by any read of the union's fields.
indirectionIndex =
[1 .. max(Ssa::getMaxIndirectionsForType(u.getAField().getUnspecifiedType()))]
} or
TCollectionContent() or // Not used in C/C++
TArrayContent() // Not used in C/C++.
}
/**
* A description of the way data may be stored inside an object. Examples
@@ -1680,24 +1678,19 @@ class UnionContent extends Content, TUnionContent {
indirectionIndex > 1 and result = u.toString() + " indirection"
}
/** Gets a field of the underlying union of this `UnionContent`, if any. */
Field getAField() { result = u.getAField() }
/** Gets the underlying union of this `UnionContent`. */
Union getUnion() { result = u }
/** Gets the indirection index of this `UnionContent`. */
pragma[inline]
int getIndirectionIndex() {
pragma[only_bind_into](result) = pragma[only_bind_out](indirectionIndex)
}
}
/** A reference through an array. */
class ArrayContent extends Content, TArrayContent {
override string toString() { result = "[]" }
}
/** A reference through the contents of some collection-like container. */
private class CollectionContent extends Content, TCollectionContent {
override string toString() { result = "<element>" }
}
/**
* An entity that represents a set of `Content`s.
*