Skip to content

Commit cc1e33f

Browse files
paldepindpaldepind
authored
Merge pull request github#17713 from hvitved/rust/ssa
Rust: Initial SSA implementation
2 parents 25b592f + 6290be2 commit cc1e33f

File tree

9 files changed

+2030
-239
lines changed

9 files changed

+2030
-239
lines changed

‎rust/ql/consistency-queries/SsaConsistency.ql

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
import codeql.rust.dataflow.Ssa
2+
import codeql.rust.dataflow.internal.SsaImpl
3+
import Consistency
4+
5+
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
6+
override predicate hasLocationInfo(
7+
string filepath, int startline, int startcolumn, int endline, int endcolumn
8+
) {
9+
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
10+
}
11+
}
12+
13+
class MyRelevantDefinitionExt extends RelevantDefinitionExt, DefinitionExt {
14+
override predicate hasLocationInfo(
15+
string filepath, int startline, int startcolumn, int endline, int endcolumn
16+
) {
17+
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
18+
}
19+
}

‎rust/ql/lib/codeql/rust/dataflow/Ssa.qll

Lines changed: 340 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,340 @@
1+
/**
2+
* Provides the module `Ssa` for working with static single assignment (SSA) form.
3+
*/
4+
5+
/**
6+
* Provides classes for working with static single assignment (SSA) form.
7+
*/
8+
module Ssa {
9+
private import rust
10+
private import codeql.rust.controlflow.BasicBlocks
11+
private import codeql.rust.controlflow.ControlFlowGraph
12+
private import codeql.rust.controlflow.internal.ControlFlowGraphImpl as CfgImpl
13+
private import internal.SsaImpl as SsaImpl
14+
15+
class Variable = SsaImpl::SsaInput::SourceVariable;
16+
17+
/** A static single assignment (SSA) definition. */
18+
class Definition extends SsaImpl::Definition {
19+
/**
20+
* Gets the control flow node of this SSA definition, if any. Phi nodes are
21+
* examples of SSA definitions without a control flow node, as they are
22+
* modeled at index `-1` in the relevant basic block.
23+
*/
24+
final CfgNode getControlFlowNode() {
25+
exists(BasicBlock bb, int i | this.definesAt(_, bb, i) | result = bb.getNode(i))
26+
}
27+
28+
/**
29+
* Gets a control-flow node that reads the value of this SSA definition.
30+
*
31+
* Example:
32+
*
33+
* ```rust
34+
* fn phi(b : bool) { // defines b_0
35+
* let mut x = 1; // defines x_0
36+
* println!("{}", x); // reads x_0
37+
* println!("{}", x + 1); // reads x_0
38+
*
39+
* if b { // reads b_0
40+
* x = 2; // defines x_1
41+
* println!("{}", x); // reads x_1
42+
* println!("{}", x + 1); // reads x_1
43+
* } else {
44+
* x = 3; // defines x_2
45+
* println!("{}", x); // reads x_2
46+
* println!("{}", x + 1); // reads x_2
47+
* }
48+
* // defines x_3 = phi(x_1, x_2)
49+
* println!("{}", x); // reads x_3
50+
* }
51+
* ```
52+
*/
53+
final CfgNode getARead() { result = SsaImpl::getARead(this) }
54+
55+
/**
56+
* Gets a first control-flow node that reads the value of this SSA definition.
57+
* That is, a read that can be reached from this definition without passing
58+
* through other reads.
59+
*
60+
* Example:
61+
*
62+
* ```rust
63+
* fn phi(b : bool) { // defines b_0
64+
* let mut x = 1; // defines x_0
65+
* println!("{}", x); // first read of x_0
66+
* println!("{}", x + 1);
67+
*
68+
* if b { // first read of b_0
69+
* x = 2; // defines x_1
70+
* println!("{}", x); // first read of x_1
71+
* println!("{}", x + 1);
72+
* } else {
73+
* x = 3; // defines x_2
74+
* println!("{}", x); // first read of x_2
75+
* println!("{}", x + 1);
76+
* }
77+
* // defines x_3 = phi(x_1, x_2)
78+
* println!("{}", x); // first read of x_3
79+
* }
80+
* ```
81+
*/
82+
final CfgNode getAFirstRead() { SsaImpl::firstRead(this, result) }
83+
84+
/**
85+
* Gets a last control-flow node that reads the value of this SSA definition.
86+
* That is, a read that can reach the end of the enclosing CFG scope, or another
87+
* SSA definition for the source variable, without passing through any other read.
88+
*
89+
* Example:
90+
*
91+
* ```rust
92+
* fn phi(b : bool) { // defines b_0
93+
* let mut x = 1; // defines x_0
94+
* println!("{}", x);
95+
* println!("{}", x + 1); // last read of x_0
96+
*
97+
* if b { // last read of b_0
98+
* x = 2; // defines x_1
99+
* println!("{}", x);
100+
* println!("{}", x + 1); // last read of x_1
101+
* } else {
102+
* x = 3; // defines x_2
103+
* println!("{}", x);
104+
* println!("{}", x + 1); // last read of x_2
105+
* }
106+
* // defines x_3 = phi(x_1, x_2)
107+
* println!("{}", x); // last read of x_3
108+
* }
109+
* ```
110+
*/
111+
final CfgNode getALastRead() { SsaImpl::lastRead(this, result) }
112+
113+
/**
114+
* Holds if `read1` and `read2` are adjacent reads of this SSA definition.
115+
* That is, `read2` can be reached from `read1` without passing through
116+
* another read.
117+
*
118+
* Example:
119+
*
120+
* ```rust
121+
* fn phi(b : bool) {
122+
* let mut x = 1; // defines x_0
123+
* println!("{}", x); // reads x_0 (read1)
124+
* println!("{}", x + 1); // reads x_0 (read2)
125+
*
126+
* if b {
127+
* x = 2; // defines x_1
128+
* println!("{}", x); // reads x_1 (read1)
129+
* println!("{}", x + 1); // reads x_1 (read2)
130+
* } else {
131+
* x = 3; // defines x_2
132+
* println!("{}", x); // reads x_2 (read1)
133+
* println!("{}", x + 1); // reads x_2 (read2)
134+
* }
135+
* println!("{}", x);
136+
* }
137+
* ```
138+
*/
139+
final predicate hasAdjacentReads(CfgNode read1, CfgNode read2) {
140+
SsaImpl::adjacentReadPair(this, read1, read2)
141+
}
142+
143+
/**
144+
* Gets an SSA definition whose value can flow to this one in one step. This
145+
* includes inputs to phi nodes and the prior definitions of uncertain writes.
146+
*/
147+
private Definition getAPhiInputOrPriorDefinition() {
148+
result = this.(PhiDefinition).getAnInput()
149+
}
150+
151+
/**
152+
* Gets a definition that ultimately defines this SSA definition and is
153+
* not itself a phi node.
154+
*
155+
* Example:
156+
*
157+
* ```rust
158+
* fn phi(b : bool) {
159+
* let mut x = 1; // defines x_0
160+
* println!("{}", x);
161+
* println!("{}", x + 1);
162+
*
163+
* if b {
164+
* x = 2; // defines x_1
165+
* println!("{}", x);
166+
* println!("{}", x + 1);
167+
* } else {
168+
* x = 3; // defines x_2
169+
* println!("{}", x);
170+
* println!("{}", x + 1);
171+
* }
172+
* // defines x_3 = phi(x_1, x_2); ultimate definitions are x_1 and x_2
173+
* println!("{}", x);
174+
* }
175+
* ```
176+
*/
177+
final Definition getAnUltimateDefinition() {
178+
result = this.getAPhiInputOrPriorDefinition*() and
179+
not result instanceof PhiDefinition
180+
}
181+
182+
override string toString() { result = this.getControlFlowNode().toString() }
183+
184+
/** Gets the scope of this SSA definition. */
185+
CfgScope getScope() { result = this.getBasicBlock().getScope() }
186+
}
187+
188+
/**
189+
* An SSA definition that corresponds to a write. Example:
190+
*
191+
* ```rust
192+
* fn m(i : i64) { // writes `i`
193+
* let mut x = i; // writes `x`
194+
* x = 11; // writes `x`
195+
* }
196+
* ```
197+
*/
198+
class WriteDefinition extends Definition, SsaImpl::WriteDefinition {
199+
private CfgNode write;
200+
201+
WriteDefinition() {
202+
exists(BasicBlock bb, int i, Variable v |
203+
this.definesAt(v, bb, i) and
204+
SsaImpl::variableWriteActual(bb, i, v, write)
205+
)
206+
}
207+
208+
/** Gets the underlying write access. */
209+
final CfgNode getWriteAccess() { result = write }
210+
211+
/**
212+
* Holds if this SSA definition assigns `value` to the underlying variable.
213+
*
214+
* This is either a direct assignment, `x = value`, or an assignment via
215+
* simple pattern matching
216+
*
217+
* ```rb
218+
* case value
219+
* in Foo => x then ...
220+
* in y => then ...
221+
* end
222+
* ```
223+
*/
224+
predicate assigns(CfgNode value) {
225+
exists(AssignmentExpr ae, BasicBlock bb, int i |
226+
this.definesAt(_, bb, i) and
227+
ae.getLhs() = bb.getNode(i).getAstNode() and
228+
value.getAstNode() = ae.getRhs()
229+
)
230+
}
231+
232+
final override string toString() { result = write.toString() }
233+
234+
final override Location getLocation() { result = write.getLocation() }
235+
}
236+
237+
/**
238+
* A phi definition. For example, in
239+
*
240+
* ```rust
241+
* if b {
242+
* x = 0
243+
* } else {
244+
* x = 1
245+
* }
246+
* println!("{}", x);
247+
* ```
248+
*
249+
* a phi definition for `x` is inserted just before the call to `println!`.
250+
*/
251+
class PhiDefinition extends Definition, SsaImpl::PhiDefinition {
252+
/**
253+
* Gets an input of this phi definition.
254+
*
255+
* Example:
256+
*
257+
* ```rust
258+
* fn phi(b : bool) {
259+
* let mut x = 1; // defines x_0
260+
* println!("{}", x);
261+
* println!("{}", x + 1);
262+
*
263+
* if b {
264+
* x = 2; // defines x_1
265+
* println!("{}", x);
266+
* println!("{}", x + 1);
267+
* } else {
268+
* x = 3; // defines x_2
269+
* println!("{}", x);
270+
* println!("{}", x + 1);
271+
* }
272+
* // defines x_3 = phi(x_1, x_2); inputs are x_1 and x_2
273+
* println!("{}", x);
274+
* }
275+
* ```
276+
*/
277+
final Definition getAnInput() { this.hasInputFromBlock(result, _) }
278+
279+
/** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */
280+
predicate hasInputFromBlock(Definition inp, BasicBlock bb) {
281+
inp = SsaImpl::phiHasInputFromBlock(this, bb)
282+
}
283+
284+
private string getSplitString() {
285+
result = this.getBasicBlock().getFirstNode().(CfgImpl::AstCfgNode).getSplitsString()
286+
}
287+
288+
override string toString() {
289+
exists(string prefix |
290+
prefix = "[" + this.getSplitString() + "] "
291+
or
292+
not exists(this.getSplitString()) and
293+
prefix = ""
294+
|
295+
result = prefix + "phi"
296+
)
297+
}
298+
299+
/*
300+
* The location of a phi definition is the same as the location of the first node
301+
* in the basic block in which it is defined.
302+
*
303+
* Strictly speaking, the node is *before* the first node, but such a location
304+
* does not exist in the source program.
305+
*/
306+
307+
final override Location getLocation() {
308+
result = this.getBasicBlock().getFirstNode().getLocation()
309+
}
310+
}
311+
312+
/**
313+
* An SSA definition inserted at the beginning of a scope to represent a
314+
* captured local variable. For example, in
315+
*
316+
* ```rust
317+
* fn capture_immut() {
318+
* let x = 100;
319+
* let mut cap = || {
320+
* println!("{}", x);
321+
* };
322+
* cap();
323+
* }
324+
* ```
325+
*
326+
* an entry definition for `x` is inserted at the start of the CFG for `cap`.
327+
*/
328+
class CapturedEntryDefinition extends Definition, SsaImpl::WriteDefinition {
329+
CapturedEntryDefinition() {
330+
exists(BasicBlock bb, int i, Variable v |
331+
this.definesAt(v, bb, i) and
332+
SsaImpl::capturedEntryWrite(bb, i, v)
333+
)
334+
}
335+
336+
final override string toString() { result = "<captured entry> " + this.getSourceVariable() }
337+
338+
override Location getLocation() { result = this.getBasicBlock().getLocation() }
339+
}
340+
}

0 commit comments

Comments
 (0)