Java: Add data-flow consistency checks. #2921

aschackmull · 2020-02-26T13:35:31Z

This adds a number of consistency queries (i.e. queries that ought to return zero results) for the shared data-flow implementation. The main file is language-independent and can be synced across languages. The idea is that this should help document expectations and invariants in the shared implementation. For Java, these queries mostly give zero results, but extractor issues can result in nodes without callables, and the TypeFlow library can give multiple type bounds in some corner cases.

A few unresolved questions:

One of the checks needs a tiny bit of customisation via the predicate isImmutableOrUnobservable(Node n) to disregard arguments without PostUpdateNodes when they have been consciously excluded. Currently I've put this in DataFlowPrivate.qll, but perhaps this predicate ought to go in its own file?
The checks currently reside next to the implementation, as this was the easiest way to access the language-specific imports. Should this move to somewhere in <lang>/ql/test/ instead? A related question is how our plumming for consistency queries work at the moment and whether that gives some restrictions?

When we are happy with the structure, I can sync this to C# and C++.

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll

jbj

I'm happy with the proposed resolution for the two unresolved questions in the PR description.

The next step can be to duplicate this for other languages and import the new module from a few new one-line ql files in the dataflow test directories.

max-schaefer

@aschackmull, I have questions about two of the consistency checks. They currently don't hold for Go (because I went with a very lazy implementation of post-update nodes), and I'm wondering how bad that is.

max-schaefer · 2020-03-02T09:18:02Z

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll

+  }
+
+  query predicate postIsNotPre(PostUpdateNode n, string msg) {
+    n.getPreUpdateNode() = n and msg = "PostUpdateNode should not equal its pre-update node."


Could you comment briefly on what happens if this condition is violated?

Flow that exits a method call through a side-effect on an argument may re-enter the method. E.g. in the following you'll get wrong flow from source to sink if you have a call to someMethod where the PostUpdateNode for the argument equals the ArgumentNode:

someMethod(A a) { sink(a.f); a.f = source(); }

Makes sense.

max-schaefer · 2020-03-02T09:18:10Z

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll

+    exists(int c |
+      c = count(n.getPreUpdateNode()) and
+      c != 1 and
+      msg = "PostUpdateNode should have one pre-update node but has " + c + "."


One example is that a store to a PostUpdateNode that doesn't have a corresponding pre-update won't be able to exit through a parameter: in someMethod(A a) { a.f = source(); } the store targets the post-update read of a in the qualifier of a.f, combined with local value flow from the ParameterNode to the corresponding pre-update node, the store is observed as a side-effect of the method and can then exit through the parameter and reach a PostUpdateNode of an argument in a call to someMethod. I don't really have an overview of what would happen if a PostUpdateNode has multiple pre-update nodes.

Right, I was mostly asking about the case of multiple pre-update nodes. Glad to hear it's not known to mess things up massively.

max-schaefer · 2020-03-02T12:29:28Z

Thanks for your responses, @aschackmull. I think we'll stick with our current simple implementation of post-update nodes for Go, and switch to a more sophisticated model when we start seeing too much imprecision.

MathiasVP · 2020-03-02T12:44:37Z

Should the new module be named DataFlowSanity (or something similar) for consistency with the InstructionSanity module in Instruction.qll?

aschackmull · 2020-03-02T14:44:12Z

Should the new module be named DataFlowSanity (or something similar) for consistency with the InstructionSanity module in Instruction.qll?

For these kinds of queries "consistency" is the preferred term over "sanity".

hvitved

Great initiative, @aschackmull .

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll

hvitved · 2020-03-06T08:44:43Z

cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplConsistency.qll

+  query predicate uniqueTypeRepr(Node n, string msg) {
+    exists(int c |
+      n instanceof RelevantNode and
+      c = count(getErasedRepr(n.getTypeBound())) and


You could use getErasedNodeTypeBound here instead...

That requires an additional import of DataFlowImplCommon, so perhaps just leave as-is?

jbj · 2020-03-11T08:54:01Z

As it stands, this PR just introduces a lot of unreachable code in qll files. Is there any value to merging that before we have ql/qlref files that reference it?

For C/C++ (AST and IR), I suggest putting a qlref file in cpp/ql/test/library-tests/dataflow/fields, cpp/ql/test/library-tests/dataflow/dataflow-tests, and cpp/ql/test/library-tests/syntax-zoo.

aschackmull · 2020-03-11T09:50:19Z

I've added the C++ tests as well as 4 additional checks related to toString and location.

aschackmull · 2020-03-30T08:59:52Z

@hvitved @jbj Anything holding this back? I'd like to get it in before it starts to bitrot.

jbj

I think it's fine to merge. I just hadn't noticed that 85d6b7c was pushed.

The results for C/C++ look wrong, but we can address that in a follow-up PR.

hvitved · 2020-03-30T10:47:26Z

Let's get it in. I will add C# tests in a follow-up PR.

Java: Add data-flow consistency checks.

ce70b86

aschackmull added C# C++ Java labels Feb 26, 2020

aschackmull requested a review from a team as a code owner February 26, 2020 13:35

jbj reviewed Feb 26, 2020

View reviewed changes

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll Outdated Show resolved Hide resolved

jbj reviewed Feb 26, 2020

View reviewed changes

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll Show resolved Hide resolved

Java: Change relevantNode to a class, and add two more checks.

a09e479

jbj reviewed Feb 27, 2020

View reviewed changes

java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll Outdated Show resolved Hide resolved

Java: Include count in messages.

8e2b56c

jbj previously approved these changes Feb 27, 2020

View reviewed changes

C++/C#: Add synchronization.

67d386b

aschackmull dismissed jbj’s stale review via 67d386b February 27, 2020 13:32

aschackmull requested review from a team as code owners February 27, 2020 13:32

max-schaefer reviewed Mar 2, 2020

View reviewed changes

rdmarsh2 mentioned this pull request Mar 5, 2020

C++: Move InstructionSanity out of Instruction.qll #2994

Merged

hvitved reviewed Mar 6, 2020

View reviewed changes

Dataflow: Adjust imports.

e97c72c

hvitved previously approved these changes Mar 10, 2020

View reviewed changes

aschackmull added 2 commits March 11, 2020 10:29

Dataflow: Add consistency checks for toString and location.

a9d76cb

C++: Add tests.

85d6b7c

aschackmull dismissed hvitved’s stale review via 85d6b7c March 11, 2020 09:49

MathiasVP mentioned this pull request Mar 24, 2020

C++: IR field flow #3118

Merged

jbj approved these changes Mar 30, 2020

View reviewed changes

hvitved merged commit 9fa9c10 into github:master Mar 30, 2020

aschackmull deleted the dataflow/consistency-checks branch March 30, 2020 10:48

jbj mentioned this pull request Mar 30, 2020

C++: Remove noise from argHasPostUpdate check #3162

Merged

Java: Add data-flow consistency checks. #2921

Java: Add data-flow consistency checks. #2921

Conversation

aschackmull commented Feb 26, 2020

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jbj left a comment

Choose a reason for hiding this comment

Uh oh!

max-schaefer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

max-schaefer commented Mar 2, 2020

Uh oh!

MathiasVP commented Mar 2, 2020

Uh oh!

aschackmull commented Mar 2, 2020

Uh oh!

hvitved left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jbj commented Mar 11, 2020

Uh oh!

aschackmull commented Mar 11, 2020

Uh oh!

aschackmull commented Mar 30, 2020

Uh oh!

jbj left a comment

Choose a reason for hiding this comment

Uh oh!

hvitved commented Mar 30, 2020

Uh oh!

Uh oh!