sharing_map::get_delta_view fix

[jezhiggins]

In a system under test we're encountering an invariant failure

--- begin invariant violation report ---
Invariant check failed
File: ../util/sharing_map.h:428 function: get_other_map_value
Condition: is_in_both_maps()
Reason: Precondition
Backtrace:

In abstract_environmentt::merge, after a bit of preamble we do the actual merge

  for(const auto &entry : env.map.get_delta_view(map))
  {
    auto merge_result = abstract_objectt::merge(
      entry.get_other_map_value(), entry.m, merge_location, widen_mode);

    modified |= merge_result.modified;
    map.replace(entry.k, merge_result.object);
  }

The invariant violation occurs in the entry.get_other_map_value() call, because the entry is not, in fact, in the other map.

There appears to be a problem in how the delta_view is calculated. I don't pretend to understand how the delta is calculated - I assume we're walking the map internal structures, but that's a little bit involved - but for the erroneous entry end up in sharing_map::add_item_if_not_shared, specifically at the line highlighted below

  if(ip->is_leaf())
  {
    if(ip->shares_with(leaf))
      return;

    if(equalT()(leaf.get_key(), ip->get_key()))
    {
      delta_view.push_back({k, leaf.get_value(), ip->get_value()});
      return;
    }

    delta_view.push_back({k, leaf.get_value()});  <--- DANGER WILL ROBINSON
    return;
  }

At this point leaf.get_value() is main_loop::$tmp::return_value___CPROVER_Ada_Range_Check__Range_Check_signedbv_64_signedbv_32$2 and ip->get_value() is standard__boolean_true. Obviously these values are not the same, so the if guard equalT()(leaf.get_key(), ip->get_key()) has failed, and so we're clearly adding something into the delta_view with only one value.

But why?

I suspect oversight.

The function is declared as

SHARING_MAPT(void)::add_item_if_not_shared(
  const nodet &leaf,
  const nodet &inner,
  const std::size_t level,
  delta_viewt &delta_view,
  const bool only_common) const

only_common is flag that's passed around indicates if the returned delta view should only contain key-value pairs for keys that exist in both map. In this case, it is true.

Elsewhere in the code we see this kind of pattern repeated several times.

  if(equalT()(ip1->get_key(), ip2->get_key()))
  {
    delta_view.push_back({ip1->get_key(), ip1->get_value(), ip2->get_value()});
  }
  else if(!only_common)
  {
    delta_view.push_back({ip1->get_key(), ip1->get_value()});
  }

I believe the case highlighted above should also be guarded with !only_common.

Making that change means our example runs to completion.

[tautschnig]

@jezhiggins Is there any chance to contribute a unit test or some other form of regression test?

[jezhiggins]

If believe this line indicated below,

cbmc/src/util/sharing_map.h

Line 910 in f917b98

delta_view.push_back({k, leaf.get_value()});

, should be similarly guarded. Happy to make that change in this PR too.

  if(ip->is_container())
  {
    for(const auto &l2 : ip->get_container())
    {
      if(leaf.shares_with(l2))
        return;

      if(leaf.get_key() == l2.get_key())
      {
        delta_view.push_back({k, leaf.get_value(), l2.get_value()});
        return;
      }
    }

    delta_view.push_back({k, leaf.get_value()}); // SHOULD BE GUARDED

    return;
  }

[tautschnig]

Wouldn't the same apply in line 909?

[jezhiggins]

Yes, I believe so - our comments crossed in the ether 🙂 - but I don't have a case that hits that line.

[jezhiggins]

I'd like the build to complete, and then I'll push that change too.

[martin-cs]

@tautschnig a regression test might be a challenge. This was encountered running the abstract interpreter on a large Ada code-base and triaging it down will be ... probably significantly more work than the PR.

[tautschnig]

@tautschnig a regression test might be a challenge. This was encountered running the abstract interpreter on a large Ada code-base and triaging it down will be ... probably significantly more work than the PR.

That's entirely fair. I think I had myself witnessed the described invariant failure when running goto-analyzer on some binaries, and it was far from obvious how to construct a small example from this. Perhaps a unit test would be feasible? I'd imagine hand-crafting sharing maps that look like the ones found right before the invariant failure. (But even that is a lot of work, I do concede.)

[codecov]

Codecov Report

Merging #6295 (0b7e36b) into develop (74e4365) will decrease coverage by 0.00%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #6295      +/-   ##
===========================================
- Coverage    75.96%   75.96%   -0.01%     
===========================================
  Files         1508     1508              
  Lines       163292   163296       +4     
===========================================
+ Hits        124052   124055       +3     
- Misses       39240    39241       +1     

Impacted Files	Coverage Δ
src/util/sharing_map.h	88.14% <100.00%> (+0.03%)	⬆️
src/solvers/flattening/bv_pointers.cpp	82.56% <0.00%> (-0.11%)	⬇️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update f917b98...0b7e36b. Read the comment docs.

[martin-cs]

Approve assuming that you have tested this on the original problem and it resolves the crash.

[martin-cs]

Merging as the only check that has failed in the over-all coverage and that looks like an artefact of how it is computed.