@@ -267,8 +267,9 @@ module VariableCapture {
267
267
private predicate closureFlowStep ( ControlFlow:: Nodes:: ExprNode e1 , ControlFlow:: Nodes:: ExprNode e2 ) {
268
268
e1 = LocalFlow:: getALastEvalNode ( e2 )
269
269
or
270
- exists ( Ssa:: Definition def |
271
- LocalFlow:: ssaDefAssigns ( def .getAnUltimateDefinition ( ) , e1 ) and
270
+ exists ( Ssa:: Definition def , AssignableDefinition adef |
271
+ LocalFlow:: defAssigns ( adef , _, e1 ) and
272
+ def .getAnUltimateDefinition ( ) .( Ssa:: ExplicitDefinition ) .getADefinition ( ) = adef and
272
273
exists ( def .getAReadAtNode ( e2 ) )
273
274
)
274
275
}
@@ -492,6 +493,30 @@ module VariableCapture {
492
493
}
493
494
}
494
495
496
+ /** Provides logic related to SSA. */
497
+ module SsaFlow {
498
+ private module Impl = SsaImpl:: DataFlowIntegration;
499
+
500
+ Impl:: Node asNode ( Node n ) {
501
+ n = TSsaNode ( result )
502
+ or
503
+ result .( Impl:: ExprNode ) .getExpr ( ) = n .( ExprNode ) .getControlFlowNode ( )
504
+ or
505
+ result .( Impl:: ExprPostUpdateNode ) .getExpr ( ) =
506
+ n .( PostUpdateNode ) .getPreUpdateNode ( ) .( ExprNode ) .getControlFlowNode ( )
507
+ or
508
+ result .( Impl:: ParameterNode ) .getParameter ( ) = n .( ExplicitParameterNode ) .getSsaDefinition ( )
509
+ }
510
+
511
+ predicate localFlowStep ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo , boolean isUseStep ) {
512
+ Impl:: localFlowStep ( def , asNode ( nodeFrom ) , asNode ( nodeTo ) , isUseStep )
513
+ }
514
+
515
+ predicate localMustFlowStep ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo ) {
516
+ Impl:: localMustFlowStep ( def , asNode ( nodeFrom ) , asNode ( nodeTo ) )
517
+ }
518
+ }
519
+
495
520
/** Provides predicates related to local data flow. */
496
521
module LocalFlow {
497
522
class LocalExprStepConfiguration extends ControlFlowReachabilityConfiguration {
@@ -617,105 +642,6 @@ module LocalFlow {
617
642
any ( LocalExprStepConfiguration x ) .hasDefPath ( _, value , def , cfnDef )
618
643
}
619
644
620
- predicate ssaDefAssigns ( Ssa:: ExplicitDefinition ssaDef , ControlFlow:: Nodes:: ExprNode value ) {
621
- exists ( AssignableDefinition def , ControlFlow:: Node cfnDef |
622
- any ( LocalExprStepConfiguration conf ) .hasDefPath ( _, value , def , cfnDef ) and
623
- ssaDef .getADefinition ( ) = def and
624
- ssaDef .getControlFlowNode ( ) = cfnDef
625
- )
626
- }
627
-
628
- /**
629
- * An uncertain SSA definition. Either an uncertain explicit definition or an
630
- * uncertain qualifier definition.
631
- *
632
- * Restricts `Ssa::UncertainDefinition` by excluding implicit call definitions,
633
- * as we---conservatively---consider such definitions to be certain.
634
- */
635
- class UncertainExplicitSsaDefinition extends Ssa:: UncertainDefinition {
636
- UncertainExplicitSsaDefinition ( ) {
637
- this instanceof Ssa:: ExplicitDefinition
638
- or
639
- this =
640
- any ( Ssa:: ImplicitQualifierDefinition qdef |
641
- qdef .getQualifierDefinition ( ) instanceof UncertainExplicitSsaDefinition
642
- )
643
- }
644
- }
645
-
646
- /** An SSA definition into which another SSA definition may flow. */
647
- private class SsaInputDefinitionExtNode extends SsaDefinitionExtNode {
648
- SsaInputDefinitionExtNode ( ) {
649
- def instanceof Ssa:: PhiNode
650
- or
651
- def instanceof SsaImpl:: PhiReadNode
652
- or
653
- def instanceof LocalFlow:: UncertainExplicitSsaDefinition
654
- }
655
- }
656
-
657
- /**
658
- * Holds if `nodeFrom` is a last node referencing SSA definition `def`, which
659
- * can reach `next`.
660
- */
661
- private predicate localFlowSsaInputFromDef (
662
- Node nodeFrom , SsaImpl:: DefinitionExt def , SsaInputDefinitionExtNode next
663
- ) {
664
- exists ( ControlFlow:: BasicBlock bb , int i |
665
- SsaImpl:: lastRefBeforeRedefExt ( def , bb , i , next .getDefinitionExt ( ) ) and
666
- def .definesAt ( _, bb , i , _) and
667
- def = getSsaDefinitionExt ( nodeFrom ) and
668
- nodeFrom != next
669
- )
670
- }
671
-
672
- /**
673
- * Holds if `read` is a last node reading SSA definition `def`, which
674
- * can reach `next`.
675
- */
676
- predicate localFlowSsaInputFromRead (
677
- Node read , SsaImpl:: DefinitionExt def , SsaInputDefinitionExtNode next
678
- ) {
679
- exists ( ControlFlow:: BasicBlock bb , int i |
680
- SsaImpl:: lastRefBeforeRedefExt ( def , bb , i , next .getDefinitionExt ( ) ) and
681
- read .asExprAtNode ( bb .getNode ( i ) ) instanceof AssignableRead
682
- )
683
- }
684
-
685
- private SsaImpl:: DefinitionExt getSsaDefinitionExt ( Node n ) {
686
- result = n .( SsaDefinitionExtNode ) .getDefinitionExt ( )
687
- or
688
- result = n .( ExplicitParameterNode ) .getSsaDefinition ( )
689
- }
690
-
691
- /**
692
- * Holds if there is a local use-use flow step from `nodeFrom` to `nodeTo`
693
- * involving SSA definition `def`.
694
- */
695
- predicate localSsaFlowStepUseUse ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo ) {
696
- exists ( ControlFlow:: Node cfnFrom , ControlFlow:: Node cfnTo |
697
- SsaImpl:: adjacentReadPairSameVarExt ( def , cfnFrom , cfnTo ) and
698
- nodeTo = TExprNode ( cfnTo ) and
699
- nodeFrom = TExprNode ( cfnFrom )
700
- )
701
- }
702
-
703
- /**
704
- * Holds if there is a local flow step from `nodeFrom` to `nodeTo` involving
705
- * SSA definition `def`.
706
- */
707
- predicate localSsaFlowStep ( SsaImpl:: DefinitionExt def , Node nodeFrom , Node nodeTo ) {
708
- // Flow from SSA definition/parameter to first read
709
- def = getSsaDefinitionExt ( nodeFrom ) and
710
- SsaImpl:: firstReadSameVarExt ( def , nodeTo .( ExprNode ) .getControlFlowNode ( ) )
711
- or
712
- // Flow from read to next read
713
- localSsaFlowStepUseUse ( def , nodeFrom .( PostUpdateNode ) .getPreUpdateNode ( ) , nodeTo )
714
- or
715
- // Flow into phi (read)/uncertain SSA definition node from def
716
- localFlowSsaInputFromDef ( nodeFrom , def , nodeTo )
717
- }
718
-
719
645
/**
720
646
* Holds if the source variable of SSA definition `def` is an instance field.
721
647
*/
@@ -800,10 +726,7 @@ module LocalFlow {
800
726
node2 .asExpr ( ) instanceof AssignExpr
801
727
)
802
728
or
803
- exists ( SsaImpl:: Definition def |
804
- def = getSsaDefinitionExt ( node1 ) and
805
- exists ( SsaImpl:: getAReadAtNode ( def , node2 .( ExprNode ) .getControlFlowNode ( ) ) )
806
- )
729
+ SsaFlow:: localMustFlowStep ( _, node1 , node2 )
807
730
or
808
731
node2 = node1 .( LocalFunctionCreationNode ) .getAnAccess ( true )
809
732
or
@@ -827,23 +750,15 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
827
750
(
828
751
LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
829
752
or
830
- exists ( SsaImpl:: DefinitionExt def |
753
+ exists ( SsaImpl:: DefinitionExt def , boolean isUseStep |
754
+ SsaFlow:: localFlowStep ( def , nodeFrom , nodeTo , isUseStep ) and
831
755
not LocalFlow:: usesInstanceField ( def ) and
832
756
not def instanceof VariableCapture:: CapturedSsaDefinitionExt
833
757
|
834
- LocalFlow:: localSsaFlowStep ( def , nodeFrom , nodeTo )
835
- or
836
- LocalFlow:: localSsaFlowStepUseUse ( def , nodeFrom , nodeTo ) and
837
- not FlowSummaryImpl:: Private:: Steps:: prohibitsUseUseFlow ( nodeFrom , _) and
838
- nodeFrom != nodeTo
758
+ isUseStep = false
839
759
or
840
- // Flow into phi (read)/uncertain SSA definition node from read
841
- exists ( Node read | LocalFlow:: localFlowSsaInputFromRead ( read , def , nodeTo ) |
842
- nodeFrom = read and
843
- not FlowSummaryImpl:: Private:: Steps:: prohibitsUseUseFlow ( nodeFrom , _)
844
- or
845
- nodeFrom .( PostUpdateNode ) .getPreUpdateNode ( ) = read
846
- )
760
+ isUseStep = true and
761
+ not FlowSummaryImpl:: Private:: Steps:: prohibitsUseUseFlow ( nodeFrom , _)
847
762
)
848
763
or
849
764
nodeTo .( ObjectCreationNode ) .getPreUpdateNode ( ) = nodeFrom .( ObjectInitializerNode )
@@ -1099,11 +1014,7 @@ private module Cached {
1099
1014
cached
1100
1015
newtype TNode =
1101
1016
TExprNode ( ControlFlow:: Nodes:: ElementNode cfn ) { cfn .getAstNode ( ) instanceof Expr } or
1102
- TSsaDefinitionExtNode ( SsaImpl:: DefinitionExt def ) {
1103
- // Handled by `TExplicitParameterNode` below
1104
- not def instanceof Ssa:: ImplicitParameterDefinition and
1105
- def .getBasicBlock ( ) = any ( DataFlowCallable c ) .getAControlFlowNode ( ) .getBasicBlock ( )
1106
- } or
1017
+ TSsaNode ( SsaImpl:: DataFlowIntegration:: SsaNode node ) or
1107
1018
TAssignableDefinitionNode ( AssignableDefinition def , ControlFlow:: Node cfn ) {
1108
1019
cfn = def .getExpr ( ) .getAControlFlowNode ( )
1109
1020
} or
@@ -1166,17 +1077,7 @@ private module Cached {
1166
1077
predicate localFlowStepImpl ( Node nodeFrom , Node nodeTo ) {
1167
1078
LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
1168
1079
or
1169
- LocalFlow:: localSsaFlowStepUseUse ( _, nodeFrom , nodeTo ) and
1170
- nodeFrom != nodeTo
1171
- or
1172
- LocalFlow:: localSsaFlowStep ( _, nodeFrom , nodeTo )
1173
- or
1174
- // Flow into phi (read)/uncertain SSA definition node from read
1175
- exists ( Node read | LocalFlow:: localFlowSsaInputFromRead ( read , _, nodeTo ) |
1176
- nodeFrom = read
1177
- or
1178
- nodeFrom .( PostUpdateNode ) .getPreUpdateNode ( ) = read
1179
- )
1080
+ SsaFlow:: localFlowStep ( _, nodeFrom , nodeTo , _)
1180
1081
or
1181
1082
// Simple flow through library code is included in the exposed local
1182
1083
// step relation, even though flow is technically inter-procedural
@@ -1245,7 +1146,7 @@ import Cached
1245
1146
1246
1147
/** Holds if `n` should be hidden from path explanations. */
1247
1148
predicate nodeIsHidden ( Node n ) {
1248
- n instanceof SsaDefinitionExtNode
1149
+ n instanceof SsaNode
1249
1150
or
1250
1151
exists ( Parameter p | p = n .( ParameterNode ) .getParameter ( ) | not p .fromSource ( ) )
1251
1152
or
@@ -1279,13 +1180,16 @@ predicate nodeIsHidden(Node n) {
1279
1180
n instanceof CaptureNode
1280
1181
}
1281
1182
1282
- /** An SSA definition, viewed as a node in a data flow graph. */
1283
- class SsaDefinitionExtNode extends NodeImpl , TSsaDefinitionExtNode {
1183
+ /** An SSA node. */
1184
+ abstract class SsaNode extends NodeImpl , TSsaNode {
1185
+ SsaImpl:: DataFlowIntegration:: SsaNode node ;
1284
1186
SsaImpl:: DefinitionExt def ;
1285
1187
1286
- SsaDefinitionExtNode ( ) { this = TSsaDefinitionExtNode ( def ) }
1188
+ SsaNode ( ) {
1189
+ this = TSsaNode ( node ) and
1190
+ def = node .getDefinitionExt ( )
1191
+ }
1287
1192
1288
- /** Gets the underlying SSA definition. */
1289
1193
SsaImpl:: DefinitionExt getDefinitionExt ( ) { result = def }
1290
1194
1291
1195
override DataFlowCallable getEnclosingCallableImpl ( ) {
@@ -1298,9 +1202,57 @@ class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
1298
1202
result = def .( Ssa:: Definition ) .getControlFlowNode ( )
1299
1203
}
1300
1204
1301
- override Location getLocationImpl ( ) { result = def .getLocation ( ) }
1205
+ override Location getLocationImpl ( ) { result = node .getLocation ( ) }
1302
1206
1303
- override string toStringImpl ( ) { result = def .toString ( ) }
1207
+ override string toStringImpl ( ) { result = node .toString ( ) }
1208
+ }
1209
+
1210
+ /** An (extended) SSA definition, viewed as a node in a data flow graph. */
1211
+ class SsaDefinitionExtNode extends SsaNode {
1212
+ override SsaImpl:: DataFlowIntegration:: SsaDefinitionExtNode node ;
1213
+ }
1214
+
1215
+ /**
1216
+ * A node that represents an input to an SSA phi (read) definition.
1217
+ *
1218
+ * This allows for barrier guards to filter input to phi nodes. For example, in
1219
+ *
1220
+ * ```csharp
1221
+ * var x = taint;
1222
+ * if (x != "safe")
1223
+ * {
1224
+ * x = "safe";
1225
+ * }
1226
+ * sink(x);
1227
+ * ```
1228
+ *
1229
+ * the `false` edge out of `x != "safe"` guards the input from `x = taint` into the
1230
+ * `phi` node after the condition.
1231
+ *
1232
+ * It is also relevant to filter input into phi read nodes:
1233
+ *
1234
+ * ```csharp
1235
+ * var x = taint;
1236
+ * if (b)
1237
+ * {
1238
+ * if (x != "safe1")
1239
+ * {
1240
+ * return;
1241
+ * }
1242
+ * } else {
1243
+ * if (x != "safe2")
1244
+ * {
1245
+ * return;
1246
+ * }
1247
+ * }
1248
+ *
1249
+ * sink(x);
1250
+ * ```
1251
+ *
1252
+ * both inputs into the phi read node after the outer condition are guarded.
1253
+ */
1254
+ class SsaInputNode extends SsaNode {
1255
+ override SsaImpl:: DataFlowIntegration:: SsaInputNode node ;
1304
1256
}
1305
1257
1306
1258
/** A definition, viewed as a node in a data flow graph. */
@@ -2946,7 +2898,7 @@ private predicate delegateCreationStep(Node nodeFrom, Node nodeTo) {
2946
2898
/** Extra data-flow steps needed for lambda flow analysis. */
2947
2899
predicate additionalLambdaFlowStep ( Node nodeFrom , Node nodeTo , boolean preservesValue ) {
2948
2900
exists ( SsaImpl:: DefinitionExt def |
2949
- LocalFlow :: localSsaFlowStep ( def , nodeFrom , nodeTo ) and
2901
+ SsaFlow :: localFlowStep ( def , nodeFrom , nodeTo , _ ) and
2950
2902
preservesValue = true
2951
2903
|
2952
2904
LocalFlow:: usesInstanceField ( def )
0 commit comments