C++: Implement Instruction.isResultConflated #3097

jbj · 2020-03-20T17:03:50Z

This predicate replaces isChiForAllAliasedMemory, which was always intended to be temporary. A test is added to IRSanity.qll to verify that the new predicate corresponds exactly with ~~(a fixed version of)~~ the old one.

The implementation of the new predicate, Cached::hasConflatedMemoryResult in SSAConstruction.qll, is faster to compute than the old isChiForAllAliasedMemory because it uses information that's readily available during SSA construction.

EDIT: This PR now also contains a fix for how EntireAllocationMemoryLocation is modelled. There were cases before where InitializeParameterInstruction appeared to overwrite the result of AliasedDefinitionInstruction.

This predicate replaces `isChiForAllAliasedMemory`, which was always intended to be temporary. A test is added to `IRSanity.qll` to verify that the new predicate corresponds exactly with (a fixed version of) the old one. The implementation of the new predicate, `Cached::hasConflatedMemoryResult` in `SSAConstruction.qll`, is faster to compute than the old `isChiForAllAliasedMemory` because it uses information that's readily available during SSA construction.

jbj · 2020-03-20T17:11:07Z

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll

+   * as originating on the `AliasedDefinitionInstruction` at the entry of the
+   * function.
+   */
+  final predicate isResultConflated() { Construction::hasConflatedMemoryResult(this) }


I modelled the naming of this predicate on isResultModeled, which is right above it.

It might be confusing that this predicate is inverted compared to isResultModeled: the new predicate holds when the instruction is imprecise, whereas isResultModeled holds when it's (in a sense) precise. Do we need isResultModeled? It's currently only used for the pretty-printer, and I think isResultConflated might be better for pretty-printing.

I don't think there will be much use of isResultModeled. In fact, I believe that your usage is the first outside of the Instruction class itself.

I like having unmodeled results and operands print out as mu instead of m. I do think that isResultConflated is worth displaying in IR dumps as well, though. I'm not sure what punctuation to use for that, but Emoji open up a world of possibilities:
# 134| m134_4🔀(unknown) = Chi : total:m134_2, partial:m134_3

Um... yes. I was thinking ma for results and operands that are conflated but not unmodelled.

...where the a is for Aliased.

jbj · 2020-03-20T17:12:26Z

cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/IRConstruction.qll

+    or
+    instruction instanceof AliasedDefinitionInstruction
+    or
+    instruction.getOpcode() instanceof Opcode::InitializeNonLocal


All the uses of InitializeNonLocal can hopefully just go away when we remove that opcode. That means this PR has a semantic conflict with @rdmarsh2's work.

dbartol

I like the approach. A few comments on the details.

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll

dbartol · 2020-03-20T17:55:50Z

csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll

@@ -65,6 +65,30 @@ private module Cached {
    instruction instanceof ChiInstruction // Chis always have modeled results
  }

+  cached


In plain language, this predicate is basically identifying instructions that are either writing to all of aliased memory (AliasedDefinition, InitializeNonLocal, certain Chis and Phis), or are unmodeled, right? If so, I think it can be simplified:

If the memory location of the result of the old instruction totally overlaps AliasedVirtualVariable

If the instruction is a Chi, and the virtual variable of the result of the non-Chi old instruction is AliasedVirtualVariable.

If the result of the instruction is unmodeled.

Yes, that's the definition I have in mind. But it's not clear to me how your alternative implementation can be written down just in terms of predicates that are public in AliasedSSA.qll and SimpleSSA.qll. (I cheated and added a few lines to SimpleSSA.qll to make my implementation work).

csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll

dbartol · 2020-03-20T18:04:48Z

csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll

+    or
+    exists(Alias::MemoryLocation location |
+      instruction = Phi(_, location) and
+      location.getVirtualVariable() instanceof Alias::AliasedVirtualVariable


I should be possible to have a Phi for a specific (non-conflated) location that happens to be part of AliasedVirtualVariable. I'm not sure if we have this specific test case, but in ssa.cpp, function MergeMustExactlyWithMustTotallyOverlap shows how this works when the location in question does not escape. You get two Phi instructions, one for the entire virtual variable, and one for the specific location within that virtual variable. See the QLDoc for the PhiInsertion module in SSAConstruction.qll for a bit more detail on the how and why.

What would a test case look like?

Perhaps this issue has to do with the test failures.

I've written a test case that exhibits the problem you describe.

I've just pushed a commit to demonstrate the problem, followed by a commit to fix it.

dbartol · 2020-03-20T18:14:31Z

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll

+   * as originating on the `AliasedDefinitionInstruction` at the entry of the
+   * function.
+   */
+  final predicate isResultConflated() { Construction::hasConflatedMemoryResult(this) }


I don't think there will be much use of isResultModeled. In fact, I believe that your usage is the first outside of the Instruction class itself.

I like having unmodeled results and operands print out as mu instead of m. I do think that isResultConflated is worth displaying in IR dumps as well, though. I'm not sure what punctuation to use for that, but Emoji open up a world of possibilities:
# 134| m134_4🔀(unknown) = Chi : total:m134_2, partial:m134_3

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll

jbj · 2020-03-20T18:43:22Z

There are test failures in the sound IR. I hadn't found these tests because I apparently grepped for the wrong thing. I'll investigate.

dbartol · 2020-03-23T20:30:42Z

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/AliasedSSA.qll

      not use instanceof EntireAllocationMemoryLocation and
-      result instanceof MustTotallyOverlap
+      if def.getAllocation() = use.getAllocation()


Yes, this looks right.

The DIL LGTM, and so do the tuple counts on Wireshark.

I had included `InitializeNonLocal` in the recursion because it made everything look better in the presence of a bug that's since been fixed. Taking it out means the sanity test is again aligned with the old `isChiForAllAliasedMemory`.

…memory Conflicts: cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/IRSanity.qll cpp/ql/src/semmle/code/cpp/ir/implementation/raw/IRSanity.qll cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/IRSanity.qll cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity.expected cpp/ql/test/library-tests/ir/ir/aliased_ssa_sanity_unsound.expected cpp/ql/test/library-tests/ir/ir/raw_sanity.expected cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected cpp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity_unsound.expected cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity.expected cpp/ql/test/library-tests/ir/ssa/aliased_ssa_sanity_unsound.expected cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity.expected cpp/ql/test/library-tests/ir/ssa/unaliased_ssa_sanity_unsound.expected cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected csharp/ql/src/semmle/code/csharp/ir/implementation/raw/IRSanity.qll csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRSanity.qll csharp/ql/test/library-tests/ir/ir/raw_ir_sanity.expected csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected

dbartol

LGTM now

jbj added the C++ label Mar 20, 2020

jbj requested review from a team as code owners March 20, 2020 17:03

jbj commented Mar 20, 2020

View reviewed changes

dbartol reviewed Mar 20, 2020

View reviewed changes

jbj commented Mar 20, 2020

View reviewed changes

cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll Show resolved Hide resolved

C++: Remove redundant case

79d5b88

C++: Fix getExtentOverlap for entire allocation

b0d3c9e

jbj added the WIP This is a work-in-progress, do not merge yet! label Mar 23, 2020

jbj added 2 commits March 23, 2020 20:32

C++: QLDoc terminology: object -> mem allocation

999051d

C#: Fixup to follow C++ changes

29c4c8c

dbartol reviewed Mar 23, 2020

View reviewed changes

jbj added 2 commits March 24, 2020 13:31

C++: failing test for non-conflated escaped var

95a8dcb

C++: Phi-node conflation is not about vvars

2783214

jbj removed the WIP This is a work-in-progress, do not merge yet! label Mar 24, 2020

jbj added 3 commits March 24, 2020 16:46

C++: Sync identical files

4e58886

C++: Fix conflated-memory sanity query

8f419d1

I had included `InitializeNonLocal` in the recursion because it made everything look better in the presence of a bug that's since been fixed. Taking it out means the sanity test is again aligned with the old `isChiForAllAliasedMemory`.

This was referenced Mar 25, 2020

C++: Wire up param/arg indirections in data flow #3123

Merged

C++: IR field flow #3118

Merged

dbartol approved these changes Mar 26, 2020

View reviewed changes

dbartol merged commit 7879dde into github:master Mar 26, 2020

C++: Implement Instruction.isResultConflated #3097

C++: Implement Instruction.isResultConflated #3097

Uh oh!

Conversation

jbj commented Mar 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dbartol 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!

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!

Uh oh!

jbj commented Mar 20, 2020

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dbartol left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jbj commented Mar 20, 2020 •

edited

Loading