diff --git a/csharp/ql/src/utils/model-generator/internal/CaptureTypeBasedSummaryModels.qll b/csharp/ql/src/utils/model-generator/internal/CaptureTypeBasedSummaryModels.qll index 8b8172741dd..478247e6174 100644 --- a/csharp/ql/src/utils/model-generator/internal/CaptureTypeBasedSummaryModels.qll +++ b/csharp/ql/src/utils/model-generator/internal/CaptureTypeBasedSummaryModels.qll @@ -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` is assumed to apply the provided function to a value stored in + * a (synthetic) field and return the result. + * (4) `Apply` is assumed to apply the provided function to provided value + * and return the result. + * public class MyGeneric { + * public void Set(T x) { ... } + * public T Get() { ... } + * public S Apply(Func f) { ... } + * public S2 Apply(S1 x, Func f) { ... } + * } */ string getSummaries() { exists(TypeParameter tp, string input, string output |