Skip to content

Commit 6054855

Browse files
paldepindpaldepind
authored
Merge pull request #17888 from paldepind/rust-data-flow-consistency
Rust: Data flow additions
2 parents bb5ee52 + 262a9f0 commit 6054855

File tree

7 files changed

+297
-15
lines changed

7 files changed

+297
-15
lines changed

‎rust/ql/lib/codeql/rust/controlflow/CfgNodes.qll‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/**
2+
* Provides subclasses of `CfgNode` that represents different types of nodes in
3+
* the control flow graph.
4+
*/
5+
6+
private import rust
7+
private import ControlFlowGraph
8+
9+
/** A CFG node that corresponds to an element in the AST. */
10+
class AstCfgNode extends CfgNode {
11+
AstNode node;
12+
13+
AstCfgNode() { node = this.getAstNode() }
14+
}
15+
16+
/** A CFG node that corresponds to an expression in the AST. */
17+
class ExprCfgNode extends AstCfgNode {
18+
override Expr node;
19+
20+
/** Gets the underlying expression. */
21+
Expr getExpr() { result = node }
22+
}

‎rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll‎

Lines changed: 125 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,9 @@ private import codeql.util.Unit
77
private import codeql.dataflow.DataFlow
88
private import codeql.dataflow.internal.DataFlowImpl
99
private import rust
10+
private import SsaImpl as SsaImpl
1011
private import codeql.rust.controlflow.ControlFlowGraph
12+
private import codeql.rust.controlflow.CfgNodes
1113
private import codeql.rust.dataflow.Ssa
1214

1315
module Node {
@@ -52,22 +54,67 @@ module Node {
5254
override Location getLocation() { none() }
5355
}
5456

57+
/**
58+
* A node in the data flow graph that corresponds to an expression in the
59+
* AST.
60+
*
61+
* Note that because of control-flow splitting, one `Expr` may correspond
62+
* to multiple `ExprNode`s, just like it may correspond to multiple
63+
* `ControlFlow::Node`s.
64+
*/
65+
final class ExprNode extends Node, TExprNode {
66+
ExprCfgNode n;
67+
68+
ExprNode() { this = TExprNode(n) }
69+
70+
override Location getLocation() { result = n.getExpr().getLocation() }
71+
72+
override string toString() { result = n.getExpr().toString() }
73+
74+
override Expr asExpr() { result = n.getExpr() }
75+
76+
override CfgNode getCfgNode() { result = n }
77+
}
78+
5579
/**
5680
* The value of a parameter at function entry, viewed as a node in a data
5781
* flow graph.
5882
*/
59-
final class ParameterNode extends Node {
60-
Param param;
83+
final class ParameterNode extends Node, TParameterNode {
84+
Param parameter;
85+
86+
ParameterNode() { this = TParameterNode(parameter) }
6187

62-
ParameterNode() { this = TSourceParameterNode(param) }
88+
override Location getLocation() { result = parameter.getLocation() }
6389

64-
override Location getLocation() { result = param.getLocation() }
90+
override string toString() { result = parameter.toString() }
6591

66-
override string toString() { result = param.toString() }
92+
/** Gets the parameter in the AST that this node corresponds to. */
93+
Param getParameter() { result = parameter }
6794
}
6895

6996
final class ArgumentNode = NaNode;
7097

98+
/** An SSA node. */
99+
class SsaNode extends Node, TSsaNode {
100+
SsaImpl::DataFlowIntegration::SsaNode node;
101+
SsaImpl::DefinitionExt def;
102+
103+
SsaNode() {
104+
this = TSsaNode(node) and
105+
def = node.getDefinitionExt()
106+
}
107+
108+
SsaImpl::DefinitionExt getDefinitionExt() { result = def }
109+
110+
/** Holds if this node should be hidden from path explanations. */
111+
abstract predicate isHidden();
112+
113+
override Location getLocation() { result = node.getLocation() }
114+
115+
override string toString() { result = node.toString() }
116+
}
117+
71118
final class ReturnNode extends NaNode {
72119
RustDataFlow::ReturnKind getKind() { none() }
73120
}
@@ -93,6 +140,64 @@ module Node {
93140
final class CastNode = NaNode;
94141
}
95142

143+
final class Node = Node::Node;
144+
145+
/** Provides logic related to SSA. */
146+
module SsaFlow {
147+
private module Impl = SsaImpl::DataFlowIntegration;
148+
149+
private Node::ParameterNode toParameterNode(Param p) { result = TParameterNode(p) }
150+
151+
/** Converts a control flow node into an SSA control flow node. */
152+
Impl::Node asNode(Node n) {
153+
n = TSsaNode(result)
154+
or
155+
result.(Impl::ExprNode).getExpr() = n.(Node::ExprNode).getCfgNode()
156+
or
157+
n = toParameterNode(result.(Impl::ParameterNode).getParameter())
158+
}
159+
160+
predicate localFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep) {
161+
Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo), isUseStep)
162+
}
163+
164+
predicate localMustFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
165+
Impl::localMustFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
166+
}
167+
}
168+
169+
/**
170+
* Holds for expressions `e` that evaluate to the value of any last (in
171+
* evaluation order) subexpressions within it. E.g., expressions that propagate
172+
* a values from a subexpression.
173+
*
174+
* For instance, the predicate holds for if expressions as `if b { e1 } else {
175+
* e2 }` evalates to the value of one of the subexpressions `e1` or `e2`.
176+
*/
177+
private predicate propagatesValue(Expr e) {
178+
e instanceof IfExpr or
179+
e instanceof LoopExpr or
180+
e instanceof ReturnExpr or
181+
e instanceof BreakExpr or
182+
e.(BlockExpr).getStmtList().hasTailExpr() or
183+
e instanceof MatchExpr
184+
}
185+
186+
/**
187+
* Gets a node that may execute last in `n`, and which, when it executes last,
188+
* will be the value of `n`.
189+
*/
190+
private ExprCfgNode getALastEvalNode(ExprCfgNode n) {
191+
propagatesValue(n.getExpr()) and result.getASuccessor() = n
192+
}
193+
194+
module LocalFlow {
195+
pragma[nomagic]
196+
predicate localFlowStepCommon(Node nodeFrom, Node nodeTo) {
197+
nodeFrom.getCfgNode() = getALastEvalNode(nodeTo.getCfgNode())
198+
}
199+
}
200+
96201
module RustDataFlow implements InputSig<Location> {
97202
/**
98203
* An element, viewed as a node in a data flow graph. Either an expression
@@ -122,10 +227,10 @@ module RustDataFlow implements InputSig<Location> {
122227

123228
predicate nodeIsHidden(Node node) { none() }
124229

125-
class DataFlowExpr = Void;
230+
class DataFlowExpr = ExprCfgNode;
126231

127232
/** Gets the node corresponding to `e`. */
128-
Node exprNode(DataFlowExpr e) { none() }
233+
Node exprNode(DataFlowExpr e) { result.getCfgNode() = e }
129234

130235
final class DataFlowCall extends TNormalCall {
131236
private CallExpr c;
@@ -191,7 +296,7 @@ module RustDataFlow implements InputSig<Location> {
191296
* Holds if there is a simple local flow step from `node1` to `node2`. These
192297
* are the value-preserving intra-callable flow steps.
193298
*/
194-
predicate simpleLocalFlowStep(Node node1, Node node2, string model) { none() }
299+
predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) { none() }
195300

196301
/**
197302
* Holds if data can flow from `node1` to `node2` through a non-local step
@@ -256,7 +361,9 @@ module RustDataFlow implements InputSig<Location> {
256361
* `node2` must be visited along a flow path, then any type known for `node2`
257362
* must also apply to `node1`.
258363
*/
259-
predicate localMustFlowStep(Node node1, Node node2) { none() }
364+
predicate localMustFlowStep(Node node1, Node node2) {
365+
SsaFlow::localMustFlowStep(_, node1, node2)
366+
}
260367

261368
class LambdaCallKind = Void;
262369

@@ -267,7 +374,7 @@ module RustDataFlow implements InputSig<Location> {
267374
/** Holds if `call` is a lambda call of kind `kind` where `receiver` is the lambda expression. */
268375
predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver) { none() }
269376

270-
/** Extra data-flow steps needed for lambda flow analysis. */
377+
/** Extra data flow steps needed for lambda flow analysis. */
271378
predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) { none() }
272379

273380
predicate knownSourceModel(Node source, string model) { none() }
@@ -286,8 +393,9 @@ cached
286393
private module Cached {
287394
cached
288395
newtype TNode =
289-
TExprNode(CfgNode n, Expr e) { n.getAstNode() = e } or
290-
TSourceParameterNode(Param param)
396+
TExprNode(ExprCfgNode n) or
397+
TParameterNode(Param p) or
398+
TSsaNode(SsaImpl::DataFlowIntegration::SsaNode node)
291399

292400
cached
293401
newtype TDataFlowCall = TNormalCall(CallExpr c)
@@ -302,7 +410,11 @@ private module Cached {
302410

303411
/** This is the local flow predicate that is exposed. */
304412
cached
305-
predicate localFlowStepImpl(Node::Node nodeFrom, Node::Node nodeTo) { none() }
413+
predicate localFlowStepImpl(Node::Node nodeFrom, Node::Node nodeTo) {
414+
LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
415+
or
416+
SsaFlow::localFlowStep(_, nodeFrom, nodeTo, _)
417+
}
306418
}
307419

308420
import Cached

‎rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ private import rust
22
private import codeql.rust.controlflow.BasicBlocks as BasicBlocks
33
private import BasicBlocks
44
private import codeql.rust.controlflow.ControlFlowGraph as Cfg
5+
private import codeql.rust.controlflow.CfgNodes as CfgNodes
56
private import Cfg
67
private import codeql.rust.controlflow.internal.ControlFlowGraphImpl as ControlFlowGraphImpl
78
private import codeql.ssa.Ssa as SsaImplCommon
@@ -395,6 +396,38 @@ private module Cached {
395396
Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
396397
Impl::uncertainWriteDefinitionInput(def, result)
397398
}
399+
400+
cached
401+
module DataFlowIntegration {
402+
import DataFlowIntegrationImpl
403+
404+
cached
405+
predicate localFlowStep(DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep) {
406+
DataFlowIntegrationImpl::localFlowStep(def, nodeFrom, nodeTo, isUseStep)
407+
}
408+
409+
cached
410+
predicate localMustFlowStep(DefinitionExt def, Node nodeFrom, Node nodeTo) {
411+
DataFlowIntegrationImpl::localMustFlowStep(def, nodeFrom, nodeTo)
412+
}
413+
414+
signature predicate guardChecksSig(CfgNodes::AstCfgNode g, Cfg::CfgNode e, boolean branch);
415+
416+
cached // nothing is actually cached
417+
module BarrierGuard<guardChecksSig/3 guardChecks> {
418+
private predicate guardChecksAdjTypes(
419+
DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
420+
) {
421+
guardChecks(g, e, branch)
422+
}
423+
424+
private Node getABarrierNodeImpl() {
425+
result = DataFlowIntegrationImpl::BarrierGuard<guardChecksAdjTypes/3>::getABarrierNode()
426+
}
427+
428+
predicate getABarrierNode = getABarrierNodeImpl/0;
429+
}
430+
}
398431
}
399432

400433
import Cached
@@ -426,3 +459,46 @@ class PhiReadNode extends DefinitionExt, Impl::PhiReadNode {
426459

427460
override Location getLocation() { result = Impl::PhiReadNode.super.getLocation() }
428461
}
462+
463+
private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
464+
class Expr extends CfgNodes::AstCfgNode {
465+
predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this = bb.getNode(i) }
466+
}
467+
468+
Expr getARead(Definition def) { result = Cached::getARead(def) }
469+
470+
/** Holds if SSA definition `def` assigns `value` to the underlying variable. */
471+
predicate ssaDefAssigns(WriteDefinition def, Expr value) {
472+
exists(BasicBlock bb, int i | def.definesAt(_, bb, i) and value = bb.getNode(i))
473+
}
474+
475+
class Parameter = Param;
476+
477+
/** Holds if SSA definition `def` initializes parameter `p` at function entry. */
478+
predicate ssaDefInitializesParam(WriteDefinition def, Parameter p) {
479+
exists(BasicBlock bb, int i | bb.getNode(i).getAstNode() = p and def.definesAt(_, bb, i))
480+
}
481+
482+
class Guard extends CfgNodes::AstCfgNode {
483+
predicate hasCfgNode(SsaInput::BasicBlock bb, int i) { this = bb.getNode(i) }
484+
}
485+
486+
/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
487+
predicate guardControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {
488+
exists(ConditionBlock conditionBlock, ConditionalSuccessor s |
489+
guard = conditionBlock.getLastNode() and
490+
s.getValue() = branch and
491+
conditionBlock.controls(bb, s)
492+
)
493+
}
494+
495+
/** Gets an immediate conditional successor of basic block `bb`, if any. */
496+
SsaInput::BasicBlock getAConditionalBasicBlockSuccessor(SsaInput::BasicBlock bb, boolean branch) {
497+
exists(Cfg::ConditionalSuccessor s |
498+
result = bb.getASuccessor(s) and
499+
s.getValue() = branch
500+
)
501+
}
502+
}
503+
504+
private module DataFlowIntegrationImpl = Impl::DataFlowIntegration<DataFlowIntegrationInput>;

‎rust/ql/test/extractor-tests/generated/MacroItems/CONSISTENCY/DataFlowConsistency.expected‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,10 @@ uniqueType
55
| common_definitions.rs:3:15:3:25 | Param | Node should have one type but has 0. |
66
| file://:0:0:0:0 | Param | Node should have one type but has 0. |
77
uniqueNodeLocation
8+
| file://:0:0:0:0 | BlockExpr | Node should have one location but has 0. |
9+
| file://:0:0:0:0 | MethodCallExpr | Node should have one location but has 0. |
10+
| file://:0:0:0:0 | MethodCallExpr | Node should have one location but has 0. |
811
| file://:0:0:0:0 | Param | Node should have one location but has 0. |
12+
| file://:0:0:0:0 | PathExpr | Node should have one location but has 0. |
913
missingLocation
10-
| Nodes without location: 1 |
14+
| Nodes without location: 5 |

‎rust/ql/test/library-tests/dataflow/local/CONSISTENCY/DataFlowConsistency.expected‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,14 @@
1+
uniqueEnclosingCallable
2+
| main.rs:6:18:6:27 | Param | Node should have one enclosing callable but has 0. |
3+
| main.rs:31:21:31:26 | Param | Node should have one enclosing callable but has 0. |
4+
| main.rs:31:29:31:34 | Param | Node should have one enclosing callable but has 0. |
5+
| main.rs:31:37:31:50 | Param | Node should have one enclosing callable but has 0. |
16
uniqueCallEnclosingCallable
27
| main.rs:3:14:3:33 | CallExpr | Call should have one enclosing callable but has 0. |
3-
| main.rs:7:5:7:14 | CallExpr | Call should have one enclosing callable but has 0. |
8+
| main.rs:39:5:39:14 | CallExpr | Call should have one enclosing callable but has 0. |
9+
| main.rs:40:5:40:23 | CallExpr | Call should have one enclosing callable but has 0. |
10+
uniqueType
11+
| main.rs:6:18:6:27 | Param | Node should have one type but has 0. |
12+
| main.rs:31:21:31:26 | Param | Node should have one type but has 0. |
13+
| main.rs:31:29:31:34 | Param | Node should have one type but has 0. |
14+
| main.rs:31:37:31:50 | Param | Node should have one type but has 0. |

‎rust/ql/test/library-tests/dataflow/local/DataFlowStep.expected‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
| main.rs:2:9:2:9 | s | main.rs:3:33:3:33 | s |
2+
| main.rs:6:18:6:21 | cond | main.rs:9:16:9:19 | cond |
3+
| main.rs:7:9:7:9 | a | main.rs:10:9:10:9 | a |
4+
| main.rs:8:9:8:9 | b | main.rs:12:9:12:9 | b |
5+
| main.rs:9:9:9:9 | c | main.rs:14:5:14:5 | c |
6+
| main.rs:9:21:11:5 | BlockExpr | main.rs:9:13:13:5 | IfExpr |
7+
| main.rs:10:9:10:9 | a | main.rs:9:21:11:5 | BlockExpr |
8+
| main.rs:11:12:13:5 | BlockExpr | main.rs:9:13:13:5 | IfExpr |
9+
| main.rs:12:9:12:9 | b | main.rs:11:12:13:5 | BlockExpr |
10+
| main.rs:14:5:14:5 | c | main.rs:6:37:15:1 | BlockExpr |
11+
| main.rs:18:9:18:9 | a | main.rs:20:15:20:15 | a |
12+
| main.rs:19:9:19:9 | b | main.rs:22:5:22:5 | b |
13+
| main.rs:20:9:20:15 | BreakExpr | main.rs:19:13:21:5 | LoopExpr |
14+
| main.rs:20:15:20:15 | a | main.rs:20:9:20:15 | BreakExpr |
15+
| main.rs:22:5:22:5 | b | main.rs:17:29:23:1 | BlockExpr |
16+
| main.rs:27:5:27:5 | i | main.rs:27:5:27:5 | i |
17+
| main.rs:27:5:27:5 | i | main.rs:28:5:28:5 | i |
18+
| main.rs:28:5:28:5 | i | main.rs:25:24:29:1 | BlockExpr |
19+
| main.rs:31:21:31:21 | a | main.rs:33:20:33:20 | a |
20+
| main.rs:31:29:31:29 | b | main.rs:34:17:34:17 | b |
21+
| main.rs:31:37:31:37 | c | main.rs:32:11:32:11 | c |
22+
| main.rs:32:5:35:5 | MatchExpr | main.rs:31:60:36:1 | BlockExpr |
23+
| main.rs:33:20:33:20 | a | main.rs:32:5:35:5 | MatchExpr |
24+
| main.rs:34:17:34:17 | b | main.rs:32:5:35:5 | MatchExpr |

0 commit comments

Comments
 (0)