@@ -267,8 +267,9 @@ module VariableCapture {
267267 private predicate closureFlowStep ( ControlFlow:: Nodes:: ExprNode e1 , ControlFlow:: Nodes:: ExprNode e2 ) {
268268 e1 = LocalFlow:: getALastEvalNode ( e2 )
269269 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
272273 exists ( def .getAReadAtNode ( e2 ) )
273274 )
274275 }
@@ -492,6 +493,30 @@ module VariableCapture {
492493 }
493494}
494495
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+
495520/** Provides predicates related to local data flow. */
496521module LocalFlow {
497522 class LocalExprStepConfiguration extends ControlFlowReachabilityConfiguration {
@@ -617,105 +642,6 @@ module LocalFlow {
617642 any ( LocalExprStepConfiguration x ) .hasDefPath ( _, value , def , cfnDef )
618643 }
619644
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-
719645 /**
720646 * Holds if the source variable of SSA definition `def` is an instance field.
721647 */
@@ -800,10 +726,7 @@ module LocalFlow {
800726 node2 .asExpr ( ) instanceof AssignExpr
801727 )
802728 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 )
807730 or
808731 node2 = node1 .( LocalFunctionCreationNode ) .getAnAccess ( true )
809732 or
@@ -827,23 +750,15 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
827750 (
828751 LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
829752 or
830- exists ( SsaImpl:: DefinitionExt def |
753+ exists ( SsaImpl:: DefinitionExt def , boolean isUseStep |
754+ SsaFlow:: localFlowStep ( def , nodeFrom , nodeTo , isUseStep ) and
831755 not LocalFlow:: usesInstanceField ( def ) and
832756 not def instanceof VariableCapture:: CapturedSsaDefinitionExt
833757 |
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
839759 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 , _)
847762 )
848763 or
849764 nodeTo .( ObjectCreationNode ) .getPreUpdateNode ( ) = nodeFrom .( ObjectInitializerNode )
@@ -1099,11 +1014,7 @@ private module Cached {
10991014 cached
11001015 newtype TNode =
11011016 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
11071018 TAssignableDefinitionNode ( AssignableDefinition def , ControlFlow:: Node cfn ) {
11081019 cfn = def .getExpr ( ) .getAControlFlowNode ( )
11091020 } or
@@ -1166,17 +1077,7 @@ private module Cached {
11661077 predicate localFlowStepImpl ( Node nodeFrom , Node nodeTo ) {
11671078 LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
11681079 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 , _)
11801081 or
11811082 // Simple flow through library code is included in the exposed local
11821083 // step relation, even though flow is technically inter-procedural
@@ -1245,7 +1146,7 @@ import Cached
12451146
12461147/** Holds if `n` should be hidden from path explanations. */
12471148predicate nodeIsHidden ( Node n ) {
1248- n instanceof SsaDefinitionExtNode
1149+ n instanceof SsaNode
12491150 or
12501151 exists ( Parameter p | p = n .( ParameterNode ) .getParameter ( ) | not p .fromSource ( ) )
12511152 or
@@ -1279,13 +1180,16 @@ predicate nodeIsHidden(Node n) {
12791180 n instanceof CaptureNode
12801181}
12811182
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 ;
12841186 SsaImpl:: DefinitionExt def ;
12851187
1286- SsaDefinitionExtNode ( ) { this = TSsaDefinitionExtNode ( def ) }
1188+ SsaNode ( ) {
1189+ this = TSsaNode ( node ) and
1190+ def = node .getDefinitionExt ( )
1191+ }
12871192
1288- /** Gets the underlying SSA definition. */
12891193 SsaImpl:: DefinitionExt getDefinitionExt ( ) { result = def }
12901194
12911195 override DataFlowCallable getEnclosingCallableImpl ( ) {
@@ -1298,9 +1202,57 @@ class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
12981202 result = def .( Ssa:: Definition ) .getControlFlowNode ( )
12991203 }
13001204
1301- override Location getLocationImpl ( ) { result = def .getLocation ( ) }
1205+ override Location getLocationImpl ( ) { result = node .getLocation ( ) }
13021206
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 ;
13041256}
13051257
13061258/** A definition, viewed as a node in a data flow graph. */
@@ -2946,7 +2898,7 @@ private predicate delegateCreationStep(Node nodeFrom, Node nodeTo) {
29462898/** Extra data-flow steps needed for lambda flow analysis. */
29472899predicate additionalLambdaFlowStep ( Node nodeFrom , Node nodeTo , boolean preservesValue ) {
29482900 exists ( SsaImpl:: DefinitionExt def |
2949- LocalFlow :: localSsaFlowStep ( def , nodeFrom , nodeTo ) and
2901+ SsaFlow :: localFlowStep ( def , nodeFrom , nodeTo , _ ) and
29502902 preservesValue = true
29512903 |
29522904 LocalFlow:: usesInstanceField ( def )
0 commit comments