[analyzer] Record nullability implications on getting items from NSDictionary

Authored by george.karpenkov on Tue, Jul 31, 6:57 PM.



If we get an item from a dictionary, we know that the item is non-null if and only if the key is non-null.

This patch is a rather hacky way to record this implication, because some logic needs to be duplicated from the solver.
And yet, it's pretty simple, performant, and works.

Other possible approaches:

  • Record the implication, in future rely on Z3 to pick it up.
  • Generalize the current code and move it to the constraint manager.


Diff Detail

rC Clang
george.karpenkov updated this revision to Diff 158449.
george.karpenkov edited the summary of this revision. (Show Details)
dcoughlin added inline comments.Wed, Aug 1, 1:47 PM
15 ↗(On Diff #158581)

"index" --> "key". In Foundation "index" refers to an array index.

33 ↗(On Diff #158581)

I think future maintainers would find it helpful it you provided a prose description of the meaning of the data structure here. Something like: "Records an implication about non nullness between symbols. If the key symbol is constrained to be not null then the value symbol will be constrained to be not null as well."

86 ↗(On Diff #158581)

It would be good to handle -[NSMutableDictionary setObject:forKey:] here as well. There is a ridiculous amount of code that uses it since the subscript syntax is relatively new.

For the same reason, we should also handle -[NSDictionary objectForKey:] below.

92 ↗(On Diff #158581)

Can you explain why this is an if-and-only-if?

In particular, it seems to me that if the key is not null but is not present in the dictionary then the output will be null.

196 ↗(On Diff #158581)

I suspect future maintainers would appreciate a more detailed comment about how this causes infinite recursion and how removing the mapping avoids it.

43 ↗(On Diff #158581)

What's this about?

92 ↗(On Diff #158581)

The comment is outdated and wrong, will fix

43 ↗(On Diff #158581)

@NoQ would probably want to correct me here, but last time he explained it to me, the configuration dumping is not actually guaranteed to work, and unrelated changes may cause previous (for some reason unshown) changes to propagate. I'm still not sure exactly why.

NoQ added inline comments.Wed, Aug 1, 3:20 PM
43 ↗(On Diff #158581)

It means that the provided test now covers a call to shouldIncludeAllocationSiteInLeakDiagnostics(). Which changes the previously not-present key in the analyzer options map to become set to the default value.

It is impossible to list all values in the analyzer options map because they aren't just listed there until they're used. Which is why this test file has some actual code: to trigger reads from the map.

But i've no idea why specifically this code suddenly starts triggering this specific option to be read.

george.karpenkov marked 6 inline comments as done.
NoQ added inline comments.Mon, Aug 6, 3:50 PM
1 ↗(On Diff #158835)

British vs. American English thing.

63–66 ↗(On Diff #158835)

Is there anything that prevents us from reducing this method to something like

for (Antecedent in Cond) { // symbol_iterator thingy
  if (SymbolRef Consequent = State->get<ImplicationMap>(Antecedent)) {
    if (State->isNull(Antecedent).isConstrainedTrue()) // somehow avoid infinite recursion
      return State->remove<ImplicationMap>(Antecedent)->assume(Consequent, false);
    if (State->isNull(Antecedent).isConstrainedFalse())
      return State->remove<ImplicationMap>(Antecedent)->assume(Consequent, true);


george.karpenkov marked an inline comment as done.
NoQ added inline comments.Mon, Aug 6, 6:23 PM
41 ↗(On Diff #159438)


140–147 ↗(On Diff #159438)

I think there should be at most two remove<>s per dead symbol.

Also because the dead set is deprecated and we plan to remove it, maybe iterate over the map instead?

225 ↗(On Diff #159438)

Should we clean both maps up immediately?

george.karpenkov marked 2 inline comments as done.Fri, Aug 10, 3:08 PM
george.karpenkov added inline comments.
41 ↗(On Diff #159438)

Nope, the direction is correct here, assuming antecedent is the key, and consequent is the value

NoQ added inline comments.Fri, Aug 10, 3:09 PM
41 ↗(On Diff #159438)

Mmm, aha, ok.

NoQ accepted this revision.Fri, Aug 10, 3:16 PM

I hope eventually we'll be able to reduce this code to a single assume() directive.

This revision is now accepted and ready to land.Fri, Aug 10, 3:16 PM
This revision was automatically updated to reflect the committed changes.