C#: Address review comments.

This commit is contained in:
Michael Nebel
2022-09-17 13:51:03 +02:00
parent b05a1f4f39
commit a464e5be72

View File

@@ -18,29 +18,19 @@ private predicate genericCollectionType(ValueOrRefType t, TypeParameter tp) {
)
}
/**
* Holds if `tp` is a type parameter of `generic`.
*/
private predicate unboundGeneric(UnboundGeneric generic, TypeParameter tp) {
tp = generic.getATypeParameter()
}
/**
* Holds if `tp` is a type parameter of the immediate type declaring `callable`.
*/
private predicate classTypeParameter(DotNet::Callable callable, TypeParameter tp) {
unboundGeneric(callable.getDeclaringType(), tp)
callable.getDeclaringType().(UnboundGeneric).getATypeParameter() = tp
}
/**
* Holds if `tp` is type parameter of `callable` or the type declaring `callable`.
*/
private predicate localTypeParameter(DotNet::Callable callable, TypeParameter tp) {
classTypeParameter(callable, tp) or unboundGeneric(callable, tp)
}
private predicate constructedGeneric(ConstructedType t, TypeParameter tp) {
t.getATypeArgument() = tp
classTypeParameter(callable, tp) or
callable.(UnboundGeneric).getATypeParameter() = tp
}
/**
@@ -101,7 +91,7 @@ private predicate delegate(DotNet::Callable callable, DelegateType dt, int posit
* Note: This predicate has to be inlined as `callable` is not related to `return` or `tp`
* in every disjunction.
*/
pragma[inline]
bindingset[callable]
private string getAccess(DotNet::Callable callable, Type return, TypeParameter tp) {
return = tp and result = ""
or
@@ -109,9 +99,9 @@ private string getAccess(DotNet::Callable callable, Type return, TypeParameter t
or
not genericCollectionType(return, tp) and
(
constructedGeneric(return, tp)
return.(ConstructedGeneric).getATypeArgument() = tp
or
callable.getDeclaringType() = return and unboundGeneric(return, tp)
callable.getDeclaringType() = return and return.(UnboundGeneric).getATypeParameter() = tp
) and
result = getSyntheticField(tp)
}
@@ -120,7 +110,7 @@ private string getAccess(DotNet::Callable callable, Type return, TypeParameter t
* Holds if `input` is a models as data string representation of, how a value of type `tp`
* (or a generic parameterized over `tp`) can be generated by a delegate parameter of `callable`.
*/
private predicate source(DotNet::Callable callable, string input, TypeParameter tp) {
private predicate delegateSource(DotNet::Callable callable, string input, TypeParameter tp) {
exists(DelegateType dt, int position, Type return, string access |
delegate(callable, dt, position) and
return = dt.getReturnType() and
@@ -143,7 +133,7 @@ private predicate input(DotNet::Callable callable, string input, TypeParameter t
or
parameter(callable, input, tp)
or
source(callable, input, tp)
delegateSource(callable, input, tp)
}
/**
@@ -162,12 +152,11 @@ private predicate returns(DotNet::Callable callable, TypeParameter tp, string ou
* and `output` is the models as data string representation of, how data is routed to
* the delegate parameter.
*/
private predicate sink(DotNet::Callable callable, TypeParameter tp, string output) {
exists(DelegateType dt, int position, Type t, Parameter p |
private predicate delegateSink(DotNet::Callable callable, TypeParameter tp, string output) {
exists(DelegateType dt, int position, Parameter p |
delegate(callable, dt, position) and
p = dt.getAParameter() and
t = p.getType() and
t = tp and
p.getType() = tp and
output = "Argument[" + position + "]" + ".Parameter[" + p.getPosition() + "]"
)
}
@@ -185,7 +174,7 @@ private predicate output(DotNet::Callable callable, TypeParameter tp, string out
or
returns(callable, tp, output)
or
sink(callable, tp, output)
delegateSink(callable, tp, output)
}
/**
@@ -196,22 +185,24 @@ class TypeBasedFlowTargetApi extends Specific::TargetApiSpecific {
TypeBasedFlowTargetApi() { Specific::isRelevantForTypeBasedFlowModels(this) }
/**
* Gets the string representation of all type based summaries inspired by
* the Theorems for Free approach.
* Gets the string representation of all type based summaries for `this`
* inspired by the Theorems for Free approach.
*
* Basic example signatures could be
* this : T -> \alpha
* this : \beta -> T
* where T is type parameter on `this` or on the declaring type of `this`.
*
* Important special cases are \alpha = unit (setter),
* \alpha = T (getter, setter and id) and \beta = unit (getter).
*
* Complex example signatures could be
* this : (T -> S) -> S
* this : S1 x (S1 -> S2) -> S2
* where T is type parameter of the class declaring `this` and S, S1 and S2 are type parameters
* of `this`.
* Examples could be (see C# psuedo code below)
* (1) `Get` returns a value of type `T`. We assume that the returned
* value was fetched from a (synthetic) field.
* (2) `Set` consumes a value of type `T`. We assume that the value is stored in
* a (synthetic) field.
* (3) `Apply<S>` is assumed to apply the provided function to a value stored in
* a (synthetic) field and return the result.
* (4) `Apply<S1,S2>` is assumed to apply the provided function to provided value
* and return the result.
* public class MyGeneric<T> {
* public void Set(T x) { ... }
* public T Get() { ... }
* public S Apply<S>(Func<T, S> f) { ... }
* public S2 Apply<S1, S2>(S1 x, Func<S1, S2> f) { ... }
* }
*/
string getSummaries() {
exists(TypeParameter tp, string input, string output |