@@ -29,6 +29,8 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
29
29
(
30
30
uninitializedWrite ( bb , i , v )
31
31
or
32
+ envVarWrite ( bb , i , v )
33
+ or
32
34
variableWriteActual ( bb , i , v , _)
33
35
or
34
36
exists ( ProcessBlockCfgNode processBlock | bb .getNode ( i ) = processBlock |
@@ -43,7 +45,11 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
43
45
}
44
46
45
47
predicate variableRead ( BasicBlock bb , int i , Variable v , boolean certain ) {
46
- variableReadActual ( bb , i , v ) and
48
+ (
49
+ variableReadActual ( bb , i , v )
50
+ or
51
+ envVarRead ( bb , i , v )
52
+ ) and
47
53
certain = true
48
54
}
49
55
}
@@ -66,6 +72,14 @@ predicate uninitializedWrite(Cfg::EntryBasicBlock bb, int i, Variable v) {
66
72
bb .getANode ( ) .getAstNode ( ) = v
67
73
}
68
74
75
+ predicate envVarWrite ( Cfg:: EntryBasicBlock bb , int i , EnvVariable v ) {
76
+ exists ( VarReadAccess va |
77
+ va .getVariable ( ) = v and
78
+ va .getEnclosingFunction ( ) .getBody ( ) = bb .getScope ( ) and
79
+ i = - 1
80
+ )
81
+ }
82
+
69
83
predicate parameterWrite ( Cfg:: EntryBasicBlock bb , int i , Parameter p ) {
70
84
bb .getNode ( i ) .getAstNode ( ) = p
71
85
}
@@ -78,6 +92,14 @@ private predicate variableReadActual(Cfg::BasicBlock bb, int i, Variable v) {
78
92
)
79
93
}
80
94
95
+ predicate envVarRead ( Cfg:: ExitBasicBlock bb , int i , EnvVariable v ) {
96
+ exists ( VarWriteAccess va |
97
+ va .getVariable ( ) = v and
98
+ va .getEnclosingFunction ( ) .getBody ( ) = bb .getScope ( ) and
99
+ bb .getNode ( i ) instanceof ExitNode
100
+ )
101
+ }
102
+
81
103
cached
82
104
private module Cached {
83
105
/**
@@ -165,7 +187,7 @@ private module Cached {
165
187
private predicate guardChecksAdjTypes (
166
188
DataFlowIntegrationInput:: Guard g , DataFlowIntegrationInput:: Expr e , boolean branch
167
189
) {
168
- guardChecks ( g , e , branch )
190
+ guardChecks ( g , e . asExprCfgNode ( ) , branch )
169
191
}
170
192
171
193
private Node getABarrierNodeImpl ( ) {
@@ -261,11 +283,48 @@ class ParameterExt extends TParameterExt {
261
283
}
262
284
263
285
private module DataFlowIntegrationInput implements Impl:: DataFlowIntegrationInputSig {
264
- class Expr extends Cfg:: CfgNodes:: ExprCfgNode {
265
- predicate hasCfgNode ( SsaInput:: BasicBlock bb , int i ) { this = bb .getNode ( i ) }
286
+ private newtype TExpr =
287
+ TExprCfgNode ( Cfg:: CfgNodes:: ExprCfgNode e ) or
288
+ TFinalEnvVarRead ( Scope scope , EnvVariable v ) {
289
+ exists ( Cfg:: ExitBasicBlock exit |
290
+ exit .getScope ( ) = scope and
291
+ envVarRead ( exit , _, v )
292
+ )
293
+ }
294
+
295
+ class Expr extends TExpr {
296
+ Cfg:: CfgNodes:: ExprCfgNode asExprCfgNode ( ) { this = TExprCfgNode ( result ) }
297
+
298
+ predicate isFinalEnvVarRead ( Scope scope , EnvVariable v ) { this = TFinalEnvVarRead ( scope , v ) }
299
+
300
+ predicate hasCfgNode ( SsaInput:: BasicBlock bb , int i ) {
301
+ this .asExprCfgNode ( ) = bb .getNode ( i )
302
+ or
303
+ exists ( EnvVariable v |
304
+ this .isFinalEnvVarRead ( bb .getScope ( ) , v ) and
305
+ bb .getNode ( i ) instanceof ExitNode
306
+ )
307
+ }
308
+
309
+ string toString ( ) {
310
+ result = this .asExprCfgNode ( ) .toString ( )
311
+ or
312
+ exists ( EnvVariable v |
313
+ this .isFinalEnvVarRead ( _, v ) and
314
+ result = v .toString ( )
315
+ )
316
+ }
266
317
}
267
318
268
- Expr getARead ( Definition def ) { result = Cached:: getARead ( def ) }
319
+ Expr getARead ( Definition def ) {
320
+ result .asExprCfgNode ( ) = Cached:: getARead ( def )
321
+ or
322
+ exists ( Variable v , Cfg:: BasicBlock bb , int i |
323
+ Impl:: ssaDefReachesRead ( v , def , bb , i ) and
324
+ envVarRead ( bb , i , v ) and
325
+ result .isFinalEnvVarRead ( bb .getScope ( ) , v )
326
+ )
327
+ }
269
328
270
329
predicate ssaDefHasSource ( WriteDefinition def ) {
271
330
any ( ParameterExt p ) .isInitializedBy ( def ) or def .( Ssa:: WriteDefinition ) .assigns ( _)
@@ -280,6 +339,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
280
339
predicate controlsBranchEdge ( SsaInput:: BasicBlock bb1 , SsaInput:: BasicBlock bb2 , boolean branch ) {
281
340
this .hasBranchEdge ( bb1 , bb2 , branch )
282
341
}
342
+
283
343
/**
284
344
* Holds if the evaluation of this guard to `branch` corresponds to the edge
285
345
* from `bb1` to `bb2`.
@@ -291,8 +351,6 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
291
351
s .getValue ( ) = branch
292
352
)
293
353
}
294
-
295
-
296
354
}
297
355
298
356
/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
0 commit comments