Skip to content

Commit 1b7339a

Browse files
michaelnebelmichaelnebel
committed
C#: Rewrite the typed based model generator.
1 parent 2d57b7d commit 1b7339a

File tree

1 file changed

+191
-95
lines changed

1 file changed

+191
-95
lines changed

‎csharp/ql/src/utils/model-generator/internal/CaptureTheoremsForFreeSummaryModels.qll

Lines changed: 191 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
private import csharp
2+
private import dotnet
23
private import semmle.code.csharp.frameworks.system.collections.Generic as GenericCollections
34
private import semmle.code.csharp.dataflow.internal.DataFlowPrivate
45
private import semmle.code.csharp.frameworks.system.linq.Expressions
@@ -8,7 +9,7 @@ private import CaptureModels
89
/**
910
* Holds if `t` is a subtype (reflexive/transitive) of `IEnumerable<T>`, where `T` = `tp`.
1011
*/
11-
private predicate isGenericCollectionType(ValueOrRefType t, TypeParameter tp) {
12+
private predicate genericCollectionType(ValueOrRefType t, TypeParameter tp) {
1213
exists(ConstructedGeneric t2 |
1314
t2 = t.getABaseType*() and
1415
t2.getUnboundDeclaration() instanceof
@@ -18,118 +19,213 @@ private predicate isGenericCollectionType(ValueOrRefType t, TypeParameter tp) {
1819
}
1920

2021
/**
21-
* A class of callables that are relevant generating summaries for based
22-
* on the Theorems for Free approach.
22+
* Holds if `tp` is a type parameter of `generic`.
2323
*/
24-
class TheoremTargetApi extends Specific::TargetApiSpecific {
25-
TheoremTargetApi() { Specific::isRelevantForTheoremModels(this) }
26-
27-
private predicate isClassTypeParameter(TypeParameter t) {
28-
t = this.getDeclaringType().(UnboundGeneric).getATypeParameter()
29-
}
24+
private predicate unboundGeneric(UnboundGeneric generic, TypeParameter tp) {
25+
tp = generic.getATypeParameter()
26+
}
3027

31-
bindingset[t]
32-
private string getAccess(TypeParameter t) {
33-
exists(string access |
34-
if isGenericCollectionType(this.getDeclaringType(), t)
35-
then access = ".Element"
36-
else access = ".SyntheticField[ArgType" + t.getIndex() + "]"
37-
|
38-
result = Specific::qualifierString() + access
39-
)
40-
}
28+
/**
29+
* Holds if `tp` is a type parameter of the immediate type declaring `callable`.
30+
*/
31+
private predicate classTypeParameter(DotNet::Callable callable, TypeParameter tp) {
32+
unboundGeneric(callable.getDeclaringType(), tp)
33+
}
4134

42-
bindingset[t]
43-
private string getReturnAccess(TypeParameter t) {
44-
exists(string access |
45-
(
46-
if isGenericCollectionType(this.getReturnType(), t)
47-
then access = ".Element"
48-
else access = ""
49-
) and
50-
result = "ReturnValue" + access
51-
)
52-
}
35+
/**
36+
* Holds if `tp` is type parameter of `callable` or the type declaring `callable`.
37+
*/
38+
private predicate localTypeParameter(DotNet::Callable callable, TypeParameter tp) {
39+
classTypeParameter(callable, tp) or unboundGeneric(callable, tp)
40+
}
5341

54-
/**
55-
* Holds if `this` returns a value of type `t` or a collection of type `t`.
56-
*/
57-
private predicate returns(TypeParameter t) {
58-
this.getReturnType() = t or isGenericCollectionType(this.getReturnType(), t)
59-
}
42+
private predicate constructedGeneric(ConstructedType t, TypeParameter tp) {
43+
t.getATypeArgument() = tp
44+
}
6045

61-
/**
62-
* Holds if `this` has a parameter `p`, which is of type `t`
63-
* or collection of type `t`.
64-
*/
65-
private predicate parameter(TypeParameter t, Parameter p) {
66-
p = this.getAParameter() and
46+
/**
47+
* Holds if `callable` has a parameter of type `tp`
48+
* or collection parameterized over type `tp`.
49+
*/
50+
private predicate parameter(DotNet::Callable callable, string input, TypeParameter tp) {
51+
exists(Parameter p |
52+
input = Specific::parameterAccess(p) and
53+
p = callable.getAParameter() and
6754
(
68-
// Parameter of type t
69-
p.getType() = t
55+
// Parameter of type tp
56+
p.getType() = tp
7057
or
71-
// Parameter is a collection of type t
72-
isGenericCollectionType(p.getType(), t)
58+
// Parameter is a collection of type tp
59+
genericCollectionType(p.getType(), tp)
7360
)
74-
}
61+
)
62+
}
7563

76-
/**
77-
* Gets the string representation of a summary for `this`, where this has a signature like
78-
* this : T -> S
79-
* where T is type parameter for the class declaring `this`.
80-
* Important cases are S = unit (setter) and S = T (both getter and setter).
81-
*/
82-
private string getSetterSummary() {
83-
exists(TypeParameter t, Parameter p |
84-
this.isClassTypeParameter(t) and
85-
this.parameter(t, p)
86-
|
87-
result = asValueModel(this, Specific::parameterAccess(p), this.getAccess(t))
88-
)
89-
}
64+
/**
65+
* Gets the string representation of a synthetic field corresponding to `tp`.
66+
*/
67+
private string getSyntheticField(TypeParameter tp) {
68+
result = ".SyntheticField[ArgType" + tp.getIndex() + "]"
69+
}
9070

91-
/**
92-
* Gets the string representation of a summary for `this`, where this has a signature like
93-
* this : S -> T
94-
* where T is type parameter for the class declaring `this`.
95-
* Important cases are S = unit (getter) and S = T (both getter and setter).
96-
*/
97-
private string getGetterSummary() {
98-
exists(TypeParameter t |
99-
this.isClassTypeParameter(t) and
100-
this.returns(t)
101-
|
102-
result = asValueModel(this, this.getAccess(t), this.getReturnAccess(t))
103-
)
104-
}
71+
/**
72+
* Gets a models as data string representation of, how a value of type `tp`
73+
* can be read or stored implicitly in relation to `callable`.
74+
*/
75+
private string implicit(DotNet::Callable callable, TypeParameter tp) {
76+
classTypeParameter(callable, tp) and
77+
exists(string access |
78+
if genericCollectionType(callable.getDeclaringType(), tp)
79+
then access = ".Element"
80+
else access = getSyntheticField(tp)
81+
|
82+
result = Specific::qualifierString() + access
83+
)
84+
}
10585

106-
/**
107-
* Gets the string representation of a summary for `this`, where this has a signature like
108-
* this : (T -> V1) -> V2
109-
* where T is type parameter for the class declaring `this`.
110-
*/
111-
private string getApplySummary() {
112-
exists(TypeParameter t, Parameter p1, Parameter p2 |
113-
this.isClassTypeParameter(t) and
114-
p1 = this.getAParameter() and
115-
p2 = p1.getType().(SystemLinqExpressions::DelegateExtType).getDelegateType().getAParameter() and
116-
p2.getType() = t
117-
|
118-
result =
119-
asValueModel(this, this.getAccess(t),
120-
Specific::parameterAccess(p1) + ".Parameter[" + p2.getPosition() + "]")
121-
)
122-
}
86+
/**
87+
* Holds if `callable` has a delegate type parameter `tp` at parameter position `position`.
88+
*/
89+
private predicate delegate(DotNet::Callable callable, DelegateType dt, int position) {
90+
exists(Parameter p |
91+
p = callable.getAParameter() and
92+
dt = p.getType().(SystemLinqExpressions::DelegateExtType).getDelegateType() and
93+
position = p.getPosition()
94+
)
95+
}
96+
97+
/**
98+
* Gets models as data input/output access relative to the type parameter `tp` in the
99+
* type `t` in the scope of `callable`.
100+
*
101+
* Note: This predicate has to be inlined as `callable` is not related to `return` or `tp`
102+
* in every disjunction.
103+
*/
104+
pragma[inline]
105+
private string getAccess(DotNet::Callable callable, Type return, TypeParameter tp) {
106+
return = tp and result = ""
107+
or
108+
genericCollectionType(return, tp) and result = ".Element"
109+
or
110+
not genericCollectionType(return, tp) and
111+
(
112+
constructedGeneric(return, tp)
113+
or
114+
callable.getDeclaringType() = return and unboundGeneric(return, tp)
115+
) and
116+
result = getSyntheticField(tp)
117+
}
118+
119+
/**
120+
* Holds if `input` is a models as data string representation of, how a value of type `tp`
121+
* (or a generic parameterized over `tp`) can be generated by a delegate parameter of `callable`.
122+
*/
123+
private predicate source(DotNet::Callable callable, string input, TypeParameter tp) {
124+
exists(DelegateType dt, int position, Type return, string access |
125+
delegate(callable, dt, position) and
126+
return = dt.getReturnType() and
127+
access = getAccess(callable, return, tp) and
128+
input = "Argument[" + position + "].ReturnValue" + access
129+
)
130+
}
131+
132+
/**
133+
* Holds if `input` is a models as data string representation of, how a
134+
* value of type `tp` (or a generic parameterized over `tp`)
135+
* can be provided as input to `callable`.
136+
* This includes
137+
* (1) The implicit synthetic field(s) of the declaring type of `callable`.
138+
* (2) The parameters of `callable`.
139+
* (3) Any delegate parameters of `callable`.
140+
*/
141+
private predicate input(DotNet::Callable callable, string input, TypeParameter tp) {
142+
input = implicit(callable, tp)
143+
or
144+
parameter(callable, input, tp)
145+
or
146+
source(callable, input, tp)
147+
}
148+
149+
/**
150+
* Holds if `callable` returns a value of type `tp` (or a generic parameterized over `tp`) and `output`
151+
* is a models as data string representation of, how data is routed to the return.
152+
*/
153+
private predicate returns(DotNet::Callable callable, TypeParameter tp, string output) {
154+
exists(Type return, string access | return = callable.getReturnType() |
155+
access = getAccess(callable, return, tp) and
156+
output = "ReturnValue" + access
157+
)
158+
}
159+
160+
/**
161+
* Holds if `callable` has a delegate parameter that accepts a value of type `tp`
162+
* and `output` is the models as data string representation of, how data is routed to
163+
* the delegate parameter.
164+
*/
165+
private predicate sink(DotNet::Callable callable, TypeParameter tp, string output) {
166+
exists(DelegateType dt, int position, Type t, Parameter p |
167+
delegate(callable, dt, position) and
168+
p = dt.getAParameter() and
169+
t = p.getType() and
170+
t = tp and
171+
output = "Argument[" + position + "]" + ".Parameter[" + p.getPosition() + "]"
172+
)
173+
}
174+
175+
/**
176+
* Holds if `output` is a models as data string representation of, how values of type `tp`
177+
* (or generics parameterized over `tp`) can be routed.
178+
* This includes
179+
* (1) The implicit synthetic field(s) of the declaring type of `callable`.
180+
* (2) The return of `callable`.
181+
* (3) Any delegate parameters of `callable`.
182+
*/
183+
private predicate output(DotNet::Callable callable, TypeParameter tp, string output) {
184+
output = implicit(callable, tp)
185+
or
186+
returns(callable, tp, output)
187+
or
188+
sink(callable, tp, output)
189+
}
190+
191+
/**
192+
* A class of callables that are relevant generating summaries for based
193+
* on the Theorems for Free approach.
194+
*/
195+
class TheoremTargetApi extends Specific::TargetApiSpecific {
196+
TheoremTargetApi() { Specific::isRelevantForTheoremModels(this) }
123197

124198
/**
125-
* Gets the string representation of all summaries based on the Theorems for Free approach.
199+
* Gets the string representation of all type based summaries inspired by
200+
* the Theorems for Free approach.
201+
*
202+
* Basic example signatures could be
203+
* this : T -> \alpha
204+
* this : \beta -> T
205+
* where T is type parameter on `this` or on the declaring type of `this`.
206+
*
207+
* Important special cases are \alpha = unit (setter),
208+
* \alpha = T (getter, setter and id) and \beta = unit (getter).
209+
*
210+
* Complex example signatures could be
211+
* this : (T -> S) -> S
212+
* this : S1 x (S1 -> S2) -> S2
213+
* where T is type parameter of the class declaring `this` and S, S1 and S2 are type parameters
214+
* of `this`.
126215
*/
127216
string getSummaries() {
128-
result = [this.getSetterSummary(), this.getGetterSummary(), this.getApplySummary()]
217+
exists(TypeParameter tp, string input, string output |
218+
localTypeParameter(this, tp) and
219+
input(this, input, tp) and
220+
output(this, tp, output) and
221+
input != output
222+
|
223+
result = asValueModel(this, input, output)
224+
)
129225
}
130226
}
131227

132228
/**
133-
* Returns the Theorems for Free summaries for `api`.
229+
* Returns the Theorems for Free inspired typed based summaries for `api`.
134230
*/
135231
string captureFlow(TheoremTargetApi api) { result = api.getSummaries() }

0 commit comments

Comments
 (0)