@@ -29,6 +29,8 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
2929 (
3030 uninitializedWrite ( bb , i , v )
3131 or
32+ envVarWrite ( bb , i , v )
33+ or
3234 variableWriteActual ( bb , i , v , _)
3335 or
3436 exists ( ProcessBlockCfgNode processBlock | bb .getNode ( i ) = processBlock |
@@ -43,7 +45,11 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
4345 }
4446
4547 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
4753 certain = true
4854 }
4955}
@@ -66,6 +72,14 @@ predicate uninitializedWrite(Cfg::EntryBasicBlock bb, int i, Variable v) {
6672 bb .getANode ( ) .getAstNode ( ) = v
6773}
6874
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+
6983predicate parameterWrite ( Cfg:: EntryBasicBlock bb , int i , Parameter p ) {
7084 bb .getNode ( i ) .getAstNode ( ) = p
7185}
@@ -78,6 +92,14 @@ private predicate variableReadActual(Cfg::BasicBlock bb, int i, Variable v) {
7892 )
7993}
8094
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+
81103cached
82104private module Cached {
83105 /**
@@ -165,7 +187,7 @@ private module Cached {
165187 private predicate guardChecksAdjTypes (
166188 DataFlowIntegrationInput:: Guard g , DataFlowIntegrationInput:: Expr e , boolean branch
167189 ) {
168- guardChecks ( g , e , branch )
190+ guardChecks ( g , e . asExprCfgNode ( ) , branch )
169191 }
170192
171193 private Node getABarrierNodeImpl ( ) {
@@ -261,11 +283,48 @@ class ParameterExt extends TParameterExt {
261283}
262284
263285private 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+ }
266317 }
267318
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+ }
269328
270329 predicate ssaDefHasSource ( WriteDefinition def ) {
271330 any ( ParameterExt p ) .isInitializedBy ( def ) or def .( Ssa:: WriteDefinition ) .assigns ( _)
@@ -280,6 +339,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
280339 predicate controlsBranchEdge ( SsaInput:: BasicBlock bb1 , SsaInput:: BasicBlock bb2 , boolean branch ) {
281340 this .hasBranchEdge ( bb1 , bb2 , branch )
282341 }
342+
283343 /**
284344 * Holds if the evaluation of this guard to `branch` corresponds to the edge
285345 * from `bb1` to `bb2`.
@@ -291,8 +351,6 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
291351 s .getValue ( ) = branch
292352 )
293353 }
294-
295-
296354 }
297355
298356 /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
0 commit comments