-
Notifications
You must be signed in to change notification settings - Fork 1.6k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
JavaScript: Add flow tracking through nested properties. #90
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -344,7 +344,8 @@ private predicate exploratoryFlowStep(DataFlow::Node pred, DataFlow::Node succ, | |
DataFlow::Configuration cfg) { | ||
basicFlowStep(pred, succ, _, cfg) or | ||
basicStoreStep(pred, succ, _) or | ||
loadStep(pred, succ, _) | ||
loadStep(pred, succ, _) or | ||
reverseLoadStep(pred, succ, _) | ||
} | ||
|
||
/** | ||
|
@@ -483,6 +484,72 @@ private predicate reachableFromStoreBase(string prop, DataFlow::Node rhs, DataFl | |
newSummary.valuePreserving() = true and | ||
summary = oldSummary.append(newSummary) | ||
) | ||
or | ||
nestedPropFlow(prop, rhs, nd, cfg, summary) | ||
} | ||
|
||
/** | ||
* Holds if `rhs` is the right-hand side of a write to property `outerProp` and some read of | ||
* another property `innerProp` is reachable from the base of that write under configuration `cfg`, | ||
* and from the base of that inner read we can reach a read `succ` of the same property `innerProp`, | ||
* such that the path from `rhs` to `succ` is summarized by `summary`. | ||
* | ||
* Example: | ||
* | ||
* ``` | ||
* let root = new A(); | ||
* let base = root.innerProp; | ||
* base.outerProp = rhs; | ||
* let succ = root.innerProp; | ||
* ``` | ||
*/ | ||
private predicate nestedPropFlow(string outerProp, DataFlow::Node rhs, DataFlow::Node succ, | ||
DataFlow::Configuration cfg, PathSummary summary) { | ||
exists (DataFlow::PropRead nestedRead, PathSummary oldSummary | | ||
reachableFromStoreBase(outerProp, rhs, nestedRead, cfg, oldSummary) and | ||
loadLoadPair(nestedRead, succ, cfg, oldSummary, summary) | ||
) | ||
} | ||
|
||
/** | ||
* Holds if `load` is a read of some property `innerProp` from which we can reach a read `succ` of the same | ||
* property `innerProp` under configuration `cfg`, and the concatenation of `oldSummary` with the summary | ||
* of that path is `summary`. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This was quite confusing for the same reason as the above, because in the example nothing appears to be reachable from |
||
* | ||
* Example: | ||
* | ||
* ``` | ||
* let root = A(); | ||
* let load = root.innerProp; | ||
* let succ = root.innerProp; | ||
* ``` | ||
*/ | ||
pragma[noinline] | ||
private predicate loadLoadPair(DataFlow::PropRead load, DataFlow::Node succ, | ||
DataFlow::Configuration cfg, PathSummary oldSummary, PathSummary summary) { | ||
exists (string innerProp, DataFlow::Node nd, PathSummary newSummary | | ||
reachableFromLoadBase(innerProp, load, nd, cfg, newSummary) and | ||
loadStep(nd, succ, innerProp) and | ||
summary = oldSummary.append(newSummary) | ||
) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't understand why we have two It seems like the summary of this edge is a pair of input/output summaries, instead of just being a summary. I mean that's what Apart from that, is it correctly understood that we would get N^2 load-load pairs for code like this?
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, that's a bad case with the current implementation. Adding |
||
} | ||
|
||
/** | ||
* Holds if `read` is a read of property `prop`, and `nd` is reachable from the base of that read | ||
* under configuration `cfg` (possibly through callees) along a path summarized by `summary`. | ||
*/ | ||
private predicate reachableFromLoadBase(string prop, DataFlow::Node read, DataFlow::Node nd, | ||
DataFlow::Configuration cfg, PathSummary summary) { | ||
reachableFromStoreBase(_, _, read, cfg, _) and | ||
reverseLoadStep(read, nd, prop) and | ||
summary = PathSummary::empty() | ||
or | ||
exists (DataFlow::Node mid, PathSummary oldSummary, PathSummary newSummary | | ||
reachableFromLoadBase(prop, read, mid, cfg, oldSummary) and | ||
flowStep(mid, cfg, nd, newSummary) and | ||
newSummary.valuePreserving() = true and | ||
summary = oldSummary.append(newSummary) | ||
) | ||
} | ||
|
||
/** | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This part was a bit confusing (in the otherwise light and enjoyable prose).
If I understand it correctly now, this predicate "defines" that there is an edge from
rhs
tosucc
, is that right? The "such that" seems to imply a condition that must be satisfied for the predicate to hold, but it's really the other way around; the edge is there because this predicate says so.I think it would clarify things to talk separately about the edge defined by the predicate, and those it uses to generate it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You're right; this needs to be documented better.