@@ -349,6 +349,18 @@ signature module InputSig<LocationSig Location> {
349349
350350 /** Holds if `fieldFlowBranchLimit` should be ignored for flow going into/out of `c`. */
351351 default predicate ignoreFieldFlowBranchLimit ( DataFlowCallable c ) { none ( ) }
352+
353+ /**
354+ * Holds if the evaluator is currently evaluating with an overlay. The
355+ * implementation of this predicate needs to be `overlay[local]`. For a
356+ * language with no overlay support, `none()` is a valid implementation.
357+ *
358+ * When called from a local predicate, this predicate holds if we are in the
359+ * overlay-only local evaluation. When called from a global predicate, this
360+ * predicate holds if we are evaluating globally with overlay and base both
361+ * visible.
362+ */
363+ default predicate isEvaluatingInOverlay ( ) { none ( ) }
352364}
353365
354366module Configs< LocationSig Location, InputSig< Location > Lang> {
@@ -645,10 +657,8 @@ private module PathGraphSigMod {
645657 }
646658}
647659
648- module DataFlowMake < LocationSig Location, InputSig< Location > Lang> {
660+ private module DataFlowMakeCore < LocationSig Location, InputSig< Location > Lang> {
649661 private import Lang
650- private import internal.DataFlowImpl:: MakeImpl< Location , Lang >
651- private import internal.DataFlowImplStage1:: MakeImplStage1< Location , Lang >
652662 import Configs< Location , Lang >
653663
654664 /**
@@ -691,59 +701,6 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
691701 predicate flowToExpr ( DataFlowExpr sink ) ;
692702 }
693703
694- /**
695- * Constructs a global data flow computation.
696- */
697- module Global< ConfigSig Config> implements GlobalFlowSig {
698- private module C implements FullStateConfigSig {
699- import DefaultState< Config >
700- import Config
701-
702- predicate accessPathLimit = Config:: accessPathLimit / 0 ;
703-
704- predicate isAdditionalFlowStep ( Node node1 , Node node2 , string model ) {
705- Config:: isAdditionalFlowStep ( node1 , node2 ) and model = "Config"
706- }
707- }
708-
709- private module Stage1 = ImplStage1< C > ;
710-
711- import Stage1:: PartialFlow
712-
713- private module Flow = Impl< C , Stage1:: Stage1NoState > ;
714-
715- import Flow
716- }
717-
718- /**
719- * Constructs a global data flow computation using flow state.
720- */
721- module GlobalWithState< StateConfigSig Config> implements GlobalFlowSig {
722- private module C implements FullStateConfigSig {
723- import Config
724-
725- predicate accessPathLimit = Config:: accessPathLimit / 0 ;
726-
727- predicate isAdditionalFlowStep ( Node node1 , Node node2 , string model ) {
728- Config:: isAdditionalFlowStep ( node1 , node2 ) and model = "Config"
729- }
730-
731- predicate isAdditionalFlowStep (
732- Node node1 , FlowState state1 , Node node2 , FlowState state2 , string model
733- ) {
734- Config:: isAdditionalFlowStep ( node1 , state1 , node2 , state2 ) and model = "Config"
735- }
736- }
737-
738- private module Stage1 = ImplStage1< C > ;
739-
740- import Stage1:: PartialFlow
741-
742- private module Flow = Impl< C , Stage1:: Stage1WithState > ;
743-
744- import Flow
745- }
746-
747704 signature class PathNodeSig {
748705 /** Gets a textual representation of this element. */
749706 string toString ( ) ;
@@ -1141,3 +1098,135 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
11411098 import PathGraph
11421099 }
11431100}
1101+
1102+ module DataFlowMake< LocationSig Location, InputSig< Location > Lang> {
1103+ import DataFlowMakeCore< Location , Lang >
1104+ private import Lang
1105+ private import internal.DataFlowImpl:: MakeImpl< Location , Lang >
1106+ private import internal.DataFlowImplStage1:: MakeImplStage1< Location , Lang >
1107+
1108+ /**
1109+ * Constructs a global data flow computation.
1110+ */
1111+ module Global< ConfigSig Config> implements GlobalFlowSig {
1112+ private module C implements FullStateConfigSig {
1113+ import DefaultState< Config >
1114+ import Config
1115+
1116+ predicate accessPathLimit = Config:: accessPathLimit / 0 ;
1117+
1118+ predicate isAdditionalFlowStep ( Node node1 , Node node2 , string model ) {
1119+ Config:: isAdditionalFlowStep ( node1 , node2 ) and model = "Config"
1120+ }
1121+
1122+ predicate observeOverlayInformedIncrementalMode ( ) { none ( ) }
1123+ }
1124+
1125+ private module Stage1 = ImplStage1< C > ;
1126+
1127+ import Stage1:: PartialFlow
1128+
1129+ private module Flow = Impl< C , Stage1:: Stage1NoState > ;
1130+
1131+ import Flow
1132+ }
1133+
1134+ /**
1135+ * Constructs a global data flow computation using flow state.
1136+ */
1137+ module GlobalWithState< StateConfigSig Config> implements GlobalFlowSig {
1138+ private module C implements FullStateConfigSig {
1139+ import Config
1140+
1141+ predicate accessPathLimit = Config:: accessPathLimit / 0 ;
1142+
1143+ predicate isAdditionalFlowStep ( Node node1 , Node node2 , string model ) {
1144+ Config:: isAdditionalFlowStep ( node1 , node2 ) and model = "Config"
1145+ }
1146+
1147+ predicate isAdditionalFlowStep (
1148+ Node node1 , FlowState state1 , Node node2 , FlowState state2 , string model
1149+ ) {
1150+ Config:: isAdditionalFlowStep ( node1 , state1 , node2 , state2 ) and model = "Config"
1151+ }
1152+
1153+ predicate observeOverlayInformedIncrementalMode ( ) { none ( ) }
1154+ }
1155+
1156+ private module Stage1 = ImplStage1< C > ;
1157+
1158+ import Stage1:: PartialFlow
1159+
1160+ private module Flow = Impl< C , Stage1:: Stage1WithState > ;
1161+
1162+ import Flow
1163+ }
1164+ }
1165+
1166+ module DataFlowMakeOverlay< LocationSig Location, InputSig< Location > Lang> {
1167+ import DataFlowMake< Location , Lang >
1168+ private import Lang
1169+ private import internal.DataFlowImpl:: MakeImpl< Location , Lang >
1170+ private import internal.DataFlowImplStage1:: MakeImplStage1< Location , Lang >
1171+
1172+ /**
1173+ * Constructs a global data flow computation.
1174+ */
1175+ module Global< ConfigSig Config> implements GlobalFlowSig {
1176+ private module C implements FullStateConfigSig {
1177+ import DefaultState< Config >
1178+ import Config
1179+
1180+ predicate accessPathLimit = Config:: accessPathLimit / 0 ;
1181+
1182+ predicate isAdditionalFlowStep ( Node node1 , Node node2 , string model ) {
1183+ Config:: isAdditionalFlowStep ( node1 , node2 ) and model = "Config"
1184+ }
1185+
1186+ predicate observeOverlayInformedIncrementalMode ( ) {
1187+ not Config:: observeDiffInformedIncrementalMode ( )
1188+ }
1189+ }
1190+
1191+ private module Stage1 = ImplStage1< C > ;
1192+
1193+ import Stage1:: PartialFlow
1194+
1195+ private module Flow = OverlayImpl< C , Stage1:: Stage1NoState > ;
1196+
1197+ import Flow
1198+ }
1199+
1200+ /**
1201+ * Constructs a global data flow computation using flow state.
1202+ */
1203+ module GlobalWithState< StateConfigSig Config> implements GlobalFlowSig {
1204+ private module C implements FullStateConfigSig {
1205+ import Config
1206+
1207+ predicate accessPathLimit = Config:: accessPathLimit / 0 ;
1208+
1209+ predicate isAdditionalFlowStep ( Node node1 , Node node2 , string model ) {
1210+ Config:: isAdditionalFlowStep ( node1 , node2 ) and model = "Config"
1211+ }
1212+
1213+ predicate isAdditionalFlowStep (
1214+ Node node1 , FlowState state1 , Node node2 , FlowState state2 , string model
1215+ ) {
1216+ Config:: isAdditionalFlowStep ( node1 , state1 , node2 , state2 ) and model = "Config"
1217+ }
1218+
1219+ predicate observeOverlayInformedIncrementalMode ( ) {
1220+ not Config:: observeDiffInformedIncrementalMode ( )
1221+ }
1222+ }
1223+
1224+ private module Stage1 = ImplStage1< C > ;
1225+
1226+ import Stage1:: PartialFlow
1227+
1228+ private module Flow = OverlayImpl< C , Stage1:: Stage1WithState > ;
1229+
1230+ import Flow
1231+ }
1232+ }
0 commit comments