Skip to content

Commit c49e2ab

Browse files
author
Alex Eyers-Taylor
committed
DataFlow: Add code to do overlay informed dataflow.
1 parent 82e4fc9 commit c49e2ab

File tree

5 files changed

+92
-5
lines changed

5 files changed

+92
-5
lines changed

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplSpecific.qll

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ module;
66

77
private import semmle.code.Location
88
private import codeql.dataflow.DataFlow
9+
private import semmle.code.java.Overlay
910

1011
module Private {
1112
import DataFlowPrivate
@@ -29,4 +30,6 @@ module JavaDataFlow implements InputSig<Location> {
2930
predicate mayBenefitFromCallContext = Private::mayBenefitFromCallContext/1;
3031

3132
predicate viableImplInCallContext = Private::viableImplInCallContext/2;
33+
34+
predicate isEvaluatingInOverlay = isOverlay/0;
3235
}

shared/dataflow/codeql/dataflow/DataFlow.qll

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -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

354366
module Configs<LocationSig Location, InputSig<Location> Lang> {
@@ -1101,6 +1113,8 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
11011113
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
11021114
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
11031115
}
1116+
1117+
predicate observeOverlayInformedIncrementalMode() { none() }
11041118
}
11051119

11061120
private module Stage1 = ImplStage1<C>;
@@ -1130,6 +1144,8 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
11301144
) {
11311145
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
11321146
}
1147+
1148+
predicate observeOverlayInformedIncrementalMode() { none() }
11331149
}
11341150

11351151
private module Stage1 = ImplStage1<C>;

shared/dataflow/codeql/dataflow/TaintTracking.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -167,6 +167,8 @@ module TaintFlowMake<
167167
) {
168168
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
169169
}
170+
171+
predicate observeOverlayInformedIncrementalMode() { none() }
170172
}
171173

172174
private module C implements DataFlowInternal::FullStateConfigSig {
@@ -201,6 +203,8 @@ module TaintFlowMake<
201203
) {
202204
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
203205
}
206+
207+
predicate observeOverlayInformedIncrementalMode() { none() }
204208
}
205209

206210
private module C implements DataFlowInternal::FullStateConfigSig {
@@ -232,6 +236,8 @@ module TaintFlowMake<
232236
) {
233237
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
234238
}
239+
240+
predicate observeOverlayInformedIncrementalMode() { none() }
235241
}
236242

237243
private module C implements DataFlowInternal::FullStateConfigSig {
@@ -270,6 +276,8 @@ module TaintFlowMake<
270276
) {
271277
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
272278
}
279+
280+
predicate observeOverlayInformedIncrementalMode() { none() }
273281
}
274282

275283
private module C implements DataFlowInternal::FullStateConfigSig {

shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
143143
*/
144144
predicate observeDiffInformedIncrementalMode();
145145

146+
/**
147+
* Holds if sources and sinks should be filtered to only include those that
148+
* are in the overlay database. This only has an effect when running
149+
* in overlay-informed incremental mode. This should be used in conjunction
150+
* with the `OverlayImpl` implementation to merge the base results back in.
151+
*/
152+
predicate observeOverlayInformedIncrementalMode();
153+
146154
Location getASelectedSourceLocation(Node source);
147155

148156
Location getASelectedSinkLocation(Node sink);

shared/dataflow/codeql/dataflow/internal/DataFlowImplStage1.qll

Lines changed: 57 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
* Provides an implementation of a fast initial pruning of global
55
* (interprocedural) data flow reachability (Stage 1).
66
*/
7-
overlay[local?]
7+
overlay[local?] // when this is removed, put `overlay[local?]` on `isOverlayNode`.
88
module;
99

1010
private import codeql.util.Unit
@@ -129,23 +129,75 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
129129

130130
private module AlertFiltering = AlertFilteringImpl<Location>;
131131

132+
/**
133+
* Holds if the given node is visible in overlay-only local evaluation.
134+
*
135+
* This predicate needs to be `overlay[local?]`, either directly or
136+
* through annotations from an outer scope. If `Node` is global for the
137+
* language under analysis, then every node is considered an overlay
138+
* node, which means there will effectively be no overlay-based
139+
* filtering of sources and sinks.
140+
*/
141+
private predicate isOverlayNode(Node node) {
142+
isEvaluatingInOverlay() and
143+
// Any local node is an overlay node if we are evaluating in overlay mode
144+
exists(node)
145+
}
146+
147+
/**
148+
* The filtering if we aren't meant to be diff-informed.
149+
*
150+
* Shared between sources and sinks.
151+
*/
152+
pragma[inline]
153+
private predicate nonDiffInformedFilter(Node node) {
154+
// If we are in base-only global evaluation, do not filter out any sources.
155+
not isEvaluatingInOverlay()
156+
or
157+
// If the configuration doesn't merge overlays, do not filter out any sources.
158+
not Config::observeOverlayInformedIncrementalMode()
159+
or
160+
// If we are in global evaluation with an overlay present, restrict
161+
// sources to those visible in the overlay.
162+
isOverlayNode(node)
163+
}
164+
165+
overlay[global]
132166
pragma[nomagic]
133167
private predicate isFilteredSource(Node source) {
134168
Config::isSource(source, _) and
169+
// Data flow is always incremental in one of two ways.
170+
// 1. If the configuration is diff-informed, we filter to only include nodes in the diff,
171+
// which gives the smallest set of nodes.
172+
// If diff information is not available, we do not filter at all.
173+
// 2. If not, in global evaluation with overlay, we filter to only
174+
// include nodes from files in the overlay; flow from
175+
// other nodes will be added back later.
176+
// We start by seeing if we should be in case 1.
135177
if Config::observeDiffInformedIncrementalMode()
136-
then AlertFiltering::filterByLocation(Config::getASelectedSourceLocation(source))
137-
else any()
178+
then
179+
// Case 1: We are meant to be diff-informed.
180+
// We still only filter if we have diff information.
181+
AlertFiltering::diffInformationAvailable()
182+
implies
183+
AlertFiltering::locationIsInDiff(Config::getASelectedSourceLocation(source))
184+
else nonDiffInformedFilter(source)
138185
}
139186

187+
overlay[global]
140188
pragma[nomagic]
141189
private predicate isFilteredSink(Node sink) {
142190
(
143191
Config::isSink(sink, _) or
144192
Config::isSink(sink)
145193
) and
194+
// See the comments in `isFilteredSource` for the reasoning behind the following.
146195
if Config::observeDiffInformedIncrementalMode()
147-
then AlertFiltering::filterByLocation(Config::getASelectedSinkLocation(sink))
148-
else any()
196+
then
197+
AlertFiltering::diffInformationAvailable()
198+
implies
199+
AlertFiltering::locationIsInDiff(Config::getASelectedSinkLocation(sink))
200+
else nonDiffInformedFilter(sink)
149201
}
150202

151203
private predicate hasFilteredSource() { isFilteredSource(_) }

0 commit comments

Comments
 (0)