Skip to content

Commit 016afac

Browse files
MichaelRFairhurstMichaelRFairhurst
committed
Add missing file, format fixes
1 parent ee6d520 commit 016afac

File tree

3 files changed

+175
-43
lines changed

3 files changed

+175
-43
lines changed

‎src/qtil/locations/CustomPathStateProblem.qll‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,8 @@ module PathStateProblem<LocationSig Location, LocatableConfig<Location> LocConfi
4848
* However, the underlying search algorithm is efficient, so this should be fast in many cases
4949
* even if this is a very large relation.
5050
*/
51-
bindingset[s1] bindingset[s2]
51+
bindingset[s1]
52+
bindingset[s2]
5253
predicate edge(Node a, State s1, Node b, State s2);
5354

5455
/**

‎test/qtil/graph/GraphPathStateSearchTest.ql‎

Lines changed: 74 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -2,18 +2,26 @@ import qtil.testing.Qnit
22
import qtil.graph.GraphPathStateSearch
33
import Family
44

5-
bindingset[relation] bindingset[result]
5+
bindingset[relation]
6+
bindingset[result]
67
string parentString(string relation) {
7-
if relation = "child" then result = "parent"
8-
else if relation = "parent" then result = "grandparent"
9-
else result = "great " + relation
8+
if relation = "child"
9+
then result = "parent"
10+
else
11+
if relation = "parent"
12+
then result = "grandparent"
13+
else result = "great " + relation
1014
}
1115

12-
bindingset[relation] bindingset[result]
16+
bindingset[relation]
17+
bindingset[result]
1318
string childString(string relation) {
14-
if relation = "parent" then result = "child"
15-
else if relation = "child" then result = "grandchild"
16-
else result = "great " + relation
19+
if relation = "parent"
20+
then result = "child"
21+
else
22+
if relation = "child"
23+
then result = "grandchild"
24+
else result = "great " + relation
1725
}
1826

1927
module BartToGrandpaConfig implements GraphPathStateSearchSig<Person> {
@@ -23,7 +31,8 @@ module BartToGrandpaConfig implements GraphPathStateSearchSig<Person> {
2331

2432
predicate end(Person p, string state) { p.getName() = "Grandpa" and state = "grandparent" }
2533

26-
bindingset[s2] bindingset[s1]
34+
bindingset[s1]
35+
bindingset[s2]
2736
predicate edge(Person p1, string s1, Person p2, string s2) {
2837
p2 = p1.getAParent() and
2938
s2 = parentString(s1)
@@ -37,9 +46,12 @@ module GrandpaToBartConfig implements GraphPathStateSearchSig<Person> {
3746

3847
predicate end(Person p, string state) { p.getName() = "Bart" and state = "grandchild" }
3948

40-
bindingset[s2] bindingset[s1]
41-
predicate edge(Person p1, State s1, Person p2, State s2) { p2 = p1.getAChild() and
42-
s2 = childString(s1) }
49+
bindingset[s1]
50+
bindingset[s2]
51+
predicate edge(Person p1, State s1, Person p2, State s2) {
52+
p2 = p1.getAChild() and
53+
s2 = childString(s1)
54+
}
4355
}
4456

4557
class TestBartForwardNodesContain extends Test, Case {
@@ -57,34 +69,40 @@ class TestBartForwardNodesContain extends Test, Case {
5769

5870
class TestBartForwardNodesState extends Test, Case {
5971
override predicate run(Qnit test) {
60-
if exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
72+
if
73+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
6174
fwd.getName() = "Bart" and
6275
fwd.getState() = "child"
63-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
76+
) and
77+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
6478
fwd.getName() = "Marge" and
6579
fwd.getState() = "parent"
66-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
80+
) and
81+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
6782
fwd.getName() = "Homer" and
6883
fwd.getState() = "parent"
69-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
84+
) and
85+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
7086
fwd.getName() = "Clancy" and
7187
fwd.getState() = "grandparent"
72-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
88+
) and
89+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
7390
fwd.getName() = "Jacquelin" and
7491
fwd.getState() = "grandparent"
75-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
92+
) and
93+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
7694
fwd.getName() = "Mona" and
7795
fwd.getState() = "grandparent"
78-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
96+
) and
97+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
7998
fwd.getName() = "Grandpa" and
8099
fwd.getState() = "grandparent"
81-
)
100+
)
82101
then test.pass("All forward nodes from Bart have the correct state")
83102
else test.fail("Some forward nodes from Bart have incorrect state")
84103
}
85104
}
86105

87-
88106
class TestBartForwardNodesDoNotContain extends Test, Case {
89107
override predicate run(Qnit test) {
90108
if
@@ -110,16 +128,18 @@ class TestBartReverseNodesContain extends Test, Case {
110128
class TestBartReverseNodesState extends Test, Case {
111129
override predicate run(Qnit test) {
112130
if
113-
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
131+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
114132
rev.getName() = "Bart" and
115133
rev.getState() = "child"
116-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
134+
) and
135+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
117136
rev.getName() = "Homer" and
118137
rev.getState() = "parent"
119-
) and exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
138+
) and
139+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
120140
rev.getName() = "Grandpa" and
121141
rev.getState() = "grandparent"
122-
)
142+
)
123143
then test.pass("All reverse nodes from Bart have the correct state")
124144
else test.fail("Some reverse nodes from Bart have incorrect state")
125145
}
@@ -138,11 +158,13 @@ class TestBartReverseNodesDoNotContain extends Test, Case {
138158

139159
class TestBartToGrandpaHasPath extends Test, Case {
140160
override predicate run(Qnit test) {
141-
if exists(Person bart, Person grandpa |
161+
if
162+
exists(Person bart, Person grandpa |
142163
bart.getName() = "Bart" and
143164
grandpa.getName() = "Grandpa" and
144-
GraphPathStateSearch<Person, BartToGrandpaConfig>::hasPath(bart, "child", grandpa, "grandparent")
145-
)
165+
GraphPathStateSearch<Person, BartToGrandpaConfig>::hasPath(bart, "child", grandpa,
166+
"grandparent")
167+
)
146168
then test.pass("Path from Bart to Grandpa exists")
147169
else test.fail("Path from Bart to Grandpa does not exist")
148170
}
@@ -161,22 +183,27 @@ class TestGrandpaToBartForwardNodesContain extends Test, Case {
161183

162184
class TestGrandpaToBartForwardNodesState extends Test, Case {
163185
override predicate run(Qnit test) {
164-
if exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
186+
if
187+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
165188
fwd.getName() = "Grandpa" and
166189
fwd.getState() = "parent"
167-
) and exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
190+
) and
191+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
168192
fwd.getName() = "Homer" and
169193
fwd.getState() = "child"
170-
) and exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
194+
) and
195+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
171196
fwd.getName() = "Bart" and
172197
fwd.getState() = "grandchild"
173-
) and exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
198+
) and
199+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
174200
fwd.getName() = "Maggie" and
175201
fwd.getState() = "grandchild"
176-
) and exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
202+
) and
203+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
177204
fwd.getName() = "Lisa" and
178205
fwd.getState() = "grandchild"
179-
)
206+
)
180207
then test.pass("All forward nodes from Grandpa have the correct state")
181208
else test.fail("Some forward nodes from Grandpa have incorrect state")
182209
}
@@ -206,16 +233,19 @@ class TestGrandpaToBartReverseNodesContain extends Test, Case {
206233

207234
class TestGrandpaToBartReverseNodesState extends Test, Case {
208235
override predicate run(Qnit test) {
209-
if exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
236+
if
237+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
210238
rev.getName() = "Grandpa" and
211239
rev.getState() = "parent"
212-
) and exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
240+
) and
241+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
213242
rev.getName() = "Homer" and
214243
rev.getState() = "child"
215-
) and exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
244+
) and
245+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
216246
rev.getName() = "Bart" and
217247
rev.getState() = "grandchild"
218-
)
248+
)
219249
then test.pass("All reverse nodes from Grandpa have the correct state")
220250
else test.fail("Some reverse nodes from Grandpa have incorrect state")
221251
}
@@ -234,12 +264,14 @@ class TestGrandpaToBartReverseNodesDoNotContain extends Test, Case {
234264

235265
class TestGrandpaToBartHasPath extends Test, Case {
236266
override predicate run(Qnit test) {
237-
if exists(Person grandpa, Person bart |
267+
if
268+
exists(Person grandpa, Person bart |
238269
grandpa.getName() = "Grandpa" and
239270
bart.getName() = "Bart" and
240-
GraphPathStateSearch<Person, GrandpaToBartConfig>::hasPath(grandpa, "parent", bart, "grandchild")
241-
)
271+
GraphPathStateSearch<Person, GrandpaToBartConfig>::hasPath(grandpa, "parent", bart,
272+
"grandchild")
273+
)
242274
then test.pass("Path from Grandpa to Bart exists")
243275
else test.fail("Path from Grandpa to Bart does not exist")
244276
}
245-
}
277+
}

‎test/qtil/locations/CustomPathProblem/CustomPathStateProblemTest.ql‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
/**
2+
* @name Custom Path State Problem Example
3+
* @description This example demonstrates how to define a custom path problem in C++ using Qtil. It
4+
* identifies paths from top-level variables to constructors that are called during their
5+
* initialization. Additionally, it tracks the depth of the search as a state.
6+
* @id qtil-example-custom-path-problem
7+
* @severity info
8+
* @kind path-problem
9+
*/
10+
11+
import cpp
12+
import cpp as cpp
13+
import qtil.locations.Locatable
14+
import qtil.locations.CustomPathStateProblem
15+
import CustomPathStateProblemCpp
16+
17+
/** Defines cpp location behavior; this will be moved to qtil.cpp eventually. */
18+
module CustomPathStateProblemCpp {
19+
module ElementConfig implements LocatableConfig<Location> {
20+
class Locatable = cpp::Locatable;
21+
}
22+
23+
import PathStateProblem<Location, ElementConfig>
24+
}
25+
26+
/**
27+
* Defines a custom path problem configuration for identifying paths from top-level variables to
28+
* constructors that are called during their initialization.
29+
*/
30+
module CallGraphPathProblemConfig implements CustomPathStateProblemConfigSig {
31+
/**
32+
* Since we are tracking flow from variable initialization to constructor calls, that means the
33+
* nodes in our path problem will be variables (roots), function calls (edges), and constructors
34+
* (end nodes).
35+
*/
36+
class Node extends Locatable {
37+
Node() {
38+
this instanceof Function or this.(Variable).isTopLevel() or this instanceof FunctionCall
39+
}
40+
}
41+
42+
class State = int; // Track search depth
43+
44+
/** Start searching from variable nodes */
45+
predicate start(Node n, int depth) { n instanceof Variable and depth = 0 }
46+
47+
/** If we reach a constructor, we have identified "problematic" flow from a variable */
48+
bindingset[depth]
49+
predicate end(Node n, int depth) {
50+
exists(Function f, Class c |
51+
n = f and
52+
c.getAConstructor() = f
53+
)
54+
}
55+
56+
bindingset[depth1]
57+
bindingset[depth2]
58+
predicate edge(Node a, int depth1, Node b, int depth2) {
59+
depth2 = depth1 + 1 and
60+
(
61+
// Increment depth for each edge traversed
62+
// Add an edge from variables to the function calls in that variable's initializer.
63+
exists(Variable var, Expr initializer, FunctionCall fc |
64+
var.getInitializer().getExpr() = initializer and
65+
fc.getParent*() = initializer and
66+
a = var and
67+
b = fc
68+
)
69+
or
70+
// Supposing we have reached a function call to some function `mid()`, then the next step in
71+
// the path problem will be one of the function calls in `mid()`.
72+
exists(FunctionCall fc, Function mid, FunctionCall next |
73+
mid = fc.getTarget() and
74+
next.getEnclosingFunction() = mid and
75+
a = fc and
76+
b = next
77+
)
78+
or
79+
// Add an edge from function calls to constructors, which are the end nodes.
80+
exists(FunctionCall fc, Function endFunc |
81+
fc.getTarget() = endFunc and
82+
end(endFunc, 0) and
83+
a = fc and
84+
b = endFunc
85+
)
86+
)
87+
}
88+
}
89+
90+
// Import the custom path problem configuration and define the problem.
91+
//
92+
// This automaticall generates the `nodes` and `edges` predicates based on the configuration that
93+
// make the path traceable for users.
94+
import CustomPathStateProblem<CallGraphPathProblemConfig>
95+
96+
from Variable var, Function ctor, int depth
97+
where problem(var, _, ctor, depth) // This finds for paths from variables to constructors
98+
select var, var, ctor, "Initialization of variable $@ calls constructor $@ at depth " + depth, var,
99+
var.getName(), ctor, ctor.getName()

0 commit comments

Comments
 (0)