@@ -256,8 +256,9 @@ module VariableCapture {
256
256
private predicate closureFlowStep ( ControlFlow:: Nodes:: ExprNode e1 , ControlFlow:: Nodes:: ExprNode e2 ) {
257
257
e1 = LocalFlow:: getALastEvalNode ( e2 )
258
258
or
259
- exists ( Ssa:: Definition def |
260
- LocalFlow:: ssaDefAssigns ( def .getAnUltimateDefinition ( ) , e1 ) and
259
+ exists ( Ssa:: Definition def , AssignableDefinition adef |
260
+ LocalFlow:: defAssigns ( adef , _, e1 ) and
261
+ def .getAnUltimateDefinition ( ) .( Ssa:: ExplicitDefinition ) .getADefinition ( ) = adef and
261
262
exists ( def .getAReadAtNode ( e2 ) )
262
263
)
263
264
}
@@ -481,6 +482,30 @@ module VariableCapture {
481
482
}
482
483
}
483
484
485
+ /** Provides logic related to SSA. */
486
+ module SsaFlow {
487
+ private module Impl = SsaImpl:: DataFlowIntegration;
488
+
489
+ Impl:: Node asNode ( Node n ) {
490
+ n = TSsaNode ( result )
491
+ or
492
+ result .( Impl:: ExprNode ) .getExpr ( ) = n .( ExprNode ) .getControlFlowNode ( )
493
+ or
494
+ result .( Impl:: ExprPostUpdateNode ) .getExpr ( ) =
495
+ n .( PostUpdateNode ) .getPreUpdateNode ( ) .( ExprNode ) .getControlFlowNode ( )
496
+ or
497
+ TExplicitParameterNode ( result .( Impl:: ParameterNode ) .getParameter ( ) ) = n
498
+ }
499
+
500
+ predicate localFlowStep ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo , boolean isUseStep ) {
501
+ Impl:: localFlowStep ( def , asNode ( nodeFrom ) , asNode ( nodeTo ) , isUseStep )
502
+ }
503
+
504
+ predicate localMustFlowStep ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo ) {
505
+ Impl:: localMustFlowStep ( def , asNode ( nodeFrom ) , asNode ( nodeTo ) )
506
+ }
507
+ }
508
+
484
509
/** Provides predicates related to local data flow. */
485
510
module LocalFlow {
486
511
class LocalExprStepConfiguration extends ControlFlowReachabilityConfiguration {
@@ -606,105 +631,6 @@ module LocalFlow {
606
631
any ( LocalExprStepConfiguration x ) .hasDefPath ( _, value , def , cfnDef )
607
632
}
608
633
609
- predicate ssaDefAssigns ( Ssa:: ExplicitDefinition ssaDef , ControlFlow:: Nodes:: ExprNode value ) {
610
- exists ( AssignableDefinition def , ControlFlow:: Node cfnDef |
611
- any ( LocalExprStepConfiguration conf ) .hasDefPath ( _, value , def , cfnDef ) and
612
- ssaDef .getADefinition ( ) = def and
613
- ssaDef .getControlFlowNode ( ) = cfnDef
614
- )
615
- }
616
-
617
- /**
618
- * An uncertain SSA definition. Either an uncertain explicit definition or an
619
- * uncertain qualifier definition.
620
- *
621
- * Restricts `Ssa::UncertainDefinition` by excluding implicit call definitions,
622
- * as we---conservatively---consider such definitions to be certain.
623
- */
624
- class UncertainExplicitSsaDefinition extends Ssa:: UncertainDefinition {
625
- UncertainExplicitSsaDefinition ( ) {
626
- this instanceof Ssa:: ExplicitDefinition
627
- or
628
- this =
629
- any ( Ssa:: ImplicitQualifierDefinition qdef |
630
- qdef .getQualifierDefinition ( ) instanceof UncertainExplicitSsaDefinition
631
- )
632
- }
633
- }
634
-
635
- /** An SSA definition into which another SSA definition may flow. */
636
- private class SsaInputDefinitionExtNode extends SsaDefinitionExtNode {
637
- SsaInputDefinitionExtNode ( ) {
638
- def instanceof Ssa:: PhiNode
639
- or
640
- def instanceof SsaImpl:: PhiReadNode
641
- or
642
- def instanceof LocalFlow:: UncertainExplicitSsaDefinition
643
- }
644
- }
645
-
646
- /**
647
- * Holds if `nodeFrom` is a last node referencing SSA definition `def`, which
648
- * can reach `next`.
649
- */
650
- private predicate localFlowSsaInputFromDef (
651
- Node nodeFrom , SsaImpl:: DefinitionExt def , SsaInputDefinitionExtNode next
652
- ) {
653
- exists ( ControlFlow:: BasicBlock bb , int i |
654
- SsaImpl:: lastRefBeforeRedefExt ( def , bb , i , next .getDefinitionExt ( ) ) and
655
- def .definesAt ( _, bb , i , _) and
656
- def = getSsaDefinitionExt ( nodeFrom ) and
657
- nodeFrom != next
658
- )
659
- }
660
-
661
- /**
662
- * Holds if `read` is a last node reading SSA definition `def`, which
663
- * can reach `next`.
664
- */
665
- predicate localFlowSsaInputFromRead (
666
- Node read , SsaImpl:: DefinitionExt def , SsaInputDefinitionExtNode next
667
- ) {
668
- exists ( ControlFlow:: BasicBlock bb , int i |
669
- SsaImpl:: lastRefBeforeRedefExt ( def , bb , i , next .getDefinitionExt ( ) ) and
670
- read .asExprAtNode ( bb .getNode ( i ) ) instanceof AssignableRead
671
- )
672
- }
673
-
674
- private SsaImpl:: DefinitionExt getSsaDefinitionExt ( Node n ) {
675
- result = n .( SsaDefinitionExtNode ) .getDefinitionExt ( )
676
- or
677
- result = n .( ExplicitParameterNode ) .getSsaDefinition ( )
678
- }
679
-
680
- /**
681
- * Holds if there is a local use-use flow step from `nodeFrom` to `nodeTo`
682
- * involving SSA definition `def`.
683
- */
684
- predicate localSsaFlowStepUseUse ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo ) {
685
- exists ( ControlFlow:: Node cfnFrom , ControlFlow:: Node cfnTo |
686
- SsaImpl:: adjacentReadPairSameVarExt ( def , cfnFrom , cfnTo ) and
687
- nodeTo = TExprNode ( cfnTo ) and
688
- nodeFrom = TExprNode ( cfnFrom )
689
- )
690
- }
691
-
692
- /**
693
- * Holds if there is a local flow step from `nodeFrom` to `nodeTo` involving
694
- * SSA definition `def`.
695
- */
696
- predicate localSsaFlowStep ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo ) {
697
- // Flow from SSA definition/parameter to first read
698
- def = getSsaDefinitionExt ( nodeFrom ) and
699
- SsaImpl:: firstReadSameVarExt ( def , nodeTo .( ExprNode ) .getControlFlowNode ( ) )
700
- or
701
- // Flow from read to next read
702
- localSsaFlowStepUseUse ( def , nodeFrom .( PostUpdateNode ) .getPreUpdateNode ( ) , nodeTo )
703
- or
704
- // Flow into phi (read)/uncertain SSA definition node from def
705
- localFlowSsaInputFromDef ( nodeFrom , def , nodeTo )
706
- }
707
-
708
634
/**
709
635
* Holds if the source variable of SSA definition `def` is an instance field.
710
636
*/
@@ -788,10 +714,7 @@ module LocalFlow {
788
714
node2 .asExpr ( ) instanceof AssignExpr
789
715
)
790
716
or
791
- exists ( SsaImpl:: Definition def |
792
- def = getSsaDefinitionExt ( node1 ) and
793
- exists ( SsaImpl:: getAReadAtNode ( def , node2 .( ExprNode ) .getControlFlowNode ( ) ) )
794
- )
717
+ SsaFlow:: localMustFlowStep ( _, node1 , node2 )
795
718
or
796
719
node2 = node1 .( LocalFunctionCreationNode ) .getAnAccess ( true )
797
720
or
@@ -815,23 +738,14 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
815
738
(
816
739
LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
817
740
or
818
- exists ( SsaImpl:: DefinitionExt def |
741
+ exists ( SsaImpl:: DefinitionExt def , boolean isUseStep |
742
+ SsaFlow:: localFlowStep ( def , nodeFrom , nodeTo , isUseStep ) and
819
743
not LocalFlow:: usesInstanceField ( def ) and
820
744
not def instanceof VariableCapture:: CapturedSsaDefinitionExt
821
745
|
822
- LocalFlow:: localSsaFlowStep ( def , nodeFrom , nodeTo )
823
- or
824
- LocalFlow:: localSsaFlowStepUseUse ( def , nodeFrom , nodeTo ) and
825
- not FlowSummaryImpl:: Private:: Steps:: prohibitsUseUseFlow ( nodeFrom , _) and
826
- nodeFrom != nodeTo
746
+ isUseStep = false
827
747
or
828
- // Flow into phi (read)/uncertain SSA definition node from read
829
- exists ( Node read | LocalFlow:: localFlowSsaInputFromRead ( read , def , nodeTo ) |
830
- nodeFrom = read and
831
- not FlowSummaryImpl:: Private:: Steps:: prohibitsUseUseFlow ( nodeFrom , _)
832
- or
833
- nodeFrom .( PostUpdateNode ) .getPreUpdateNode ( ) = read
834
- )
748
+ not FlowSummaryImpl:: Private:: Steps:: prohibitsUseUseFlow ( nodeFrom , _)
835
749
)
836
750
or
837
751
nodeTo .( ObjectCreationNode ) .getPreUpdateNode ( ) = nodeFrom .( ObjectInitializerNode )
@@ -1097,10 +1011,7 @@ private module Cached {
1097
1011
cached
1098
1012
newtype TNode =
1099
1013
TExprNode ( ControlFlow:: Nodes:: ElementNode cfn ) { cfn .getAstNode ( ) instanceof Expr } or
1100
- TSsaDefinitionExtNode ( SsaImpl:: DefinitionExt def ) {
1101
- // Handled by `TExplicitParameterNode` below
1102
- not def instanceof Ssa:: ImplicitParameterDefinition
1103
- } or
1014
+ TSsaNode ( SsaImpl:: DataFlowIntegration:: SsaNode node ) or
1104
1015
TAssignableDefinitionNode ( AssignableDefinition def , ControlFlow:: Node cfn ) {
1105
1016
cfn = def .getExpr ( ) .getAControlFlowNode ( )
1106
1017
} or
@@ -1165,17 +1076,7 @@ private module Cached {
1165
1076
predicate localFlowStepImpl ( Node nodeFrom , Node nodeTo ) {
1166
1077
LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
1167
1078
or
1168
- LocalFlow:: localSsaFlowStepUseUse ( _, nodeFrom , nodeTo ) and
1169
- nodeFrom != nodeTo
1170
- or
1171
- LocalFlow:: localSsaFlowStep ( _, nodeFrom , nodeTo )
1172
- or
1173
- // Flow into phi (read)/uncertain SSA definition node from read
1174
- exists ( Node read | LocalFlow:: localFlowSsaInputFromRead ( read , _, nodeTo ) |
1175
- nodeFrom = read
1176
- or
1177
- nodeFrom .( PostUpdateNode ) .getPreUpdateNode ( ) = read
1178
- )
1079
+ SsaFlow:: localFlowStep ( _, nodeFrom , nodeTo , _)
1179
1080
or
1180
1081
// Simple flow through library code is included in the exposed local
1181
1082
// step relation, even though flow is technically inter-procedural
@@ -1239,7 +1140,7 @@ import Cached
1239
1140
1240
1141
/** Holds if `n` should be hidden from path explanations. */
1241
1142
predicate nodeIsHidden ( Node n ) {
1242
- n instanceof SsaDefinitionExtNode
1143
+ n instanceof SsaNode
1243
1144
or
1244
1145
exists ( Parameter p | p = n .( ParameterNode ) .getParameter ( ) | not p .fromSource ( ) )
1245
1146
or
@@ -1273,13 +1174,16 @@ predicate nodeIsHidden(Node n) {
1273
1174
n instanceof CaptureNode
1274
1175
}
1275
1176
1276
- /** An SSA definition, viewed as a node in a data flow graph. */
1277
- class SsaDefinitionExtNode extends NodeImpl , TSsaDefinitionExtNode {
1177
+ /** An SSA node. */
1178
+ abstract class SsaNode extends NodeImpl , TSsaNode {
1179
+ SsaImpl:: DataFlowIntegration:: SsaNode node ;
1278
1180
SsaImpl:: DefinitionExt def ;
1279
1181
1280
- SsaDefinitionExtNode ( ) { this = TSsaDefinitionExtNode ( def ) }
1182
+ SsaNode ( ) {
1183
+ this = TSsaNode ( node ) and
1184
+ def = node .getDefinitionExt ( )
1185
+ }
1281
1186
1282
- /** Gets the underlying SSA definition. */
1283
1187
SsaImpl:: DefinitionExt getDefinitionExt ( ) { result = def }
1284
1188
1285
1189
override DataFlowCallable getEnclosingCallableImpl ( ) {
@@ -1292,9 +1196,57 @@ class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
1292
1196
result = def .( Ssa:: Definition ) .getControlFlowNode ( )
1293
1197
}
1294
1198
1295
- override Location getLocationImpl ( ) { result = def .getLocation ( ) }
1199
+ override Location getLocationImpl ( ) { result = node .getLocation ( ) }
1296
1200
1297
- override string toStringImpl ( ) { result = def .toString ( ) }
1201
+ override string toStringImpl ( ) { result = node .toString ( ) }
1202
+ }
1203
+
1204
+ /** An (extended) SSA definition, viewed as a node in a data flow graph. */
1205
+ class SsaDefinitionExtNode extends SsaNode {
1206
+ override SsaImpl:: DataFlowIntegration:: SsaDefinitionExtNode node ;
1207
+ }
1208
+
1209
+ /**
1210
+ * A node that represents an input to an SSA phi (read) definition.
1211
+ *
1212
+ * This allows for barrier guards to filter input to phi nodes. For example, in
1213
+ *
1214
+ * ```csharp
1215
+ * var x = taint;
1216
+ * if (x != "safe")
1217
+ * {
1218
+ * x = "safe";
1219
+ * }
1220
+ * sink(x);
1221
+ * ```
1222
+ *
1223
+ * the `false` edge out of `x != "safe"` guards the input from `x = taint` into the
1224
+ * `phi` node after the condition.
1225
+ *
1226
+ * It is also relevant to filter input into phi read nodes:
1227
+ *
1228
+ * ```csharp
1229
+ * var x = taint;
1230
+ * if (b)
1231
+ * {
1232
+ * if (x != "safe1")
1233
+ * {
1234
+ * return;
1235
+ * }
1236
+ * } else {
1237
+ * if (x != "safe2")
1238
+ * {
1239
+ * return;
1240
+ * }
1241
+ * }
1242
+ *
1243
+ * sink(x);
1244
+ * ```
1245
+ *
1246
+ * both inputs into the phi read node after the outer condition are guarded.
1247
+ */
1248
+ class SsaInputNode extends SsaNode {
1249
+ override SsaImpl:: DataFlowIntegration:: SsaInputNode node ;
1298
1250
}
1299
1251
1300
1252
/** A definition, viewed as a node in a data flow graph. */
@@ -2844,7 +2796,7 @@ private predicate delegateCreationStep(Node nodeFrom, Node nodeTo) {
2844
2796
/** Extra data-flow steps needed for lambda flow analysis. */
2845
2797
predicate additionalLambdaFlowStep ( Node nodeFrom , Node nodeTo , boolean preservesValue ) {
2846
2798
exists ( SsaImpl:: DefinitionExt def |
2847
- LocalFlow :: localSsaFlowStep ( def , nodeFrom , nodeTo ) and
2799
+ SsaFlow :: localFlowStep ( def , nodeFrom , nodeTo , _ ) and
2848
2800
preservesValue = true
2849
2801
|
2850
2802
LocalFlow:: usesInstanceField ( def )
0 commit comments